Simon Cruanes
90f100d9b1
helpers to build terms and solvers
2022-08-27 20:24:28 -04:00
Simon Cruanes
28173c1852
feat(term): replace E_app_uncurried with E_app_fold
2022-08-25 20:50:56 -04:00
Simon Cruanes
9762968373
feat(bool): use lists for B_and/B_or, along with App_uncurried
2022-08-22 22:12:27 -04:00
Simon Cruanes
dd66efb772
feat(term): add App_uncurried constructor
...
sometimes currying is really costly. For example, in boolean formulas,
the formula `/\_i=1^100 a_i` has 100 atoms as subterms, but if
represented curried with binary `/\` it also has 98 intermediate
conjunctions as subterms. With how the rest of sidekick works, this
means each of these gets its own atom and CNF; instead we're going to
use App_uncurried.
2022-08-22 22:12:27 -04:00
Simon Cruanes
dff65c5d26
refactor: Term.abs takes store again, so abs false can be false,true
2022-08-22 22:12:26 -04:00
Simon Cruanes
310d2183c4
add Lit.Tbl,Lit.Set,Lit.Map
2022-08-16 21:29:45 -04:00
Simon Cruanes
d5b7c2b0ee
feat(printer): always put (), do not box applications
2022-08-16 21:27:09 -04:00
Simon Cruanes
23e70a192a
perf(cc): more inlining; remove dead code
2022-08-14 22:33:32 -04:00
Simon Cruanes
593b693caf
refactor lit a bit
2022-08-12 23:09:56 -04:00
Simon Cruanes
b73c1bf464
feat(bool): use binary symbols for boolean operators
...
this helps in simplifying only fully applied boolean operators, and
avoiding simplifying the binary function `(or)` to `(false)`
2022-08-10 22:41:53 -04:00
Simon Cruanes
b9c0265cb9
feat(core): add Gensym module, add Proof_trace.close
2022-08-10 22:07:30 -04:00
Simon Cruanes
95beb2bf27
core: add better printer
2022-08-08 21:49:47 -04:00
Simon Cruanes
7aa113f379
feat(core): make CC_view part of the core library; with default CC view
2022-08-08 21:17:37 -04:00
Simon Cruanes
c2af589282
add core.bool_view
2022-08-07 22:40:39 -04:00
Simon Cruanes
4aec4fe491
refactor(proofs): make proof terms a recursive term
2022-08-01 20:42:45 -04:00
Simon Cruanes
1edf054104
refactor(proof): use a suspension but keep uniform Proof_term.data type
...
this makes proof terms uniformly printable or (de)serializable.
2022-07-31 15:01:11 -04:00
Simon Cruanes
1ecb189fd5
refactor: core and CC
2022-07-30 21:17:20 -04:00
Simon Cruanes
7595f66e59
refactor(core): add Proof_step
2022-07-29 23:27:04 -04:00
Simon Cruanes
1905d2d628
feat(core): improve Lit
2022-07-29 00:02:06 -04:00
Simon Cruanes
9df981d650
feat(core): concrete lit, proof traces, proof terms
2022-07-28 23:30:56 -04:00
Simon Cruanes
f3f0628261
large refactor with signature splitting, events, etc.
2022-07-18 23:20:07 -04:00
Simon Cruanes
633a658e0c
wip: use new sigs
2022-07-15 23:51:53 -04:00
Simon Cruanes
00dec7ced8
remove iarray
2022-07-15 21:06:46 -04:00
Simon Cruanes
5a559bec92
remove veci32
2022-07-15 20:32:06 -04:00
Simon Cruanes
a1bc186d2e
use ocamlformat
2022-07-14 22:09:13 -04:00
Simon Cruanes
1946a5e7cf
feat: construct model from congruence closure after th-combination
...
we already obtain a model from theories, and saturate the congruence
closure with it, it's a shame not to use it.
2022-02-18 14:59:27 -05:00
Simon Cruanes
a388c96fe3
cc: remove new_merges
2022-02-18 14:59:27 -05:00
Simon Cruanes
6e941683a2
add with_model_mode to congruence closure
...
this mode:
- enables `set_mode_value`
- disables all callbacks
- can only be used locally with a push/pop wrapper
2022-02-18 14:59:26 -05:00
Simon Cruanes
95f84b4854
refactor(th-comb): provide full model to the CC
...
this way it can fail on merges of classes assigned conflicting value.
2022-02-18 14:59:26 -05:00
Simon Cruanes
fd66039c8d
wip: theory combination by exposing model (classes) directly to CC
2022-02-18 14:59:26 -05:00
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
