Simon Cruanes
a81a21c341
core: add n_levels to monoid
2022-02-08 13:13:00 -05:00
Simon Cruanes
cbc9c5ac6f
refactor(smt): preprocessing is now using a queue of delayed actions
...
- preprocessing doesn't simplify anymore, it assumes terms are already
simplified. It only adds clauses/adds literals, it does not return
new terms.
- adding clauses/literals to SAT is done as delayed actions, to avoid
issues of reentrancy.
These actions are performed after preprocessing, in a loop that has
access to the SAT solver.
2022-02-04 16:08:01 -05:00
Simon Cruanes
a98132ed0c
feat(model): add theory hooks to "complete" models
...
these hooks are allowed to add terms to the model, that are not in the
congruence closure (for example in LRA, terms that were preprocessed
away).
2022-02-03 14:00:43 -05:00
Simon Cruanes
3fdb07b533
feat: handle get-model/get-value from smtlib inputs
2022-02-02 15:51:44 -05:00
Simon Cruanes
f7195bf980
feat(smt): ability for a theory to declare we're in incomplete fragment
2022-01-11 14:00:04 -05:00
Simon Cruanes
af8ab338e6
feat(smt): add a registry to share values between theories
2022-01-11 14:00:04 -05:00
Simon Cruanes
63f50d03fa
feat: proper proof production for theory merges in CC
...
this involves resolution steps between the lemma (typically a kind of
horn clause with the merge as conclusion) and a bunch of literals
responsible for some equational hypotheses of this horn clause, being true
2021-12-29 15:56:54 -05:00
Simon Cruanes
80cb096e8a
feat: change signature of explanations for CC theory merges
2021-12-28 23:07:27 -05:00
Simon Cruanes
584b56075f
feat: add push/pop for assumptions; add check_sat_propagation_only
...
this gives the user the possibility of controlling search by mostly
using assumptions (and the underlying assumption stack) as well as
boolean+theory propagation. The result is **not** complete, but can
still help as a beefed-up contextual simplifier.
2021-12-20 15:34:34 -05:00
Simon Cruanes
5d2f8a1d3d
feat(api): add callbacks to measure progress or ask solver to stop
2021-12-20 13:51:59 -05:00
Simon Cruanes
3b409c8944
feat(proof): add proof_r1 as a pendant to proof_p1 for non-equations
2021-12-17 11:38:07 -05:00
Simon Cruanes
2e4fd5e1c1
update conflict resolution for better proofs, improve code
2021-11-27 15:30:45 -05:00
Simon Cruanes
0abe4b7020
wip: decode more proof steps to quip
2021-10-27 21:50:28 -04:00
Simon Cruanes
3589592296
wip: use real proofs
2021-10-16 22:00:29 -04:00
Simon Cruanes
fd1d068997
proof stubs and sat proof
2021-10-12 22:13:28 -04:00
Simon Cruanes
1779b7115a
wip: proof production (incl. better tracking of proofs in CC)
2021-10-11 14:27:14 -04:00
Simon Cruanes
0550f6fcfa
wip: proof production
2021-10-09 00:51:15 -04:00
Simon Cruanes
d3537f2c3f
wip: refactor proof
2021-10-07 20:49:39 -04:00
Simon Cruanes
bbb995b0d5
refactor some names related to proofs; wip add unit paramod
2021-10-03 20:32:37 -04:00
Simon Cruanes
4621cc948f
feat(core): change the way proofs work
...
Now a proof returns a `step_id` which identifies its resulting clause.
This might be a dummy value when proofs are disabled.
We attach a step_id to each new clause to make sure it's properly
tracked, but step_ids might outlive their clause (and the actual proof
data might be on disk, only keeping in ram a small unique identifier).
2021-09-29 22:16:22 -04:00
Simon Cruanes
16bb65ebfa
wip: clause pools
2021-08-31 09:30:28 -04:00
Simon Cruanes
e7e8873295
fix more warnings
2021-08-27 09:28:59 -04:00
Simon Cruanes
e93e084eac
refactor: eager proofs; stronger preprocessing
...
proofs are now directly emitted (almost) everywhere, which simplifies
a lot of things. preprocessing is more recursive (a bit too much
really).
2021-08-22 01:13:41 -04:00
Simon Cruanes
1ab7d34a7d
refactor: make it compile again
2021-08-20 18:18:30 -04:00
Simon Cruanes
9f01b98cde
wip: imperative proofs
...
- getting closer to having the SMT solver compile again
- dummy proof implementation
- DRUP proof implementation for pure SAT solver
2021-08-18 23:59:39 -04:00
Simon Cruanes
7bead748a6
refactor: move SAT_PROOF into sidekick.core
...
SAT proofs are part of bigger proofs, now. And we expect them to work on
the literals of CDCL(T) directly, bypassing the low level boolean atoms
2021-08-17 23:59:02 -04:00
Simon Cruanes
d40ce304ae
wip: refactor proofs into traces
2021-08-17 09:29:46 -04:00
Simon Cruanes
27e775ee04
wip: refactor proofs for SMT
2021-08-12 22:05:49 -04:00
Simon Cruanes
d53b3c291e
feat: add "drup" case to proofs
2021-07-20 23:27:11 -04:00
Simon Cruanes
47bb521158
wip: refactor SAT solver
2021-07-19 09:57:02 -04:00
Simon Cruanes
162fd37d9d
wip: refactor
2021-07-19 09:57:02 -04:00
Simon Cruanes
71360ad1f8
refactor: change signature of field access in CC
2021-07-04 00:25:59 -04:00
Simon Cruanes
9cfaecec99
helpers
2021-07-03 23:39:20 -04:00
Simon Cruanes
6578ea9136
move form to sidekick_base; rename {Term,Ty}.state into store
2021-07-03 22:48:44 -04:00
Simon Cruanes
be46f40312
more docs
2021-07-03 21:46:39 -04:00
Simon Cruanes
590f1ef887
more cleanup, add doc
2021-07-03 21:14:17 -04:00
Simon Cruanes
a223b6cd5c
fix(cc): fix bad proof production for the merge-bool-parent case
2021-06-16 19:58:42 -04:00
Simon Cruanes
252f7243a4
feat(proof): add binary res/res1
2021-06-15 20:54:27 -04:00
Simon Cruanes
899ea67188
post-rebase fix
2021-06-11 21:55:44 -04:00
Simon Cruanes
2eee760e29
refactor(proof): new serialization; faster implem
2021-06-11 21:53:13 -04:00
Simon Cruanes
19e083c682
produce nn steps
2021-06-11 21:53:13 -04:00
Simon Cruanes
ef3fa2b7a7
use newer quip format, with bool-c taking terms
2021-06-11 21:53:13 -04:00
Simon Cruanes
7507a7f0b1
proofs: remove with_defs
2021-06-11 21:53:13 -04:00
Simon Cruanes
19e6f80b45
refactor(proof): rename defc to stepc
2021-06-11 21:53:13 -04:00
Simon Cruanes
c02da6ce8a
feat(proof): progress on preprocessing; proper proofs for th-bool
2021-06-11 21:53:12 -04:00
Simon Cruanes
502dce503c
refactor(proof): merge proof and lemma, add composite proof constructor
2021-06-11 21:51:53 -04:00
Simon Cruanes
22d6786c40
refactor(proof): more and better constructs; compile again
2021-06-11 21:51:15 -04:00
Simon Cruanes
ff7a87f3fb
wip: feat(proof): insert proof constructs in most of sidekick
2021-06-11 21:50:25 -04:00
Simon Cruanes
57bf44dfb9
feat: basic proof production for QF_UF (wip)
2021-06-11 21:47:53 -04:00
Simon Cruanes
4fd8afb129
more docs; move some code around for a flatter src/ dir structure
2021-06-11 18:47:29 -04:00
