Simon Cruanes
7722319b0a
move tseitin transformation into its own lib
2017-12-28 16:01:36 +01:00
Simon Cruanes
ac50e10788
big refactoring
...
- move to jbuilder
- use a functorial heap (with indices embedded in lit/var)
- update Vec with optims from mc2
- change semantics of Vec.shrink
- use new Log module
2017-12-28 15:51:04 +01:00
Guillaume Bury
4159a34c20
Removed module alias for SAT expressions
2016-12-02 15:49:49 +01:00
Guillaume Bury
73ea4fea30
Removed useless check option in test_api
2016-11-22 16:58:02 +01:00
Guillaume Bury
b88b906da9
Added test for bug (conflict at level 0)
2016-11-21 15:51:55 +01:00
Guillaume Bury
4f5bb640ca
[WIP] All is setup, remains to have real theories
...
Architecture is now all setup, but theories for the smt and mcsat
solvers are currently dummy ones that are not doing anything.
2016-09-16 15:49:33 +02:00
Simon Cruanes
d6c6331d85
check proofs in test_api
2016-07-28 11:10:31 +02:00
Simon Cruanes
09b13be78d
reflect test_api result in its errcode
2016-07-27 23:24:01 +02:00
Simon Cruanes
98d5074da6
updates to tests
2016-07-27 19:09:11 +02:00
Simon Cruanes
3e54fac7f9
add some tests for the API
2016-07-27 18:54:56 +02:00