simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-12 22:10:53 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1303 commits 53 branches 1 tag 17 MiB
Commit graph

92 commits

Author SHA1 Message Date
Simon Cruanes
7f18e5f29a fix 2021-07-19 09:57:02 -04:00
Simon Cruanes
47bb521158 wip: refactor SAT solver 2021-07-19 09:57:02 -04:00
Simon Cruanes
b85c47ece1 wip: refactor(sat): use struct-of-array for atom/var 2021-07-19 09:57:02 -04:00
Simon Cruanes
162fd37d9d wip: refactor 2021-07-19 09:57:02 -04:00
Simon Cruanes
923033f9bf feat: mli for the SAT solver 2021-07-19 09:17:20 -04:00
Simon Cruanes
15d86d7c62 refactor(sat): use first-class modules instead of records 2021-07-18 19:18:42 -04:00
Simon Cruanes
1aa160fe56 use a pure sat solver for cnf files 2021-07-18 02:46:04 -04:00
Simon Cruanes
4cb8887639 wip: remove all traces of mcsat from src/sat 2021-07-18 02:14:56 -04:00
Simon Cruanes
564dcec252 cleanup msat, rename it sidekick.sat 2021-07-18 01:40:55 -04:00
Simon Cruanes
4a337a85d3 cleanup msat 2021-07-18 01:29:28 -04:00
Simon Cruanes
1a58ab0bfc vendor current msat in src/sat for further modifications 2021-07-18 01:26:11 -04:00
Simon Cruanes
d024a6a3f0 prepare for vendoring 2021-07-18 01:24:04 -04:00
Simon Cruanes
0266a39b04 fix deprecation warnings related to pervasives 2019-11-29 14:04:33 -06:00
Simon Cruanes
65a8a65095 chore: be robust to deprecations 2019-02-11 16:55:43 +01:00
Simon Cruanes
f62fa88b0f api: annotate input clauses with theory proofs, too 
this replaces the old "tag" system
 2019-02-11 16:55:43 +01:00
Simon Cruanes
aa47a44242 feat: expose msat.sat as a proper library, with module Int_lit 2019-02-11 16:55:43 +01:00
Simon Cruanes
f3488d68db test: add regression tests and icnf parser for assumptions 2019-02-11 16:55:43 +01:00
Simon Cruanes
1655d09035 refactor: simpler, cleaner functors 2019-02-11 16:55:43 +01:00
Simon Cruanes
c815ccf648 refactor: use pp instead of print 2019-02-11 16:55:43 +01:00
Simon Cruanes
8b4458b066 refactor(api): make theory state also explicit 2019-02-11 16:55:43 +01:00
Simon Cruanes
e60aff60b6 refactor: simplify vec, remove the need to provide dummy elt 2019-02-11 16:55:43 +01:00
Simon Cruanes
05e2506362 refactor: remove minismt things, make simple msat.sh 2019-02-11 16:55:43 +01:00
Simon Cruanes
2fb51d8082 chore: move to dune 2019-02-11 16:55:43 +01:00
Simon Cruanes
b2e646343a do not expose St in solver, but only expose a restricted API. 2019-02-11 16:55:43 +01:00
Simon Cruanes
ef7333af6d make state explicit and add type t state-wrapper in most modules 2019-02-11 16:55:43 +01:00
Simon Cruanes
eff8ed1c4f split some features into minismt lib 2019-02-11 16:55:43 +01:00
Simon Cruanes
cbe3750b0d use generative functors, remove a layer of nesting for SMT libs 2019-02-11 16:55:43 +01:00
Simon Cruanes
2707215aa2 move tseitin transformation into its own lib 2019-02-11 16:55:43 +01:00
Simon Cruanes
768f59f88b big refactoring 
- move to jbuilder
- use a functorial heap (with indices embedded in lit/var)
- update Vec with optims from mc2
- change semantics of Vec.shrink
- use new Log module
 2019-02-11 16:55:43 +01:00
Simon Cruanes
27d1841f6b wip: migrate to msat 0.8 2019-01-28 21:09:57 -06:00
Simon Cruanes
4fadbeb04d chore: migrate to dune 2019-01-18 18:37:26 -06:00
Simon Cruanes
73c7db2b4e feat(cc): boolean propagation of literals in CC 2018-08-18 19:56:22 -05:00
Simon Cruanes
c1a662e2c8 refactor(sat): improve style of theory propagation handler 2018-08-18 19:55:30 -05:00
Simon Cruanes
324c9d2e36 fix(sat): allow proofs with unary resolution history 
can happen if the conflict clause is a theory lemma
 2018-08-18 19:54:46 -05:00
Simon Cruanes
dd58fa21ef fix(sat): fix bug in restarts, we need to solve again after one 2018-08-18 18:08:42 -05:00
Simon Cruanes
ca531d73a6 refactor(cc): fix bugs, use list of nodes in equiv class 2018-08-18 18:06:16 -05:00
Simon Cruanes
c2d79b2e6a fix(main): properly handle option no-restarts 2018-08-18 18:05:22 -05:00
Simon Cruanes
e6a96df0d9 chore: remove dead code in sat 2018-08-18 17:47:20 -05:00
Simon Cruanes
72750b9e1a fix(sat): bugfix about adding clauses with true lits 2018-08-18 17:47:04 -05:00
Simon Cruanes
46ff8c3ba6 fix(sat): bug with re-internalization of terms upon backtracking 2018-08-18 17:20:20 -05:00
Simon Cruanes
b8445d0ca3 refactor: introduce check_invariants in CC 
costly, but helps find bugs
 2018-08-18 14:52:44 -05:00
Simon Cruanes
bf0b5185bd fix: proper proof for clause deduplication 2018-07-10 13:54:02 -05:00
Simon Cruanes
b7518a632a refactor(cc): simplify congruence closure 2018-06-27 21:38:16 -05:00
Simon Cruanes
c125fdafa6 fix(sat): use Conflict exn to signal conflict on add_clause 2018-06-22 21:01:22 -05:00
Simon Cruanes
9ac274fc09 refactor: simplify literals; remove useless casts in CC; bit for pending nodes 2018-06-22 19:38:04 -05:00
Simon Cruanes
6933a7b5d0 refactor: add reset_tasks function to clear caches on backtrack 
also refactor CC a bit
 2018-06-16 22:50:03 -05:00
Simon Cruanes
5e380464ce fix(sat): base-level = 1 under assumptions 2018-06-11 21:47:37 -05:00
Simon Cruanes
080cde778e feat(model): proper model construction for CC + fun interpretation 2018-06-11 21:42:02 -05:00
Simon Cruanes
10d394a9c3 fix(cc): public add function must also saturate CC 2018-05-28 01:22:58 -05:00
Simon Cruanes
0b42a34a20 refactor: cleanup SAT 2018-05-25 21:33:38 -05:00