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

Commit graph

  • 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
  • 0bd2770b40 feat(lra): certificate checking for simplex2 Simon Cruanes 2021-02-16 15:18:19 -05:00
  • 284a475197 lra is not optional Simon Cruanes 2021-02-16 14:00:59 -05:00
  • cfbd352ca0 feat(lra): restore theory combination; improve preprocessing Simon Cruanes 2021-02-16 13:25:21 -05:00
  • e5338b91ba chore: faster CI hopefully Simon Cruanes 2021-02-15 17:30:48 -05:00
  • 0634e7c356 perf(lra): only call simplex.check if new things were asserted Simon Cruanes 2021-02-15 17:09:38 -05:00
  • 2a6c224f08 fix(lra): proper negation for basic operators Simon Cruanes 2021-02-15 16:53:57 -05:00
  • acf99504c4 test: option to display stats Simon Cruanes 2021-02-15 16:53:46 -05:00
  • 69b2fde084 fix(simplex2): add basic var's bound in the certificate Simon Cruanes 2021-02-15 16:35:54 -05:00
  • 0081926a50 fix(lra): refactor Simon Cruanes 2021-02-15 16:35:41 -05:00
  • a908f2b3f2 feat(arith): integrate simplex2 into sidekick; remove old simplex Simon Cruanes 2021-02-15 16:19:13 -05:00
  • d6f0fa0ffc feat(simplex2): build proper certificates Simon Cruanes 2021-02-15 16:18:40 -05:00
  • f0dd1b08e8 details Simon Cruanes 2021-02-15 13:54:35 -05:00
  • aea634ca8b test: add a test of the backtracking behavior of simplex2 Simon Cruanes 2021-02-15 13:46:25 -05:00
  • 0aa04480ce test: improve simplex2 tests Simon Cruanes 2021-02-15 13:29:33 -05:00
  • 4d9f99e65d fix(simplex2): correct pivot; refactor; better printing Simon Cruanes 2021-02-15 13:29:12 -05:00
  • f226c6b820 fix(lra): many fixes in simplex; some fixme/todo Simon Cruanes 2021-02-12 19:42:16 -05:00
  • 5fc8d746c2 test: add tests for simplex2 Simon Cruanes 2021-02-12 19:42:07 -05:00
  • fb52e79287 test: update test harness Simon Cruanes 2021-02-12 19:41:34 -05:00
  • dd4719b1a4 wip(LRA): new simplex implementation Simon Cruanes 2021-02-12 15:48:02 -05:00
  • 2a0e14a635 refactor: a bit of cleanup Simon Cruanes 2021-02-11 17:17:55 -05:00
  • 75ce199bb0 wip: new simplex Simon Cruanes 2021-02-11 17:17:43 -05:00
  • 3d46315b82 try to fix ci Simon Cruanes 2021-02-05 14:25:38 -05:00
  • dc80c1de1a perf(simplex): optim: no new variable for constraints like a·x <= b Simon Cruanes 2021-02-05 14:16:34 -05:00
  • 14a25f95a8 perf: make simplex more imperative Simon Cruanes 2021-02-05 13:48:57 -05:00
  • dee47743f7
         Merge pull request #6 from c-cube/wip-lra-simplex-unsat-core Simon Cruanes 2021-02-04 10:47:50 -05:00
  • 8b06566013 fix tests the most stupid way possible Simon Cruanes 2020-12-29 10:36:18 -05:00
  • d5b4798e20 try to fix test Simon Cruanes 2020-12-23 16:12:50 -05:00
  • b9b1b685d1 chore: update msat Simon Cruanes 2020-12-23 16:00:16 -05:00
  • 14e07f7a8a prepare for 0.9 Simon Cruanes 2020-12-23 14:22:06 -05:00
  • a3e618a4fe
         Merge pull request #22 from Gbury/feat-th-decisions Simon Cruanes 2020-12-23 14:05:26 -05:00
  • d3103c5355
         Merge pull request #24 from Gbury/feat-lit-pol Simon Cruanes 2020-12-23 14:05:17 -05:00
  • 3979380896 feat(profile): add instant probe Simon Cruanes 2020-12-22 16:45:55 -05:00
  • fafb001934 feat: add profiling system based on TEF Simon Cruanes 2020-12-22 16:27:45 -05:00