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

1067 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
e90b3ec76b perf(tef): inlining attrs 2021-06-11 21:53:13 -04:00
Simon Cruanes
0242a97327 feat(proof): compress proof by introducing name for shared 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
d195a2fa87 feat(term): util for post-order DAG traversal 2021-06-11 21:53:13 -04:00
Simon Cruanes
a2c397f1e5 feat(profile): util with2 2021-06-11 21:53:13 -04:00
Simon Cruanes
784c1dceee feat(main): -o to dump proof into a file 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
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
4fd8afb129 more docs; move some code around for a flatter src/ dir structure 2021-06-11 18:47:29 -04:00
Simon Cruanes
96d1ff5775 more doc 2021-06-10 14:20:27 -04:00
Simon Cruanes
8a4747d5d1 fix ci for doc gen 2021-06-10 13:07:55 -04:00
Simon Cruanes
12ba49ae5f more doc 2021-06-10 13:00:00 -04:00
Simon Cruanes
e3a8422ab0 udpate CI; bump minimal ocaml to 4.04; add auto-doc 
run simplex tests only on OCaml >= 4.08
 2021-06-10 12:57:23 -04:00
Simon Cruanes
a89f031fa0 get rid of travis 2021-06-08 10:40:15 -04:00
Simon Cruanes
9380622096 small refactor 2021-05-03 10:36:04 -04:00
Simon Cruanes
7b2b11486f dbg 2021-05-03 10:36:04 -04:00
Simon Cruanes
903243643f perf(hash): use FNV hashing 2021-04-04 17:45:36 -04:00
Simon Cruanes
18fbb950bc feat(CC): change cc_view so that App_ho is curried 2021-04-01 22:28:46 -04:00
Simon Cruanes
8558719cc8 remove debug 2021-03-29 13:30:13 -04:00
Simon Cruanes
4170224a37 add tests/dune to ignore test directories for dune 2021-03-29 13:30:13 -04:00
Simon Cruanes
5427618dab gitignore 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
acc4301bec fix build for msat 0.9 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
481e8e9e58 feat(msat-solver): profiling probe for conflicts 2021-03-29 13:30:13 -04:00
Simon Cruanes
f893f14f21 feat(profile): enabled function 2021-03-29 13:30:13 -04:00
Simon Cruanes
ff77617a5d fix(monoid): call find on sub-nodes 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
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
367c1945ef feat(main): handle check-sat-assuming statement 2021-03-24 15:31:49 -04:00
Simon Cruanes
3fedca069d wip: perf(lra): implement basic propagations 2021-03-22 12:15:36 -04:00
Simon Cruanes
7bf6b18bc0 basic renaming 2021-03-22 12:15:36 -04:00
Simon Cruanes
3aadb055b6 refactor: make proof production lazy 2021-03-19 17:26:30 -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
0b351ea67e test: add regression test for bad LRA preprocessing 2021-03-18 14:14:24 -04:00
Simon Cruanes
17702729d5 feat(core): expose a preprocess function 2021-03-18 14:14:06 -04:00
Simon Cruanes
945ee577c0 tool: add ddSMT drivers and short readme 2021-03-18 13:44:53 -04:00
Simon Cruanes
380efa816f debug msg 2021-03-18 13:37:55 -04:00