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
2db3a5a494
Ignore some smtlib statements in test executable
2017-08-25 18:36:42 +02:00
Guillaume Bury
0119d04899
Update after Dolmen change
...
Dolmen Introduced a new 'Clause' statement, which has to be taken into
account in the test executable of msat.
2017-08-09 20:54:53 +02:00
Guillaume Bury
0c99e6b2e7
[breaking] Better interface for the DOT backend
2017-07-20 13:55:55 +02:00
Guillaume Bury
2f3a044271
Add local assumptions support to msat binary
2017-03-30 18:41:35 +02:00
Guillaume Bury
8076c06047
[bugfix] Eliminate duplicates in input clauses
...
When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.
2017-02-15 13:04:54 +01:00
Guillaume Bury
1656995097
Added uninterpreted functions to mcsat solver
2016-09-23 15:39:23 +02: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
Guillaume Bury
2a33534312
Added (dummy) mcsat module for test binary
2016-09-14 19:55:57 +02:00
Guillaume Bury
0631135bd5
Smt solver with dummy theory now builds
2016-09-12 15:43:57 +02:00
Guillaume Bury
dfff903f8c
Removed additional libs.
2016-09-12 15:32:22 +02:00
Guillaume Bury
9d509241ad
[WIP] Some drastic cleanup of code
...
Some of these changes are to be reverted, among other the structure of
terms used for the instantiation of the pure SAT solver
2016-09-09 18:09:04 +02:00
Guillaume Bury
954892ac4a
[WIP] Strange compiler bug
2016-09-09 12:07:13 +02:00
Guillaume Bury
742f8c469d
Added Expr and typing module from ArchSat
2016-09-07 17:58:07 +02:00
Simon Cruanes
41557a1509
wip: make SMT great again
2016-08-16 17:20:48 +02:00
Simon Cruanes
563e9027e1
first draft of replacing push/pop by assumptions
2016-07-27 17:50:03 +02:00
Guillaume Bury
bbbc29948d
Added src directory, moved some files around
2016-07-07 15:48:50 +02:00
