Simon Cruanes
233df98229
perf(sat): proper GC for clauses
...
GC is now eager in the cleanup of watchlists and more elaborate.
It starts by marking all clauses justifying literals on the trail,
because we cannot remove them yet (they might be used in resolution
steps during clause analysis).
Then, we sort set of learnt clauses by decreasing activity, and pop them
one by one until the target size is reached. Clauses that are marked,
because they are on the trail, are kept on the side so we can push them
back at the end.
For each clause we want to remove, we start by marking it "dead".
Then we mark its two watch literals are "dirty", which means we will
need to purge their watchlists from dead clauses.
Then we purge watchlists (remove deadclauses entirely). At this point
the dead clauses are unreachable from both trail and watchlists.
We can remove all data for each such clause, and put their index for
recycling so another new clause can reuse their slot.
Finally we unmark dirty literals and saved-by-trail-explanation
explanation clauses.
2021-07-21 20:29:27 -04:00
Simon Cruanes
a174e5958a
more stats for main
2021-07-21 20:24:27 -04:00
Simon Cruanes
77c61b536e
refactor(sat): rename some bitfields, leaner clause creation
2021-07-21 20:24:03 -04:00
Simon Cruanes
3aa25cb2a2
sat: use an atom array for clauses again
...
allocator is not worth the complexity, and has a lot of double
indirections anyway.
2021-07-21 10:02:56 -04:00
Simon Cruanes
8b94e8404f
wip: data-oriented clauses
2021-07-20 23:34:58 -04:00
Simon Cruanes
97d87cc58f
perf: tiny detail in int indices in solver
2021-07-20 23:34:38 -04:00
Simon Cruanes
a03d7f6bef
fix
2021-07-20 23:31:21 -04:00
Simon Cruanes
89051fd3ad
perf(solver): use VecI32 in the heap
...
this reduces the size of the heap (4 bits per element, not 8), and
reduces GC work by not scanning the bigarray
2021-07-20 10:07:43 -04:00
Simon Cruanes
347e098fc2
misc
2021-07-20 09:20:14 -04:00
Simon Cruanes
f2b2bbb973
some stats for the SAT solver
2021-07-19 21:44:58 -04:00
Simon Cruanes
b624a1ca5d
cleanup: remove commented code
2021-07-19 21:15:16 -04:00
Simon Cruanes
e30cf9fdbf
perf: allocate less in conflict analysis
...
use preallocated vectors
2021-07-19 21:13:00 -04:00
Simon Cruanes
7463bd66aa
fix(sat): sign error
2021-07-19 09:57:02 -04:00
Simon Cruanes
227662f789
detail
2021-07-19 09:57:02 -04:00
Simon Cruanes
7f18e5f29a
fix
2021-07-19 09:57:02 -04:00
Simon Cruanes
47bb521158
wip: refactor SAT solver
2021-07-19 09:57:02 -04:00
Simon Cruanes
b85c47ece1
wip: refactor(sat): use struct-of-array for atom/var
2021-07-19 09:57:02 -04:00
Simon Cruanes
162fd37d9d
wip: refactor
2021-07-19 09:57:02 -04:00
Simon Cruanes
923033f9bf
feat: mli for the SAT solver
2021-07-19 09:17:20 -04:00
Simon Cruanes
15d86d7c62
refactor(sat): use first-class modules instead of records
2021-07-18 19:18:42 -04:00
Simon Cruanes
1aa160fe56
use a pure sat solver for cnf files
2021-07-18 02:46:04 -04:00
Simon Cruanes
4cb8887639
wip: remove all traces of mcsat from src/sat
2021-07-18 02:14:56 -04:00
Simon Cruanes
564dcec252
cleanup msat, rename it sidekick.sat
2021-07-18 01:40:55 -04:00
Simon Cruanes
4a337a85d3
cleanup msat
2021-07-18 01:29:28 -04:00
Simon Cruanes
1a58ab0bfc
vendor current msat in src/sat for further modifications
2021-07-18 01:26:11 -04:00
Simon Cruanes
d024a6a3f0
prepare for vendoring
2021-07-18 01:24:04 -04:00
Simon Cruanes
0266a39b04
fix deprecation warnings related to pervasives
2019-11-29 14:04:33 -06:00
Simon Cruanes
65a8a65095
chore: be robust to deprecations
2019-02-11 16:55:43 +01:00
Simon Cruanes
f62fa88b0f
api: annotate input clauses with theory proofs, too
...
this replaces the old "tag" system
2019-02-11 16:55:43 +01:00
Simon Cruanes
aa47a44242
feat: expose msat.sat as a proper library, with module Int_lit
2019-02-11 16:55:43 +01:00
Simon Cruanes
f3488d68db
test: add regression tests and icnf parser for assumptions
2019-02-11 16:55:43 +01:00
Simon Cruanes
1655d09035
refactor: simpler, cleaner functors
2019-02-11 16:55:43 +01:00
Simon Cruanes
c815ccf648
refactor: use pp instead of print
2019-02-11 16:55:43 +01:00
Simon Cruanes
8b4458b066
refactor(api): make theory state also explicit
2019-02-11 16:55:43 +01:00
Simon Cruanes
e60aff60b6
refactor: simplify vec, remove the need to provide dummy elt
2019-02-11 16:55:43 +01:00
Simon Cruanes
05e2506362
refactor: remove minismt things, make simple msat.sh
2019-02-11 16:55:43 +01:00
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
