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

59 commits

Author SHA1 Message Date
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
79bd88b999 api: remove spurious () for calls to solve 2019-02-11 16:55:43 +01:00
Simon Cruanes
1c188afb6b test: refactor a bit so that benchs are run by dune 2019-02-11 16:55:43 +01:00
Simon Cruanes
9a8f0e9d82 test: add small sudoku solver to test the CDCL(T) interface 2019-02-11 16:55:43 +01:00
Simon Cruanes
5e1508ff2b refactor: use a vec for the new clauses 2019-02-11 16:55:43 +01:00
Simon Cruanes
53dd3acd4e chore: improve test infra 2019-02-11 16:55:43 +01:00
Simon Cruanes
f8281bfcc2 test: check unsat cores in icnf-solve 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
05e2506362 refactor: remove minismt things, make simple msat.sh 2019-02-11 16:55:43 +01:00
Simon Cruanes
5846ae7e17 chore: finish moving to dune 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
9bc85160b8 restrict what Msat core lib exposes, provide shortcuts 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
Cedric Cellier
0425ce6206 Fix typo in the pigeon hole test description 2018-06-02 18:55:20 +02:00
Guillaume Bury
33cf73e304 [bug] Add test file 2017-03-31 15:17:31 +02:00
Guillaume Bury
4aa4cb063c Add original problem to bug testfile 2017-03-30 19:32:33 +02:00
Guillaume Bury
7a7f224dd5 Add bug testfile 2017-03-30 18:47:10 +02:00
Guillaume Bury
8076c06047 [bugfix] Eliminate duplicates in input clauses 
When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.
 2017-02-15 13:04:54 +01:00
Guillaume Bury
4159a34c20 Removed module alias for SAT expressions 2016-12-02 15:49:49 +01:00
Guillaume Bury
73ea4fea30 Removed useless check option in test_api 2016-11-22 16:58:02 +01:00
Guillaume Bury
b88b906da9 Added test for bug (conflict at level 0) 2016-11-21 15:51:55 +01:00
Guillaume Bury
f35d3a9f23 Fixed uninterpreted predicates for mcsat solver 2016-09-23 15:57:38 +02:00
Guillaume Bury
1656995097 Added uninterpreted functions to mcsat solver 2016-09-23 15:39:23 +02:00
Guillaume Bury
4f5bb640ca [WIP] All is setup, remains to have real theories 
Architecture is now all setup, but theories for the smt and mcsat
solvers are currently dummy ones that are not doing anything.
 2016-09-16 15:49:33 +02:00
Simon Cruanes
d6c6331d85 check proofs in test_api 2016-07-28 11:10:31 +02:00
Simon Cruanes
09b13be78d reflect test_api result in its errcode 2016-07-27 23:24:01 +02:00
Simon Cruanes
98d5074da6 updates to tests 2016-07-27 19:09:11 +02:00
Simon Cruanes
3e54fac7f9 add some tests for the API 2016-07-27 18:54:56 +02:00
Guillaume Bury
cb8092af3b Cleaned makefile a bit + moved the testing binary 2016-01-30 17:02:24 +01:00
Guillaume Bury
2613926ab1 First changes for better persistent proofs 
This commit ensures that clauses now contain
all necessary information to construct the proof
graph (without relying on propagation reasons).
 2016-01-21 00:06:41 +01:00
Guillaume Bury
bbbd407631 Res now includes solver type 2015-10-02 13:30:32 +02:00
Guillaume Bury
434697ea47 Better dot backend 2015-07-28 23:23:05 +02:00
Guillaume Bury
2ed541d528 Faster iterating over subterms 2014-12-18 15:34:01 +01:00
Guillaume Bury
aacae0883b Bundled both smt and mcsat in sat_solve; updated the tests in Makefile 2014-12-16 21:32:18 +01:00
Guillaume Bury
ca70f87973 Mcsat now works 2014-12-16 17:30:14 +01:00
Guillaume Bury
5654414bfa Small fixes 2014-11-18 18:41:32 +01:00
Guillaume Bury
bfce3e54a2 Fixed incomplete proofs due to level 0 propagation 2014-11-15 20:23:11 +01:00
Guillaume Bury
384bcb7270 Better explanations in equivalence closure 2014-11-15 18:39:19 +01:00
Guillaume Bury
e92740e75e Better integration of smt into sat-solve (sic) 2014-11-15 00:59:09 +01:00
Guillaume Bury
37d8ddbd7b Trivial tests for smt 2014-11-14 18:01:07 +01:00
Guillaume Bury
c963145b8f Replaced True and false as pure formulas in tseitin 2014-11-12 23:38:05 +01:00
Guillaume Bury
172ff8bca3 Added smtlib unsat tests to test script 2014-11-10 20:01:51 +01:00
Guillaume Bury
4c040ccbde Added smtlib input option 2014-11-09 23:39:54 +01:00
Guillaume Bury
cac9df4510 Parametric input/output in sat_solve 2014-11-07 16:05:38 +01:00
Guillaume Bury
e1486b416d Lots of fixes for proof generation. 2014-11-07 15:11:32 +01:00