simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 17:04:39 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 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
  • a89f031fa0 get rid of travis Simon Cruanes 2021-06-08 10:40:15 -04:00
  • 9380622096 small refactor Simon Cruanes 2021-05-03 10:35:55 -04:00
  • 7b2b11486f dbg Simon Cruanes 2021-03-30 16:00:36 -04:00
  • 84898c404a
         Add files via upload woollybear917 2021-04-17 23:15:51 -04:00
  • 994755caf6
         Add files via upload AmazoneyBobuxey 2021-04-17 11:05:52 -04:00
  • 903243643f perf(hash): use FNV hashing Simon Cruanes 2021-04-04 17:45:36 -04:00
  • 18fbb950bc feat(CC): change cc_view so that App_ho is curried Simon Cruanes 2021-04-01 22:28:46 -04:00
  • bc9206d8fa dbg wip-model-production Simon Cruanes 2021-03-30 16:00:36 -04:00
  • 8558719cc8 remove debug Simon Cruanes 2021-03-29 12:59:24 -04:00
  • 4170224a37 add tests/dune to ignore test directories for dune Simon Cruanes 2021-03-24 12:40:40 -04:00
  • 5427618dab gitignore Simon Cruanes 2021-03-24 12:40:23 -04:00
  • 8aa851608a fix(data): use a cstor equality rather than is-a for model completion Simon Cruanes 2021-03-24 12:36:14 -04:00
  • 111fe8c1b9 wip Simon Cruanes 2021-03-24 12:27:52 -04:00
  • acc4301bec fix build for msat 0.9 Simon Cruanes 2021-03-24 12:13:48 -04:00
  • 65fda4de41 feat(th-data): completion of models by picking a base-cstor Simon Cruanes 2021-03-24 12:07:40 -04:00
  • 481e8e9e58 feat(msat-solver): profiling probe for conflicts Simon Cruanes 2021-03-24 12:07:11 -04:00
  • f893f14f21 feat(profile): enabled function Simon Cruanes 2021-03-24 12:06:53 -04:00
  • ff77617a5d fix(monoid): call find on sub-nodes Simon Cruanes 2021-03-22 14:09:31 -04:00
  • 6d7edbb601 fix(CC/monoid): in monoid, store N.t, not a term. Simon Cruanes 2021-03-22 13:06:44 -04:00
  • 9e0c79f597 feat: basic model production for th-data Simon Cruanes 2021-03-22 12:58:05 -04:00
  • be97938e12 refactor: remove Value, just use terms in the model Simon Cruanes 2021-03-22 12:53:38 -04:00
  • b6713fb833 refactor: rename some hooks; prepare for model generation in th-data Simon Cruanes 2021-03-22 12:35:00 -04:00
  • 3d2edc6b3b feat: model_hook type for cooperative model production Simon Cruanes 2021-03-19 18:55:06 -04:00
  • 367c1945ef feat(main): handle check-sat-assuming statement Simon Cruanes 2021-03-24 15:30:01 -04:00
  • b6ea55e7ab merge opam fix from opam-repo Simon Cruanes 2021-03-24 15:18:52 -04:00
  • 457aa15729 prepare for 0.9.1 Simon Cruanes 2021-03-24 13:53:20 -04:00
  • db042f7b88 fix: termination issue when using add_decision_lit Simon Cruanes 2021-03-24 11:28:02 -04:00
  • a64202c6ec feat: add on_conflict callback Simon Cruanes 2021-03-23 15:28:34 -04:00
  • 3fedca069d wip: perf(lra): implement basic propagations wip-lra-simplex-propagations Simon Cruanes 2021-02-22 14:28:44 -05:00
  • 7bf6b18bc0 basic renaming Simon Cruanes 2021-03-20 23:55:31 -04:00
  • 3aadb055b6 refactor: make proof production lazy Simon Cruanes 2021-03-19 17:26:30 -04:00
  • d665f83c65 add assertion Simon Cruanes 2021-03-19 12:43:38 -04:00
  • ffc45b0db6 fix: do not preemptively simplify imply Simon Cruanes 2021-03-18 18:20:39 -04:00
  • 9fea7462dc feat(th-bool): more direct encoding of => Simon Cruanes 2021-03-18 18:04:20 -04:00
  • 0b351ea67e test: add regression test for bad LRA preprocessing Simon Cruanes 2021-03-18 14:14:24 -04:00
  • 17702729d5 feat(core): expose a preprocess function Simon Cruanes 2021-03-18 14:14:06 -04:00
  • 945ee577c0 tool: add ddSMT drivers and short readme Simon Cruanes 2021-03-18 13:44:53 -04:00
  • 380efa816f debug msg Simon Cruanes 2021-03-18 13:27:21 -04:00
  • 2312da883c feat(bool): also provide xor/neq Simon Cruanes 2021-03-18 11:52:19 -04:00
  • 0a14d556d9 style Simon Cruanes 2021-03-18 11:42:51 -04:00
  • b35ca4496f fix(data): bad explanations in on-new-term rules Simon Cruanes 2021-03-18 12:53:06 -04:00
  • 4eeec5487a debug Simon Cruanes 2021-03-18 12:52:57 -04:00
  • 791290118b fix(form): make eval rule more precise Simon Cruanes 2021-03-18 12:26:14 -04:00
  • 07ca5546f5 refator(preproc): remove explicit recursion, but rewrite top-down Simon Cruanes 2021-03-18 12:19:30 -04:00
  • 3693861008 debug msg Simon Cruanes 2021-03-18 12:13:39 -04:00
  • 0d31d9d84e refactor(th-bool): parametrize bool_view by type of lists Simon Cruanes 2021-03-17 18:29:39 -04:00
  • 5f9675e7d1 feat: expose Atom.neg Simon Cruanes 2021-03-17 15:01:39 -04:00
  • fd8b598650 feat: reexport type state Simon Cruanes 2021-03-17 14:43:46 -04:00
  • 0aa13ca808 refactor: provide a state for Ty.bool in core signature Simon Cruanes 2021-02-24 15:52:54 -05:00
  • 2d2bbf6a23 try to fix ci Simon Cruanes 2021-02-24 15:09:50 -05:00
  • b23f19b783 fix opam Simon Cruanes 2021-02-24 14:39:03 -05:00
  • d26732271a fix opam version Simon Cruanes 2021-02-24 14:37:51 -05:00
  • 2810312e2f add simplify to LRA Simon Cruanes 2021-02-22 21:10:18 -05:00
  • 15cadbaeaa Merge branch 'wip-lra-simplex' Simon Cruanes 2021-02-22 17:17:27 -05:00
  • 04615e4e3d Merge branch 'wip-lra-simplex' Simon Cruanes 2021-02-22 17:13:39 -05:00
  • a5166fb19b more stats wip-lra-simplex Simon Cruanes 2021-02-22 16:45:21 -05:00
  • d6aa1071d7 test: add more regression files Simon Cruanes 2021-02-22 14:30:43 -05:00
  • 4d0c24f40f refactor lra Simon Cruanes 2021-02-22 14:28:31 -05:00
  • 45893e92f1 fix: missing preprocessing in LRA; better theory combination Simon Cruanes 2021-02-22 14:01:55 -05:00
  • a8e2764e92 lra: refactor theory combination (have CC tell us what terms are subterms) Simon Cruanes 2021-02-22 12:04:52 -05:00
  • a7afce3af4 fix(lra): only do theory combination on terms known to the CC Simon Cruanes 2021-02-16 18:35:21 -05:00
  • 0e5e40f145 feat(core/cc): expose more from the congruence closure Simon Cruanes 2021-02-16 18:35:07 -05:00
  • aa20605567 feat(lra): expose some stats Simon Cruanes 2021-02-16 19:18:45 -05:00
  • e2d3afb4df chore: add zarith lower bound in opam Simon Cruanes 2021-02-16 19:06:01 -05:00
  • 6df35161b0 typo Simon Cruanes 2021-02-16 18:06:38 -05:00
  • d7119d50ff chore: indicate dep on mtime for sidekick Simon Cruanes 2021-02-16 16:03:01 -05:00
  • 341d82fa7f add test for certificates Simon Cruanes 2021-02-16 15:18:38 -05:00