Simon Cruanes
46ff8c3ba6
fix(sat): bug with re-internalization of terms upon backtracking
2018-08-18 17:20:20 -05:00
Simon Cruanes
b8445d0ca3
refactor: introduce check_invariants in CC
...
costly, but helps find bugs
2018-08-18 14:52:44 -05:00
Simon Cruanes
bf0b5185bd
fix: proper proof for clause deduplication
2018-07-10 13:54:02 -05:00
Simon Cruanes
b7518a632a
refactor(cc): simplify congruence closure
2018-06-27 21:38:16 -05:00
Simon Cruanes
c125fdafa6
fix(sat): use Conflict exn to signal conflict on add_clause
2018-06-22 21:01:22 -05:00
Simon Cruanes
9ac274fc09
refactor: simplify literals; remove useless casts in CC; bit for pending nodes
2018-06-22 19:38:04 -05:00
Simon Cruanes
6933a7b5d0
refactor: add reset_tasks function to clear caches on backtrack
...
also refactor CC a bit
2018-06-16 22:50:03 -05:00
Simon Cruanes
5e380464ce
fix(sat): base-level = 1 under assumptions
2018-06-11 21:47:37 -05:00
Simon Cruanes
080cde778e
feat(model): proper model construction for CC + fun interpretation
2018-06-11 21:42:02 -05:00
Simon Cruanes
10d394a9c3
fix(cc): public add function must also saturate CC
2018-05-28 01:22:58 -05:00
Simon Cruanes
0b42a34a20
refactor: cleanup SAT
2018-05-25 21:33:38 -05:00
Simon Cruanes
9b8c21513a
refactor: internalize terms earlier
2018-05-25 21:32:24 -05:00
Simon Cruanes
47ddce5960
refactor: use 1st class for theory actions
2018-05-25 20:23:09 -05:00
Simon Cruanes
b73e900839
sat: only re-internalize atoms of permanent clauses, on backtrack
2018-05-25 19:36:53 -05:00
Simon Cruanes
d1c88e73f7
wip: fix main solver
2018-05-23 22:24:24 -05:00
Simon Cruanes
39be2c260e
fixes
2018-05-20 15:32:06 -05:00
Simon Cruanes
208f51276d
fix: some fixes in SAT
2018-05-20 14:43:33 -05:00
Simon Cruanes
fade033458
refactor: get SAT properly again on some problems
2018-05-20 14:30:36 -05:00
Simon Cruanes
4a39192846
refactor(sat): wip: simpler clauses
2018-05-20 13:38:39 -05:00
Simon Cruanes
f69d5cd9f1
refactor(sat): wip: simplify SAT solver
2018-05-20 13:09:51 -05:00
Simon Cruanes
5860612cd9
wip: refactor SAT solver
2018-05-11 20:33:36 -05:00
Simon Cruanes
3968688a35
large refactor of SAT solver, all internal code in Internal now
2018-05-09 22:47:21 -05:00
Simon Cruanes
36df2d952b
delay addition of clauses to internal sat solver until solve()
2018-05-09 21:09:55 -05:00
Simon Cruanes
441ca61465
remove annoying spelling mistake
2018-05-09 19:58:04 -05:00
Simon Cruanes
24bbe97ceb
rename to sidekick
2018-05-09 19:28:41 -05:00
Simon Cruanes
eb40cfa5e3
wip
2018-05-09 18:14:06 -05:00
Simon Cruanes
da77d3ab3b
add todo
2018-04-11 09:02:36 -05:00
Simon Cruanes
4e215e3d01
fix(cc): fix bugs in congruence closure and explanations
...
also, simplify API for backtracking
2018-04-02 21:10:49 -05:00
Simon Cruanes
dac3378198
improve SAT solver messages, remove semantic reason
2018-02-23 00:43:56 -06:00
Simon Cruanes
77af72e739
fix bugs in SAT solver
...
- new atoms must always be added to heap if not present
- fix slices dimensions at creation, do not depend on mutable indices
2018-02-19 21:32:13 -06:00
Simon Cruanes
d7fc5cf29d
fix problems with slices in the SAT core
2018-02-19 20:47:43 -06:00
Simon Cruanes
d53bd8671a
lower overhead for adding clauses to the SAT solver
...
- directly build clauses from arrays
- use IArrays rather than lists, when possible
- pushing local/persistent clauses is now direct, no more queues
2018-02-19 19:47:03 -06:00
Simon Cruanes
e1717f3afe
wip: heavy refactoring of SAT solver, making most things backtrackable
...
the idea is that most changes should be undone upon backtracking,
using the global `on_backtrack` command and `at_level_0` to
know when something is going to be permanent.
In particular, should be (possibly optionally) undone on backtracking:
- addition of clauses (clauses being attached)
- propagations of atoms
- addition of literals to the heap
- internalization of literals (tbd)
clauses should also be added immediately, not pushed into a queue
2018-02-11 22:58:24 -06:00
Simon Cruanes
7b44146102
make it compile! with stubs for conversion parse ast -> ast -> term
2018-02-08 22:19:32 -06:00
Simon Cruanes
d73684902f
wip: have a proper smtlib parser
2018-02-05 23:09:29 -06:00
Simon Cruanes
ac396e8cf5
rename to cdcl
2018-01-22 22:09:47 -06:00
Simon Cruanes
8c8209c08c
large refactoring to keep only a simpler, easier CDCL(T) interface
...
- only one functor to instantiate
- explicit state that is carried around
- remove minismt stuff
2018-01-22 21:52:06 -06:00
Simon Cruanes
d415f8ed20
do not expose St in solver, but only expose a restricted API.
2017-12-29 18:29:56 +01:00
Simon Cruanes
99078b2335
make state explicit and add type t state-wrapper in most modules
2017-12-29 16:48:26 +01:00
Simon Cruanes
1cd70b048c
split some features into minismt lib
2017-12-28 19:43:54 +01:00
Simon Cruanes
1037c06636
use generative functors, remove a layer of nesting for SMT libs
2017-12-28 19:12:41 +01:00
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
2f3a044271
Add local assumptions support to msat binary
2017-03-30 18:41:35 +02:00
Guillaume Bury
a13906184c
Fix warnings
2017-02-15 13:34:21 +01:00
Guillaume Bury
4159a34c20
Removed module alias for SAT expressions
2016-12-02 15:49:49 +01:00
Guillaume Bury
1d8fa08f92
Added Sat module to the lib. Updated README
2016-12-01 18:55:58 +01:00
Guillaume Bury
9cf13bd7a2
Mcsat now works (for pure equality problems)
2016-09-22 18:31:22 +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
fa8957784a
Restored simple expressions for pure SAT
2016-09-12 15:37:06 +02:00
