sidekick

simon/sidekick

Fork 0

mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 17:04:39 -04:00

Commit graph

a205c429e7 feat(sat): check proofs if asked to Simon Cruanes 2021-08-02 23:13:18 -04:00
2d081c554b chore: fix makefile Simon Cruanes 2021-08-02 21:34:37 -04:00
2a2b03ffc8 remove symlinks Simon Cruanes 2021-07-30 11:34:58 -04:00
74f2844652 wip: DRUP checker Simon Cruanes 2021-07-23 00:08:52 -04:00
a08cda8c5b test: add a lot more tests (for SAT) Simon Cruanes 2021-07-22 23:31:55 -04:00
c14070b622 perf: compile in release by default 😡 wip-dod-sat Simon Cruanes 2021-08-02 16:04:59 -04:00
62f45777a1 feat(sat): implement phase saving in the SAT solver wip-sat-phase-saving-2021-07-22 Simon Cruanes 2021-07-22 09:58:04 -04:00
515a720d00 detail Simon Cruanes 2021-07-22 09:57:53 -04:00
233df98229 perf(sat): proper GC for clauses Simon Cruanes 2021-07-21 20:24:33 -04:00
a174e5958a more stats for main Simon Cruanes 2021-07-21 20:24:27 -04:00
77c61b536e refactor(sat): rename some bitfields, leaner clause creation Simon Cruanes 2021-07-21 20:24:03 -04:00
3aa25cb2a2 sat: use an atom array for clauses again Simon Cruanes 2021-07-21 10:02:56 -04:00
8b94e8404f wip: data-oriented clauses Simon Cruanes 2021-07-20 23:34:58 -04:00
97d87cc58f perf: tiny detail in int indices in solver Simon Cruanes 2021-07-20 23:34:38 -04:00
29892d07de feat(util): Vec_float based on bigarrays Simon Cruanes 2021-07-20 23:33:37 -04:00
a03d7f6bef fix Simon Cruanes 2021-07-20 23:30:51 -04:00
11b1ea4eda feat(vec): more Simon Cruanes 2021-07-20 23:28:18 -04:00
d53b3c291e feat: add "drup" case to proofs Simon Cruanes 2021-07-20 23:27:11 -04:00
89051fd3ad perf(solver): use VecI32 in the heap Simon Cruanes 2021-07-20 10:07:43 -04:00
d08d5fe9c4 feat(util): add VecI32 based on bigarray Simon Cruanes 2021-07-20 10:07:29 -04:00
347e098fc2 misc Simon Cruanes 2021-07-19 23:09:34 -04:00
674a619ca7 deploy: eb23644195 c-cube 2021-07-20 04:52:29 +00:00
eb23644195 fix ci for gh-pages Simon Cruanes 2021-07-20 00:46:16 -04:00
6f7f2b2823 fix doc Simon Cruanes 2021-07-20 00:35:49 -04:00
f2b2bbb973 some stats for the SAT solver Simon Cruanes 2021-07-19 21:44:58 -04:00
b624a1ca5d cleanup: remove commented code Simon Cruanes 2021-07-19 21:15:16 -04:00
e30cf9fdbf perf: allocate less in conflict analysis Simon Cruanes 2021-07-19 21:13:00 -04:00
7463bd66aa fix(sat): sign error Simon Cruanes 2021-07-19 09:45:34 -04:00
227662f789 detail Simon Cruanes 2021-07-19 09:23:32 -04:00
7f18e5f29a fix Simon Cruanes 2021-07-19 00:27:20 -04:00
47bb521158 wip: refactor SAT solver Simon Cruanes 2021-07-19 00:23:17 -04:00
b85c47ece1 wip: refactor(sat): use struct-of-array for atom/var Simon Cruanes 2021-07-18 22:28:02 -04:00
162fd37d9d wip: refactor Simon Cruanes 2021-07-18 20:49:15 -04:00
2107b3de7e feat(util): a Bitvec module, refactor testing Simon Cruanes 2021-07-18 20:48:28 -04:00
97aab34e46 statistics for pure sat solver Simon Cruanes 2021-07-19 09:56:51 -04:00
923033f9bf feat: mli for the SAT solver Simon Cruanes 2021-07-18 22:27:54 -04:00
cab541e712 Merge branch 'wip-vendored-msat' Simon Cruanes 2021-07-18 20:50:18 -04:00
15d86d7c62 refactor(sat): use first-class modules instead of records wip-vendored-msat Simon Cruanes 2021-07-18 19:18:42 -04:00
041e83139d feat: make mtime optional with dummy "tef" backend Simon Cruanes 2021-07-18 10:31:03 -04:00
c7bf4b01e7 feat: optional memtrace support Simon Cruanes 2021-07-18 10:17:44 -04:00
ff5cf1239c chore: CI on PRs Simon Cruanes 2021-07-18 09:29:55 -04:00
5faa1d6ef7 chore: try to build again Simon Cruanes 2021-07-18 08:04:56 -04:00
1aa160fe56 use a pure sat solver for cnf files Simon Cruanes 2021-07-18 02:46:04 -04:00
4cb8887639 wip: remove all traces of mcsat from src/sat Simon Cruanes 2021-07-18 02:01:19 -04:00
564dcec252 cleanup msat, rename it sidekick.sat Simon Cruanes 2021-07-18 01:40:55 -04:00
4a337a85d3 cleanup msat Simon Cruanes 2021-07-18 01:29:28 -04:00
1a58ab0bfc vendor current msat in src/sat for further modifications Simon Cruanes 2021-07-18 01:26:11 -04:00
d024a6a3f0 prepare for vendoring Simon Cruanes 2021-07-18 01:07:31 -04:00
98f246db4c fix test wip-self-contained-proofs Simon Cruanes 2021-07-18 01:04:15 -04:00
77e3c15ad7 normalize proofs Simon Cruanes 2021-07-18 00:11:56 -04:00
ed11741122 feat(proof): add self-contained mode Simon Cruanes 2021-07-11 22:10:54 -04:00
ca4f22baca wip Simon Cruanes 2021-07-11 21:07:51 -04:00
1fd226183e wip: add small SMT solver for the guide wip-doc-small-solver Simon Cruanes 2021-07-07 22:21:52 -04:00
1c2b37eb72 details Simon Cruanes 2021-07-04 22:48:55 -04:00
ceb0b09426 chore: disable CI on mac OS for now Simon Cruanes 2021-07-04 18:39:07 -04:00
2f353cfd94 add stat to count number of acyclicity conflicts in datatypes Simon Cruanes 2021-07-04 17:42:55 -04:00
75fde183f9 add some datatype acyclicity benchs + a generator Simon Cruanes 2021-07-04 17:17:33 -04:00
653783744c fix tets Simon Cruanes 2021-07-04 01:36:28 -04:00
b41a23e427 deploy: 0368a29ada c-cube 2021-07-04 05:30:10 +00:00
0368a29ada add helper in base Simon Cruanes 2021-07-04 01:29:23 -04:00
9b43630990 update guide Simon Cruanes 2021-07-04 01:29:13 -04:00
57e2290151 try to fix CI for mdx Simon Cruanes 2021-07-04 00:30:03 -04:00
c561f6ae70 doc: update readme Simon Cruanes 2021-07-04 00:27:31 -04:00
70d59f82a6 deploy: 71360ad1f8 c-cube 2021-07-04 04:27:03 +00:00
71360ad1f8 refactor: change signature of field access in CC Simon Cruanes 2021-07-04 00:25:59 -04:00
961ff2bb63 deploy: 51ac678ccd c-cube 2021-07-04 04:07:53 +00:00
51ac678ccd trivial helper Simon Cruanes 2021-07-04 00:06:42 -04:00
a2b27a5dc2 doc: more on guide Simon Cruanes 2021-07-04 00:05:25 -04:00
5bdd079b55 deploy: 29bff98da6 c-cube 2021-07-04 04:01:42 +00:00
29bff98da6 chore: fix opam Simon Cruanes 2021-07-04 00:00:48 -04:00
4e07e6039a add helpers for LRA in base Simon Cruanes 2021-07-03 23:49:14 -04:00
ec9a770d76 doc: update readme Simon Cruanes 2021-07-03 23:41:18 -04:00
72043f6135 deploy: c05d870b2c c-cube 2021-07-04 03:40:43 +00:00
c05d870b2c doc: start guide, with ocaml-mdx to ensure it stays up to date Simon Cruanes 2021-07-03 23:39:37 -04:00
9cfaecec99 helpers Simon Cruanes 2021-07-03 23:39:20 -04:00
aebaaf56af deploy: 6578ea9136 c-cube 2021-07-04 02:50:03 +00:00
6578ea9136 move form to sidekick_base; rename {Term,Ty}.state into store Simon Cruanes 2021-07-03 22:48:44 -04:00
80b50e8744 refactor: add solver instance in sidekick base Simon Cruanes 2021-07-03 22:28:57 -04:00
8167a40579 deploy: be46f40312 c-cube 2021-07-04 01:47:36 +00:00
be46f40312 more docs Simon Cruanes 2021-07-03 21:46:39 -04:00
86ac475398 deploy: 4c05bd0759 c-cube 2021-07-04 01:39:46 +00:00
4c05bd0759 fix opam file Simon Cruanes 2021-07-03 21:38:30 -04:00
590f1ef887 more cleanup, add doc Simon Cruanes 2021-07-03 21:13:32 -04:00
79bc3def3f refactor to get sidekick-base library Simon Cruanes 2021-07-03 20:20:19 -04:00
813f645a9c refactor: rename sidekick-base-term to sidekick-base Simon Cruanes 2021-07-03 17:42:19 -04:00
d491fd5580 doc: add a short summary to readme Simon Cruanes 2021-06-28 21:48:54 -04:00
3131b5fb51 deploy: 655ea76a6a c-cube 2021-06-29 01:41:24 +00:00
655ea76a6a fix(proof): sharing of terms must define them in order Simon Cruanes 2021-06-17 21:59:34 -04:00
952740f66f add test case to mini-cc Simon Cruanes 2021-06-16 20:10:26 -04:00
a223b6cd5c fix(cc): fix bad proof production for the merge-bool-parent case Simon Cruanes 2021-06-16 19:58:42 -04:00
941fe92125 callbacks for conflict/decisions/new-atoms Simon Cruanes 2021-06-15 21:17:25 -04:00
e979b88148 add IArray.iteri2 Simon Cruanes 2021-06-15 20:54:43 -04:00
252f7243a4 feat(proof): add binary res/res1 Simon Cruanes 2021-06-15 20:54:27 -04:00
e32d949dd3 refactor CC a bit Simon Cruanes 2021-06-14 20:01:42 -04:00
fad57a7ee0 update index Simon Cruanes 2021-06-11 22:25:09 -04:00
0042f50db2 try to fix ci again Simon Cruanes 2021-06-11 22:06:27 -04:00
899ea67188 post-rebase fix Simon Cruanes 2021-06-11 21:55:44 -04:00
6a9dbb8440 pick proof format with env variable Simon Cruanes 2021-06-11 10:25:40 -04:00
2eee760e29 refactor(proof): new serialization; faster implem Simon Cruanes 2021-06-10 22:20:54 -04:00
19e083c682 produce nn steps Simon Cruanes 2021-06-09 21:13:04 -04:00