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

  • af0635dab7 fix: remove dead code Simon Cruanes 2019-06-10 16:04:01 -05:00
  • 36449d1645 feat(cc): expose a way to access bitfields Simon Cruanes 2019-06-10 15:05:20 -05:00
  • ac99903aec feat: add backtrackable table Simon Cruanes 2019-06-10 14:55:38 -05:00
  • 6c603d5589 refactor: remove code that checks invariants Simon Cruanes 2019-06-10 14:27:41 -05:00
  • b2f6a30cc8 feat: function to add a theory and retain its state Simon Cruanes 2019-06-10 14:16:09 -05:00
  • 128e7dceb8 refactor: move Hash to util/; fix some warnings Simon Cruanes 2019-06-10 10:46:16 -05:00
  • b8fd24ea7b tool: update analyse.py with the minisat-ml version Simon Cruanes 2019-06-10 09:56:32 -05:00
  • b86a6432eb fix(base-term): no dep on zarith necessary for now Simon Cruanes 2019-06-07 18:07:22 -05:00
  • 2f23f41d99 add missing files Simon Cruanes 2019-06-07 18:06:37 -05:00
  • 6176085965 update dev docs Simon Cruanes 2019-06-07 18:05:28 -05:00
  • 70e4c655a2 refactor: split smtlib+bin into their own opam package Simon Cruanes 2019-06-07 17:59:07 -05:00
  • d1aec70cbe fix: restore the module type coercion Simon Cruanes 2019-06-07 17:55:22 -05:00
  • c9d8fd2f51 feat: ensure the congruence closure can propagate literals Simon Cruanes 2019-06-07 17:37:52 -05:00
  • 38f001b0e7 refactor: move Lit inside the solver, as output, not input Simon Cruanes 2019-06-07 17:31:11 -05:00
  • 81e7953261 Merge branch 'wip-refactor' back Simon Cruanes 2019-06-07 16:35:39 -05:00
  • 07d3e22cc1 fix(cc): fix error in initial signature Simon Cruanes 2019-06-07 16:18:38 -05:00
  • 966dfa1724 feat(main): disable check by default Simon Cruanes 2019-06-07 16:18:28 -05:00
  • d2bbc633bd fix: remove debug statement in th-bool Simon Cruanes 2019-06-07 16:18:01 -05:00
  • 8dcb67552e refactor: rewrite production of explanation in CC Simon Cruanes 2019-06-07 15:48:20 -05:00
  • 12ea0c3be4 feat: check propagations if --check is passed Simon Cruanes 2019-06-07 14:58:46 -05:00
  • ef1110925f feat(cc): callback on propagations Simon Cruanes 2019-06-07 14:54:24 -05:00
  • 357dc73426 feat(check): use mini-cc to check CC conflicts on the fly Simon Cruanes 2019-06-07 13:57:12 -05:00
  • 2000114ab4 feat: add more stats Simon Cruanes 2019-06-07 13:27:03 -05:00
  • 8c9590b1e8 fix(tool): update analyse script Simon Cruanes 2019-06-07 13:26:51 -05:00
  • 951be35112 test: fix config for new option format Simon Cruanes 2019-06-07 11:36:45 -05:00
  • 2efa811b3f fix: more precise signature Simon Cruanes 2019-06-07 11:34:06 -05:00
  • e51e996512 test: only run on smt2 files Simon Cruanes 2019-06-07 11:24:04 -05:00
  • e3e964a4c6 fix: first version that seems to work on QF_UF Simon Cruanes 2019-06-07 11:23:53 -05:00
  • a47641ecea feat(main): use --long style for options Simon Cruanes 2019-06-07 11:23:43 -05:00
  • cad49b3747 wip: preprocess/simplify as part of theories Simon Cruanes 2019-06-06 17:13:21 -05:00
  • 19d65b4069 remove dimacs stuff Simon Cruanes 2019-06-06 10:45:09 -05:00
  • b3f328027c wip wip-refactor-old Simon Cruanes 2019-06-05 20:47:58 -05:00
  • 2e7ab9ba9b wip: simplify a lot and only keep th-bool-static in the functor Simon Cruanes 2019-06-05 16:53:13 -05:00
  • 5d86d825f3 feat: remove distinct theory Simon Cruanes 2019-06-05 11:15:54 -05:00
  • 5b989c33ba Set theme jekyll-theme-slate Simon Cruanes 2019-06-05 10:58:36 -05:00
  • fc80d8c6e9 wip: theories Simon Cruanes 2019-06-01 16:56:05 -05:00
  • 44259ec5fc wip: msat solver Simon Cruanes 2019-06-01 16:55:47 -05:00
  • 6ef3da9d02 wip: move Value into the arguments to the Solver Simon Cruanes 2019-06-01 16:55:37 -05:00
  • 5f6ded8566 rename prop to bool Simon Cruanes 2019-06-01 16:55:12 -05:00
  • 080a20480f refactor: continue functorization of sidekick Simon Cruanes 2019-05-27 19:55:21 -05:00
  • e4f20d08c7 wip: refactor: update theories Simon Cruanes 2019-05-27 19:55:02 -05:00
  • 2978821b6e refactor: functorize th-cstor Simon Cruanes 2019-05-27 17:03:16 -05:00
  • 28126eaebd refactor: functorize(th-bool) Simon Cruanes 2019-05-27 17:03:05 -05:00
  • c36092d217 refactor: updated interface for sidekick_core Simon Cruanes 2019-05-27 17:03:25 -05:00
  • 6e9e95c233 wip: functorize everything Simon Cruanes 2019-05-26 23:20:47 -05:00
  • bb0c0d44b2 wip: add core library with signatures for the whole system Simon Cruanes 2019-05-18 18:27:39 -05:00
  • 9c78c6f7bb perf: some basic optimizations Simon Cruanes 2019-05-15 13:02:40 -05:00
  • 6f1fcee828 feat: add Event in util Simon Cruanes 2019-04-26 22:35:37 -05:00
  • 6bd3b2e67b chore: remove all deps on menhir Simon Cruanes 2019-04-04 10:18:22 -05:00
  • f199dd50a6 feat: package for msat-bin, with gzip input Simon Cruanes 2019-04-03 16:55:39 -05:00
  • a35f5719b7 wip: functorize theories wrt some "env" Simon Cruanes 2019-04-02 21:30:28 -05:00
  • ddde590ffd refactor(cc): no micro theories, only callbacks Simon Cruanes 2019-04-02 21:30:14 -05:00
  • 632bec0e66 feat: embed micro theories in theories, fix th-distinct Simon Cruanes 2019-03-22 20:37:30 -05:00
  • 14992f07ec fix: model evaluation must prioritize defined constants' semantics Simon Cruanes 2019-03-22 20:26:06 -05:00
  • 539186bfe6 feat: modular statistics aggregate Simon Cruanes 2019-03-22 20:14:28 -05:00
  • fadf76d944 chore: migrate from sequence to iter Simon Cruanes 2019-03-22 19:43:05 -05:00
  • d58759aa8c fix: integrate negation into CC; map boolean subterms to literals Simon Cruanes 2019-03-22 19:41:05 -05:00
  • 866249deb1 test: add more tests Simon Cruanes 2019-03-14 15:52:02 -05:00
  • 90eedeaf8d chore: use msat 0.8 in opam Simon Cruanes 2019-03-22 18:43:21 -05:00
  • 338a84bf3a chore: use iter, not sequence, in dune Simon Cruanes 2019-03-16 13:54:38 -05:00
  • 9aa4159f2b chore: fix travis Simon Cruanes 2019-03-10 12:11:59 -05:00
  • 47a7142a3c prepare for 0.8 Simon Cruanes 2019-03-10 11:36:01 -05:00
  • fb219fb415 refactor: use iter instead of sequence Simon Cruanes 2019-03-10 11:33:44 -05:00
  • 6e8cedd790 cleanup some files Simon Cruanes 2019-03-10 11:27:37 -05:00
  • d3702d1e1f refactor: fix issues found by @gbury Simon Cruanes 2019-03-01 19:13:24 -06:00
  • 7e9693348a fix: ensure that the mdx test doesn't run too early Simon Cruanes 2019-02-26 19:10:06 -06:00
  • 2aa9b3d4bc refactor: modifications asked by @gbury in review Simon Cruanes 2019-02-26 19:03:47 -06:00
  • 7a050df902 fix readme to account for new sudoku output Simon Cruanes 2019-02-25 13:41:00 -06:00
  • 34f64d2d69 detail: sudoku solver prints total time Simon Cruanes 2019-02-21 17:51:52 -06:00
  • 5bfd975ed3 refactor: move constant parameters outside of the solver Simon Cruanes 2019-02-21 17:50:35 -06:00
  • efe93c3647 feat: Proof.check_empty_conclusion as a separate function Simon Cruanes 2019-02-16 20:41:37 -06:00
  • 591298e296 refactor: remove dimacs backend Simon Cruanes 2019-02-16 19:17:52 -06:00
  • 28afd6eefe fix lazy propagation Simon Cruanes 2019-02-16 19:17:34 -06:00
  • ed64e6b69d chore: try to fix the mdx test; cleanup makefile Simon Cruanes 2019-02-16 17:51:14 -06:00
  • c2a6c2d47b refactor(propagate): make propagation clause lazy Simon Cruanes 2019-02-16 16:58:29 -06:00
  • b1c687faac chore: make default target build, not dev Simon Cruanes 2019-02-16 16:55:59 -06:00
  • 596034d16a fix(dot): proper labelling of hyper-res nodes Simon Cruanes 2019-02-16 12:33:43 -06:00
  • cdb52ee757 fix(proof): unsat conflicts now call Proof.prove_unsat Simon Cruanes 2019-02-16 12:16:41 -06:00
  • 2e2bbfd4d0 fix(proof.check): ensure that the proof is an empty clause Simon Cruanes 2019-02-16 12:16:19 -06:00
  • 92ca9c328f refactor(main): catch resolution errors properly; style Simon Cruanes 2019-02-16 12:16:00 -06:00
  • e30c54e11b refactor: use hyper-res steps in proofs Simon Cruanes 2019-02-15 19:06:39 -06:00
  • b2cec9eaa2 perf: use mutable flags on atoms to perform proof checking Simon Cruanes 2019-02-11 21:16:59 -06:00
  • 7a2f59e9dd feat: add basic theory of constructors Simon Cruanes 2019-03-09 16:51:57 -06:00
  • cb0b5cbcbd refactor: change signature of CC.Theory.on_new_term Simon Cruanes 2019-03-09 16:51:39 -06:00
  • 314bd7f8b2 feat: add ite theory Simon Cruanes 2019-03-09 16:16:21 -06:00
  • 431988d5e4 feat: more expressive theories, also plug distinct in Simon Cruanes 2019-03-09 16:15:24 -06:00
  • 6c1e18dd58 wip: have as_lit be stored in theory data in repr node feat-cc-as-lit-in-th-data Simon Cruanes 2019-03-03 16:59:08 -06:00
  • d4758a2fcf cleanup Simon Cruanes 2019-03-03 16:21:03 -06:00
  • f58bdb5f30 feat: first working version of th-distinct as a separate theory Simon Cruanes 2019-03-03 15:17:06 -06:00
  • 23c0e3c087 wip: new "distinct" theory Simon Cruanes 2019-02-26 22:46:43 -06:00
  • 342dba4533 wip: new micro-theories in CC Simon Cruanes 2019-02-26 22:46:40 -06:00
  • 57147cea85 chore: add common dune file Simon Cruanes 2019-02-26 22:46:13 -06:00
  • c79a5a4798 wip: micro theories Simon Cruanes 2019-02-22 20:57:17 -06:00
  • 77a5475862 wip: cleanup cc Simon Cruanes 2019-02-22 18:54:56 -06:00
  • de1cc952a5 refactor: use new msat lazy propagation Simon Cruanes 2019-02-16 19:09:43 -06:00
  • 3873718174 refactor: require state in Lit.atom, and in Term.abs Simon Cruanes 2019-02-16 17:43:49 -06:00
  • 4d2bddc660 refactor(cc): smaller explanations for congruence-based merges Simon Cruanes 2019-02-16 17:43:04 -06:00
  • 14255f94a7 refactor(cc): remove dead code Simon Cruanes 2019-02-16 15:32:35 -06:00
  • 365aedb138 perf(cc): path compression Simon Cruanes 2019-02-16 15:28:16 -06:00
  • ac030641db refactor(ty): use Hashcons with weak table for types Simon Cruanes 2019-02-16 15:23:57 -06:00