sidekick

simon/sidekick

Fork 0

mirror of https://github.com/c-cube/sidekick.git synced 2025-12-16 23:56:53 -05:00

Commit graph

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
1655d09035 refactor: simpler, cleaner functors Simon Cruanes 2019-01-18 22:38:15 -06:00
c4da650e45 perf: use release profile in msat.sh Simon Cruanes 2019-01-18 22:38:03 -06:00
1b6ff0e849 chore: update travis Simon Cruanes 2019-01-18 20:34:17 -06:00
c815ccf648 refactor: use pp instead of print Simon Cruanes 2019-01-18 20:24:39 -06:00
7e9fd1a363 perf: remove bitfield, implement it manually Simon Cruanes 2019-01-18 20:19:23 -06:00
8b4458b066 refactor(api): make theory state also explicit Simon Cruanes 2019-01-18 20:14:47 -06:00
e60aff60b6 refactor: simplify vec, remove the need to provide dummy elt Simon Cruanes 2019-01-18 19:59:23 -06:00
b3fc070d09 style: remove old headers Simon Cruanes 2019-01-18 19:42:41 -06:00
05e2506362 refactor: remove minismt things, make simple msat.sh Simon Cruanes 2019-01-18 19:39:12 -06:00
5846ae7e17 chore: finish moving to dune Simon Cruanes 2019-01-18 18:18:36 -06:00
9d729b2136 chore: move to opam 2 Simon Cruanes 2019-01-18 18:05:01 -06:00
2fb51d8082 chore: move to dune Simon Cruanes 2019-01-18 18:01:09 -06:00
cba9f9592d fix: update .travis.yml Simon Cruanes 2018-05-30 20:02:37 -05:00
6eeb649cdc doc Simon Cruanes 2018-01-03 22:08:55 +01:00
27cbb981e7 more controled API for Res Simon Cruanes 2018-01-03 22:07:40 +01:00
83d3048648 a bit of doc Simon Cruanes 2018-01-03 22:01:12 +01:00
f5066a2ff3 typo Simon Cruanes 2017-12-29 22:10:01 +01:00
6762985d18 expose {push,pop} in main solver Simon Cruanes 2017-12-29 21:29:43 +01:00
241e2fa4d7 remove useless functions Simon Cruanes 2017-12-29 19:12:17 +01:00
87fc9aef26 reinstate better way of picking watch literals Simon Cruanes 2017-12-29 19:00:32 +01:00
5279456419 reset some record accesses, for perf Simon Cruanes 2017-12-29 18:53:26 +01:00
585bf6bd50 detail Simon Cruanes 2017-12-29 18:35:27 +01:00
b2e646343a do not expose St in solver, but only expose a restricted API. Simon Cruanes 2017-12-29 18:29:56 +01:00
a612a1cda2 make Solver.t more lightweight by removing some useless fields Simon Cruanes 2017-12-29 17:29:24 +01:00
a34c191ddc add optional size argument to create functions Simon Cruanes 2017-12-29 17:24:09 +01:00
ef7333af6d make state explicit and add type t state-wrapper in most modules Simon Cruanes 2017-12-29 16:48:26 +01:00
eff3f8024f wip: use submodules of Solver_types to clean up code Simon Cruanes 2017-12-29 15:29:04 +01:00
8eef2deebd faster addition of clauses' watch literals Simon Cruanes 2017-12-29 12:32:27 +01:00
8550102ea6 dependencies in opam files; put binary in minismt package Simon Cruanes 2017-12-28 19:47:05 +01:00
eff8ed1c4f split some features into minismt lib Simon Cruanes 2017-12-28 19:43:54 +01:00
9bc85160b8 restrict what Msat core lib exposes, provide shortcuts Simon Cruanes 2017-12-28 19:23:36 +01:00
cbe3750b0d use generative functors, remove a layer of nesting for SMT libs Simon Cruanes 2017-12-28 19:12:41 +01:00
797e1b86fe makefile Simon Cruanes 2017-12-28 19:12:32 +01:00