simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-18 00:26:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 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
  • ef3fa2b7a7 use newer quip format, with bool-c taking terms Simon Cruanes 2021-06-09 20:46:23 -04:00
  • 8d05387bc9 use named version of Bool_c Simon Cruanes 2021-06-05 17:42:08 -04:00
  • 01e1bfe6e2 proofs: better sharing, reuse existing definitions when possible Simon Cruanes 2021-05-07 18:32:00 -04:00
  • 7507a7f0b1 proofs: remove with_defs Simon Cruanes 2021-05-07 18:31:51 -04:00
  • e90b3ec76b perf(tef): inlining attrs Simon Cruanes 2021-04-30 18:17:31 -04:00
  • 0242a97327 feat(proof): compress proof by introducing name for shared terms Simon Cruanes 2021-04-27 23:14:17 -04:00
  • 19e6f80b45 refactor(proof): rename defc to stepc Simon Cruanes 2021-04-27 23:14:02 -04:00
  • d195a2fa87 feat(term): util for post-order DAG traversal Simon Cruanes 2021-04-27 23:13:15 -04:00
  • a2c397f1e5 feat(profile): util with2 Simon Cruanes 2021-04-27 23:04:20 -04:00
  • 784c1dceee feat(main): -o to dump proof into a file Simon Cruanes 2021-04-27 23:04:08 -04:00
  • c02da6ce8a feat(proof): progress on preprocessing; proper proofs for th-bool Simon Cruanes 2021-04-26 22:06:58 -04:00
  • 502dce503c refactor(proof): merge proof and lemma, add composite proof constructor Simon Cruanes 2021-04-25 21:56:16 -04:00
  • 22d6786c40 refactor(proof): more and better constructs; compile again Simon Cruanes 2021-04-19 23:39:12 -04:00
  • ff7a87f3fb wip: feat(proof): insert proof constructs in most of sidekick Simon Cruanes 2021-04-15 00:03:15 -04:00
  • 683909c6ef wip: proof printing in sidekick.msat-solver Simon Cruanes 2021-04-10 16:33:49 -04:00
  • 57bf44dfb9 feat: basic proof production for QF_UF (wip) Simon Cruanes 2021-04-04 18:50:23 -04:00
  • dccc4b83eb deploy: fbc3ec7ed6 c-cube 2021-06-11 23:02:23 +00:00
  • fbc3ec7ed6 more docs Simon Cruanes 2021-06-11 19:01:31 -04:00
  • 54f90282b9 deploy: dcbc4d4a59 c-cube 2021-06-11 23:00:26 +00:00
  • dcbc4d4a59 more doc Simon Cruanes 2021-06-11 18:59:26 -04:00
  • 16ab84e1c5 deploy: 4fd8afb129 c-cube 2021-06-11 22:53:57 +00:00
  • 4fd8afb129 more docs; move some code around for a flatter src/ dir structure Simon Cruanes 2021-06-11 18:47:29 -04:00
  • 48edf72ae0 deploy: 96d1ff5775 c-cube 2021-06-10 18:21:15 +00:00
  • 96d1ff5775 more doc Simon Cruanes 2021-06-10 14:20:27 -04:00
  • 9bc52f493b deploy: 8a4747d5d1 c-cube 2021-06-10 17:14:24 +00:00
  • 8a4747d5d1 fix ci for doc gen Simon Cruanes 2021-06-10 13:07:55 -04:00
  • 12ba49ae5f more doc Simon Cruanes 2021-06-10 13:00:00 -04:00
  • e3a8422ab0 udpate CI; bump minimal ocaml to 4.04; add auto-doc Simon Cruanes 2021-06-10 12:57:23 -04:00
  • 5c97c39829 fix test Simon Cruanes 2021-06-10 12:37:46 -04:00
  • 402504b97d run simplex tests only on OCaml >= 4.08 Simon Cruanes 2021-06-10 12:21:26 -04:00
  • afa725825a update CI Simon Cruanes 2021-06-10 12:00:56 -04:00
  • 9c606fbe81 bump minimal ocaml to 4.04 Simon Cruanes 2021-06-10 11:58:50 -04:00
  • 664e084087 update ci, add auto-doc Simon Cruanes 2021-06-10 11:47:20 -04:00