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
Simon Cruanes
6d7edbb601
fix(CC/monoid): in monoid, store N.t, not a term.
...
make sure the sub-elements of the monoid are represented in the
congruence closure before-hand.
2021-03-29 13:30:13 -04:00
Simon Cruanes
9e0c79f597
feat: basic model production for th-data
2021-03-29 13:30:13 -04:00
Simon Cruanes
b6713fb833
refactor: rename some hooks; prepare for model generation in th-data
2021-03-29 13:30:13 -04:00
Simon Cruanes
b35ca4496f
fix(data): bad explanations in on-new-term rules
2021-03-18 12:53:06 -04:00
Simon Cruanes
45893e92f1
fix: missing preprocessing in LRA; better theory combination
2021-02-22 14:01:55 -05:00
Simon Cruanes
ae6d298790
move to containers 3.0
2020-09-08 22:33:24 -04:00
Simon Cruanes
7cfdb3507c
fix(th-data): fix acyclicity
2020-02-20 19:32:33 -06:00
Simon Cruanes
11d8f8e879
remove dead code, some printing info
2020-02-15 14:33:44 -06:00
Simon Cruanes
b2c047190f
fix(data): check is-a lits in final-check
2020-01-17 19:12:06 -06:00
Simon Cruanes
eb64acb31f
fix(data): reimplement acyclicity check
2020-01-17 19:10:46 -06:00
Simon Cruanes
e21dea4780
feat(cc): flag some explanations as being theory-induced
2020-01-17 18:49:14 -06:00
Simon Cruanes
a31b2b36ef
fixes: add missing expl in monoids; handle is-c t
2020-01-14 22:41:33 -06:00
Simon Cruanes
10b9febe9d
fix(th-data): avoid redundant explanations
2019-12-28 09:00:59 -06:00
Simon Cruanes
6f67593be1
feat(data): fixes (decide args of is-a/select; rearrange reduction rules)
2019-12-28 08:31:52 -06:00
Simon Cruanes
91e9b6cc2c
feat: initial support for is-a/select
2019-12-28 07:08:23 -06:00
Simon Cruanes
6aafaad48f
feat(data): store is-a/select parents in a monoid
2019-12-28 06:15:50 -06:00
Simon Cruanes
9293553925
feat(th-data): first draft of acyclicity
2019-12-28 05:19:01 -06:00
Simon Cruanes
6061b5843e
fix(th-data): fix merge explanation in cstor monoid
2019-12-28 05:19:01 -06:00
Simon Cruanes
a4e3fd5a69
feat: provide simple repr->monoid mapping in core
2019-12-28 05:17:47 -06:00
