simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-26 11:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1486 commits 53 branches 1 tag 17 MiB
Commit graph

45 commits

Author SHA1 Message Date
Simon Cruanes
0abe4b7020
wip: decode more proof steps to quip 2021-10-27 21:50:28 -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
fa04cb7997
refactor(th-bool): remove cache and most recursion 
the preprocessing framework already takes care of both.
 2021-08-22 15:50:42 -04:00
Simon Cruanes
9aee35c6ce
fix other issue in th-bool preprocessing 2021-08-22 01:31:59 -04:00
Simon Cruanes
27796da5a8
fix preprocessing in th-bool 2021-08-22 01:29:01 -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
d40ce304ae wip: refactor proofs into traces 2021-08-17 09:29:46 -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
590f1ef887 more cleanup, add doc 2021-07-03 21:14:17 -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
8d05387bc9 use named version of Bool_c 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
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
dcbc4d4a59 more doc 2021-06-11 18:59:26 -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
7bf6b18bc0 basic renaming 2021-03-22 12:15:36 -04:00
Simon Cruanes
d665f83c65 add assertion 2021-03-19 12:43:38 -04:00
Simon Cruanes
ffc45b0db6 fix: do not preemptively simplify imply 2021-03-18 18:20:39 -04:00
Simon Cruanes
9fea7462dc feat(th-bool): more direct encoding of => 2021-03-18 18:04:20 -04:00
Simon Cruanes
380efa816f debug msg 2021-03-18 13:37:55 -04:00
Simon Cruanes
2312da883c feat(bool): also provide xor/neq 2021-03-18 13:06:44 -04:00
Simon Cruanes
07ca5546f5 refator(preproc): remove explicit recursion, but rewrite top-down 
give a chance to simplifiers to rewrite before we rewrite subterms.
 2021-03-18 12:19:30 -04:00
Simon Cruanes
0d31d9d84e refactor(th-bool): parametrize bool_view by type of lists 
use iterator instead of a IArray.t on the view side
 2021-03-17 18:29:39 -04:00
Simon Cruanes
0aa13ca808 refactor: provide a state for Ty.bool in core signature 2021-02-24 15:52:54 -05:00
Simon Cruanes
9a3e387405 refactor: explicit recursion in preprocessing 
if a preprocessor fires, it's up to it to preprocess subterms. rewriting
is now from the root, not the leaves on.

Use that in LRA to rewrite under linear expressions.
 2020-11-12 18:21:37 -05:00
Simon Cruanes
b332e8ceb0 fix: preprocess away "ite" 2020-01-14 20:23:23 -06:00
Simon Cruanes
3cd79ee4c9 refactor(th_bool): cache tseitin on absolute values 2019-11-01 15:53:12 -05:00
Simon Cruanes
7d8589accd refactor: change the functor stack 2019-10-29 15:06:19 -05:00
Simon Cruanes
0031c64ea9 feat(th-bool-static): check for new terms in the CC in final check 2019-10-08 09:08:05 -05:00
Simon Cruanes
49a7446631 feat(th-bool-static): add non-traversable opaque boolean term 2019-10-05 18:37:49 -05:00
Simon Cruanes
d527b2b945 fix: remove some module aliases for 4.08 2019-07-31 03:25:04 -05:00
Simon Cruanes
38f001b0e7 refactor: move Lit inside the solver, as output, not input 2019-06-07 17:31:11 -05:00
Simon Cruanes
d2bbc633bd fix: remove debug statement in th-bool 2019-06-07 16:18:01 -05:00
Simon Cruanes
e3e964a4c6 fix: first version that seems to work on QF_UF 2019-06-07 11:23:53 -05:00
Simon Cruanes
cad49b3747 wip: preprocess/simplify as part of theories 2019-06-06 17:13:21 -05:00
Simon Cruanes
2e7ab9ba9b wip: simplify a lot and only keep th-bool-static in the functor 2019-06-05 16:53:13 -05:00