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

  • 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
  • 3b671aa7a4 refactor(term): use hashconsing with a weak table Simon Cruanes 2019-02-16 15:08:49 -06:00
  • 1ef0cf4183 refactor: small cleanup in terms Simon Cruanes 2019-02-16 14:58:13 -06:00
  • a14fe25ba0 chore: add tools, update gitignore Simon Cruanes 2019-02-16 14:50:34 -06:00
  • e878907f4b refactor(bool): bool-view of terms, functorized theory Simon Cruanes 2019-02-16 14:49:00 -06:00
  • 1f68753121 refactor: remove proof printing code Simon Cruanes 2019-02-16 13:38:54 -06:00
  • c06e4025fa perf(bag): remove constant-time size Simon Cruanes 2019-02-16 13:38:43 -06:00
  • c39431315f fix: fix test on dune 1.7 Simon Cruanes 2019-02-15 17:50:10 -06:00
  • eea95346eb fix: remove dead aliases Simon Cruanes 2019-02-13 08:52:54 -06:00
  • 7f05da56cc fix: cache E_unsat in direct add_clause functions Simon Cruanes 2019-02-11 08:50:12 -06:00
  • 4127db2153 Revert "fix: catch E_unsat in assume, if one adds an empty clause" Simon Cruanes 2019-02-11 08:44:15 -06:00
  • 7673bddf82 fix: catch E_unsat in assume, if one adds an empty clause Simon Cruanes 2019-02-10 18:03:11 -06:00
  • ea98f6f027 refactor: return an array from conflict analysis Simon Cruanes 2019-02-10 16:58:49 -06:00
  • 110eda2f05 feat: re-export exn Simon Cruanes 2019-02-10 16:58:41 -06:00
  • 96c4d83781 detail: add debug message Simon Cruanes 2019-02-09 21:43:57 -06:00
  • 8ad78b2acd refactor: a bit of cleanup for mcsat Simon Cruanes 2019-02-09 17:12:33 -06:00
  • 7583e78bd2 fix(propagate): insert propagated literal itself Simon Cruanes 2019-02-09 17:10:39 -06:00
  • 1ccc292d79 refactor: move Backtrackable_ref into its own sub-library Simon Cruanes 2019-02-06 22:01:33 -06:00
  • 8d012d2f49 refactor: fix problems from review Simon Cruanes 2019-02-04 20:35:28 -06:00
  • ffa769c48c doc: add a section and test on the sudoku solver Simon Cruanes 2019-02-02 21:22:27 -06:00
  • 1632c1a619 doc: check something in the readme Simon Cruanes 2019-02-02 19:28:12 -06:00
  • c376f1d763 fix: msat.tseitin depends on msat Simon Cruanes 2019-02-02 19:10:17 -06:00
  • 75476b8dd7 test: use mdx to ensure the readme code snippets compile Simon Cruanes 2019-02-02 18:55:05 -06:00
  • 7891f2b69e refactor: cleaner choice of which vector to add a clause to Simon Cruanes 2019-02-01 21:59:24 -06:00
  • ba4c360cbd fix: when simplifying, copy flags properly Simon Cruanes 2019-02-01 21:53:04 -06:00
  • d089db3e4d feat: expose printers Simon Cruanes 2019-02-01 19:46:58 -06:00
  • 6dbaa2d335 feat: expose eval_atom Simon Cruanes 2019-02-01 19:44:02 -06:00
  • c89a99e82b rename log-proof to store-proof Simon Cruanes 2019-02-01 19:16:38 -06:00
  • ebd8ad7110 refactor: rename flag clause.{learnt,removable} Simon Cruanes 2019-02-01 19:09:22 -06:00
  • da24541fa0 feat: allow optional disabling of proof logging Simon Cruanes 2019-02-01 19:05:53 -06:00
  • 65a8a65095 chore: be robust to deprecations Simon Cruanes 2019-01-30 15:44:56 -06:00
  • f62fa88b0f api: annotate input clauses with theory proofs, too Simon Cruanes 2019-01-28 19:21:14 -06:00
  • 79bd88b999 api: remove spurious () for calls to solve Simon Cruanes 2019-01-28 19:02:32 -06:00
  • 1736b4a99e api: sat_state takes formulas, not atoms Simon Cruanes 2019-01-28 19:00:10 -06:00
  • a58c940c6d feat: ask less from values in mcsat Simon Cruanes 2019-01-26 13:07:46 -06:00
  • 4fbaae7d2d refactor(log): use a S-expr-style format for log messages Simon Cruanes 2019-01-26 12:57:50 -06:00
  • 0a3a3b576a refactor: remove dead code, some basic simplifications Simon Cruanes 2019-01-26 12:57:33 -06:00
  • fdc042aee3 fix: no need to add trivial clauses at all Simon Cruanes 2019-01-26 12:51:58 -06:00
  • 83c0d0e7f1 feat: add Value.t to the mcsat interface Simon Cruanes 2019-01-26 12:36:07 -06:00
  • 95bdc80ed5 feat: rename slice to acts, add some functions in it Simon Cruanes 2019-01-26 12:00:04 -06:00
  • 872d4433db feat: add a "backtrackable ref" module Simon Cruanes 2019-01-26 11:30:11 -06:00
  • 8f1c24c1a6 refactor: change API to {final,partial}_check Simon Cruanes 2019-01-26 11:23:45 -06:00
  • a0ba576b0f test: details in sudoku solver Simon Cruanes 2019-01-25 22:29:06 -06:00
  • ecf1de42b5 chore(opam): require sequence Simon Cruanes 2019-01-25 22:21:00 -06:00
  • a6d74898ff test: add another check to the sudoku solver Simon Cruanes 2019-01-25 22:15:04 -06:00
  • 1c188afb6b test: refactor a bit so that benchs are run by dune Simon Cruanes 2019-01-25 22:07:34 -06:00
  • 9a8f0e9d82 test: add small sudoku solver to test the CDCL(T) interface Simon Cruanes 2019-01-25 22:02:06 -06:00
  • ced266663e refactor: change backtracking API (push/pop_levels) Simon Cruanes 2019-01-25 22:01:50 -06:00
  • f26f74e119 fix: bugfix in construction of slices in SAT/theory interface Simon Cruanes 2019-01-25 22:01:17 -06:00
  • 5e1508ff2b refactor: use a vec for the new clauses Simon Cruanes 2019-01-25 22:00:35 -06:00
  • 14319f959f refactor: a bit of cleanup in analyze Simon Cruanes 2019-01-25 20:05:56 -06:00
  • a5ec88f2a7 refactor: use Var.mark and a pre-allocated vec for analyze Simon Cruanes 2019-01-25 19:27:25 -06:00
  • cf6147c500 details Simon Cruanes 2019-01-25 17:53:14 -06:00
  • 9024b0f0a9 refactor: change theory API to be simpler and more imperative Simon Cruanes 2019-01-23 08:36:07 -06:00
  • 53dd3acd4e chore: improve test infra Simon Cruanes 2019-01-22 20:51:16 -06:00
  • 74956e2e87 fix(proof): fix proof production for unsat cores Simon Cruanes 2019-01-22 20:48:11 -06:00
  • 8f29aa8005 refactor: small cleanup Simon Cruanes 2019-01-22 20:26:55 -06:00
  • ca62db00e1 perf: garbage collect clauses (only for clauses with ≥3 lits) Simon Cruanes 2019-01-22 20:17:37 -06:00
  • 3c940ed4f6 refactor(core): use bitfield in clauses, use Vec.iter more Simon Cruanes 2019-01-22 20:17:00 -06:00
  • 0d7ae34880 fix(analyze-final): mistake in production of unsat cores Simon Cruanes 2019-01-19 18:13:41 -06:00
  • f8281bfcc2 test: check unsat cores in icnf-solve Simon Cruanes 2019-01-19 18:13:29 -06:00
  • 52ae127a5d refactor: implement analyze_final to compute unsat cores Simon Cruanes 2019-01-19 15:57:27 -06:00
  • 4ca441fa38 fix(core): cancel-until 0 before solving Simon Cruanes 2019-01-19 15:57:18 -06:00
  • a88752759f feat: expose simple script for icnf-solve Simon Cruanes 2019-01-19 15:56:54 -06:00
  • aa47a44242 feat: expose msat.sat as a proper library, with module Int_lit Simon Cruanes 2019-01-19 15:56:36 -06:00
  • 1136416a7c wip: remove push/pop Simon Cruanes 2019-01-18 23:30:01 -06:00
  • f3488d68db test: add regression tests and icnf parser for assumptions Simon Cruanes 2019-01-19 15:01:09 -06:00
  • df9538a91e perf: exit early from propagation loop in case of conflict Simon Cruanes 2019-01-18 23:27:54 -06:00