simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1094 commits 53 branches 1 tag 17 MiB
Commit graph

62 commits

Author SHA1 Message Date
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
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
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
683909c6ef wip: proof printing in sidekick.msat-solver 2021-06-11 21:47:54 -04:00
Simon Cruanes
57bf44dfb9 feat: basic proof production for QF_UF (wip) 2021-06-11 21:47:53 -04:00
Simon Cruanes
dcbc4d4a59 more doc 2021-06-11 18:59:26 -04:00
Simon Cruanes
acc4301bec fix build for msat 0.9 2021-03-29 13:30:13 -04:00
Simon Cruanes
481e8e9e58 feat(msat-solver): profiling probe for conflicts 2021-03-29 13:30:13 -04:00
Simon Cruanes
be97938e12 refactor: remove Value, just use terms in the model 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
3d2edc6b3b feat: model_hook type for cooperative model production 2021-03-29 13:30:13 -04:00
Simon Cruanes
3aadb055b6 refactor: make proof production lazy 2021-03-19 17:26:30 -04:00
Simon Cruanes
17702729d5 feat(core): expose a preprocess function 2021-03-18 14:14:06 -04:00
Simon Cruanes
4eeec5487a debug 2021-03-18 12:52:57 -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
fd8b598650 feat: reexport type state 2021-03-17 14:43:46 -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
04615e4e3d Merge branch 'wip-lra-simplex' 2021-02-22 17:13:39 -05:00
Simon Cruanes
a8e2764e92 lra: refactor theory combination (have CC tell us what terms are subterms) 2021-02-22 12:09:44 -05:00
Simon Cruanes
0e5e40f145 feat(core/cc): expose more from the congruence closure 2021-02-22 12:09:44 -05:00
Simon Cruanes
3979380896 feat(profile): add instant probe 2020-12-22 16:45:55 -05:00
Simon Cruanes
fafb001934 feat: add profiling system based on TEF 
- a `Sidekick_util.Profile` module, deps-free
- an optional sidekick.tef library that needs unix+mtime
 2020-12-22 16:27:45 -05:00
Simon Cruanes
9839e5a36b feat(core): add push_decision, for model-based th combination 2020-11-17 18:23:16 -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
51be2f52e8 style 2020-10-12 02:06:16 -04:00
Simon Cruanes
c67e44e654 detail 2020-10-09 23:59:38 -04:00
Simon Cruanes
ae6d298790 move to containers 3.0 2020-09-08 22:33:24 -04:00
Simon Cruanes
bb449257d8 fix(solver): in final-check, fixpoint until CC has no merges 2020-02-15 14:40:57 -06:00
Simon Cruanes
11d8f8e879 remove dead code, some printing info 2020-02-15 14:33:44 -06:00
Simon Cruanes
ef60d1466f feat: better debug message 2020-01-14 21:23:02 -06:00
Simon Cruanes
e58b29da02 fix(term): hashconsing error leading to non termination 2019-12-28 08:49:14 -06:00
Simon Cruanes
721b1874b7 fix: re-check CC after calling on-final-check 2019-11-01 17:04:36 -05:00
Simon Cruanes
d4c3d3e443 cleanup: remove a few functions 2019-11-01 14:17:28 -05:00
Simon Cruanes
9ddce6a186 feat(check-cc): add statistics 2019-10-30 13:31:04 -05:00
Simon Cruanes
7d8589accd refactor: change the functor stack 2019-10-29 15:06:19 -05:00
Simon Cruanes
1658887ea3 feat: basic production of models 2019-10-02 18:44:02 -05:00
Simon Cruanes
7552808c33 feat: add is_valid_literal filter to add_term_rec 2019-10-02 18:16:51 -05:00
Alexander Bentkamp
7fe6f07c0b split on_merge into two events: pre and post merge 2019-08-21 11:43:59 -05:00
Simon Cruanes
769b80030a feat: progress bar in solver 2019-07-31 04:36:32 -05:00
Simon Cruanes
af0635dab7 fix: remove dead code 2019-06-10 16:04:01 -05:00
Simon Cruanes
6c603d5589 refactor: remove code that checks invariants 2019-06-10 14:28:05 -05:00
Simon Cruanes
b2f6a30cc8 feat: function to add a theory and retain its state 2019-06-10 14:16:09 -05:00