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

73 commits

Author SHA1 Message Date
Simon Cruanes
dbf88279a1 test: more reg tests 2019-12-28 09:19:17 -06:00
Simon Cruanes
8749cfff0a test: add reg test 2019-12-28 08:49:04 -06:00
Simon Cruanes
b250587a5f tst: add some regression tests; remove dead file 2019-12-28 08:34:42 -06:00
Simon Cruanes
c54ee2310e test: better conf for sidekick 2019-12-28 05:19:01 -06:00
Simon Cruanes
c4d2a800ab test: update test config to use $cur_dir 2019-12-28 05:17:47 -06:00
Simon Cruanes
0ec9c1683f test: modify logitest config file 2019-12-28 05:17:47 -06:00
Simon Cruanes
c55e7a613b test: add some basic datatype tests 2019-12-28 05:17:47 -06:00
Simon Cruanes
14f68749a5 add more tests 2019-12-13 17:55:10 -06:00
Simon Cruanes
d6c003390d rename logitest to benchpress 2019-12-13 16:38:01 -06:00
Simon Cruanes
85b0066660 test: update logitest config and makefile 2019-12-11 18:37:37 -06:00
Simon Cruanes
682edc4640 test: update logitest config 2019-12-09 17:40:57 -06:00
Simon Cruanes
678bf5e03d test: update expect field in toml 2019-11-23 13:23:30 -06:00
Simon Cruanes
f1fc429b5a add basic test for th-cstor 2019-11-23 13:23:30 -06:00
Simon Cruanes
e414112010 test: add some basic datatype tests 2019-11-23 13:23:30 -06:00
Simon Cruanes
0aa7a4ea25 chore: update test config 2019-11-19 16:16:47 -06:00
Simon Cruanes
951be35112 test: fix config for new option format 2019-06-07 11:36:45 -05:00
Simon Cruanes
e51e996512 test: only run on smt2 files 2019-06-07 11:24:04 -05:00
Simon Cruanes
866249deb1 test: add more tests 2019-03-22 18:49:25 -05:00
Simon Cruanes
9e5c9056d0 test: add a logitest target 2019-02-10 18:07:06 -06:00
Simon Cruanes
26b4f677e0 test: update some tests 2019-02-10 17:00:38 -06:00
Simon Cruanes
668bd36311 test: remove API test, which belongs in msat 2019-02-01 21:12:26 -06:00
Simon Cruanes
4fadbeb04d chore: migrate to dune 2019-01-18 18:37:26 -06:00
Simon Cruanes
c5f23e32b9 test: proper smtlib for QFUF problems 2018-06-11 21:56:34 -05:00
Simon Cruanes
f52883f059 update tests 2018-02-08 22:19:28 -06:00
Simon Cruanes
d73684902f wip: have a proper smtlib parser 2018-02-05 23:09:29 -06:00
Simon Cruanes
ac396e8cf5 rename to cdcl 2018-01-22 22:09:47 -06:00
Simon Cruanes
8c8209c08c large refactoring to keep only a simpler, easier CDCL(T) interface 
- only one functor to instantiate
- explicit state that is carried around
- remove minismt stuff
 2018-01-22 21:52:06 -06:00
Simon Cruanes
99078b2335 make state explicit and add type t state-wrapper in most modules 2017-12-29 16:48:26 +01:00
Simon Cruanes
1cd70b048c split some features into minismt lib 2017-12-28 19:43:54 +01:00
Simon Cruanes
d6c84b93bf restrict what Msat core lib exposes, provide shortcuts 2017-12-28 19:31:55 +01:00
Simon Cruanes
1037c06636 use generative functors, remove a layer of nesting for SMT libs 2017-12-28 19:12:41 +01:00
Simon Cruanes
7722319b0a move tseitin transformation into its own lib 2017-12-28 16:01:36 +01:00
Simon Cruanes
ac50e10788 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
 2017-12-28 15:51:04 +01: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