Simon Cruanes
2fb51d8082
chore: move to dune
2019-02-11 16:55:43 +01:00
Simon Cruanes
b2e646343a
do not expose St in solver, but only expose a restricted API.
2019-02-11 16:55:43 +01:00
Simon Cruanes
ef7333af6d
make state explicit and add type t state-wrapper in most modules
2019-02-11 16:55:43 +01:00
Simon Cruanes
eff8ed1c4f
split some features into minismt lib
2019-02-11 16:55:43 +01:00
Simon Cruanes
cbe3750b0d
use generative functors, remove a layer of nesting for SMT libs
2019-02-11 16:55:43 +01:00
Simon Cruanes
2707215aa2
move tseitin transformation into its own lib
2019-02-11 16:55:43 +01:00
Simon Cruanes
768f59f88b
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
2019-02-11 16:55:43 +01:00
Simon Cruanes
27d1841f6b
wip: migrate to msat 0.8
2019-01-28 21:09:57 -06:00
Simon Cruanes
4fadbeb04d
chore: migrate to dune
2019-01-18 18:37:26 -06:00
Simon Cruanes
73c7db2b4e
feat(cc): boolean propagation of literals in CC
2018-08-18 19:56:22 -05:00
Simon Cruanes
c1a662e2c8
refactor(sat): improve style of theory propagation handler
2018-08-18 19:55:30 -05:00
Simon Cruanes
324c9d2e36
fix(sat): allow proofs with unary resolution history
...
can happen if the conflict clause is a theory lemma
2018-08-18 19:54:46 -05:00
Simon Cruanes
dd58fa21ef
fix(sat): fix bug in restarts, we need to solve again after one
2018-08-18 18:08:42 -05:00
Simon Cruanes
ca531d73a6
refactor(cc): fix bugs, use list of nodes in equiv class
2018-08-18 18:06:16 -05:00
Simon Cruanes
c2d79b2e6a
fix(main): properly handle option no-restarts
2018-08-18 18:05:22 -05:00
Simon Cruanes
e6a96df0d9
chore: remove dead code in sat
2018-08-18 17:47:20 -05:00
Simon Cruanes
72750b9e1a
fix(sat): bugfix about adding clauses with true lits
2018-08-18 17:47:04 -05:00
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
