Simon Cruanes
c9138144f3
refactor(preprocess): break infinite recursion
2022-09-08 21:55:09 -04:00
Simon Cruanes
317f406620
wip: refactor(preprocess): recursive preprocess guided by theories
2022-09-07 19:35:09 -04:00
Simon Cruanes
e74439cf2a
wip: new attempt at theory combination
2022-09-01 22:34:27 -04:00
Simon Cruanes
5feb5d8e73
refactor: new API for combination, with theories claiming terms
...
interface variables are terms claimed by >= 2 theories. Theories now
have a unique ID attributed at their creation.
2022-08-27 22:51:16 -04:00
Simon Cruanes
4d78be0c52
wip: model builder
2022-08-25 20:13:49 -04:00
Simon Cruanes
6ad07921c4
details
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
3e39232696
fix build temporarily
2022-08-19 21:34:21 -04:00
Simon Cruanes
4d97f1a525
fix build
2022-08-19 21:32:55 -04:00
Simon Cruanes
5fa5fb5bd7
fix(th-data): need to propagate from is-a eagerly
...
the final check is too late: we need the info from `is_a c t` to be
fully propagated in the CC before we can run the acyclicity check.
2022-08-19 21:31:27 -04:00
Simon Cruanes
c643e547f6
wip: refactor(th-data): remove some model building, cleanup code
2022-08-19 00:08:57 -04:00
Simon Cruanes
94ba945bf3
feat(cc.plugin): plugins have state, passed at init
2022-08-14 23:21:49 -04:00
Simon Cruanes
647d66a196
feat(th-data): use lists, not iter/array; add Proof_rules
2022-08-10 22:07:54 -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
0d0751b7d2
refactor(theories): remove functors
2022-07-30 23:02:13 -04:00
Simon Cruanes
2922cca78f
fix: proper negation when raising an acyclicity conflict
2022-07-22 21:54:22 -04:00
Simon Cruanes
851dda696a
feat(cc): have 2 phases of pre-merge events
...
the first phase observes plugin data unchanged; the second one
is used to update plugin data themselves. This fix a bug that manifests
itself depending on implementation details of Event, where some theory's
event handler fires too late and observes a state that has already
changed.
2022-07-22 21:31:42 -04:00
Simon Cruanes
6da6284711
refactor(cc): use explicit actions in CC, not effectful functions
2022-07-22 21:26:21 -04:00
Simon Cruanes
b10aaf05f2
wip: expose bug caused by order of event handlers
...
if plugin data is updated before `Th_data.on_pre_merge` is called, it
never has a chance to observe the un-merged data and react accordingly.
we need to ensure that all handlers see the same data before any change
is made.
2022-07-20 21:40:04 -04:00
Simon Cruanes
f3f0628261
large refactor with signature splitting, events, etc.
2022-07-18 23:20:07 -04:00
Simon Cruanes
00dec7ced8
remove iarray
2022-07-15 21:06:46 -04:00
Simon Cruanes
a1bc186d2e
use ocamlformat
2022-07-14 22:09:13 -04:00
Simon Cruanes
d153c80ca5
details
2022-02-18 14:59:27 -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
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
44c63d4c13
debug
2021-12-17 16:40:52 -05:00
Simon Cruanes
f9f471ce12
details
2021-12-17 13:46:48 -05:00
Simon Cruanes
2d24a21908
fix: do not preprocess but add equations eagerly for single-cstor terms
2021-12-17 11:58:39 -05:00
Simon Cruanes
6d72203437
fix: avoid preprocessing loops
2021-12-17 11:48:41 -05:00
Simon Cruanes
0841bddbaf
feat(data): preprocessing step for single-cstor types
...
if t:ty where ty has exactly one constructor `c`, we replace
t at preprocessing by `c(sel-c-0(t), … sel-c-n(t))`
2021-12-17 11:39:25 -05:00
Simon Cruanes
63eeb81290
refactor: modify interface of Th_data
2021-12-17 11:39:22 -05:00
Simon Cruanes
fd1d068997
proof stubs and sat proof
2021-10-12 22:13:28 -04:00
Simon Cruanes
af901f54b1
proof production for th-data
2021-10-11 19:57:25 -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
73b39fe075
fix more warnings
2021-08-27 21:34:26 -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
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
2f353cfd94
add stat to count number of acyclicity conflicts in datatypes
2021-07-04 18:02:48 -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
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
fbc3ec7ed6
more docs
2021-06-11 19:01:31 -04:00
Simon Cruanes
dcbc4d4a59
more doc
2021-06-11 18:59:26 -04:00
Simon Cruanes
7b2b11486f
dbg
2021-05-03 10:36:04 -04:00
Simon Cruanes
8558719cc8
remove debug
2021-03-29 13:30:13 -04:00
Simon Cruanes
8aa851608a
fix(data): use a cstor equality rather than is-a for model completion
2021-03-29 13:30:13 -04:00
Simon Cruanes
111fe8c1b9
wip
2021-03-29 13:30:13 -04:00
Simon Cruanes
65fda4de41
feat(th-data): completion of models by picking a base-cstor
2021-03-29 13:30:13 -04:00
