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

86 commits

Author SHA1 Message Date
Simon Cruanes
0b351ea67e test: add regression test for bad LRA preprocessing 2021-03-18 14:14:24 -04:00
Simon Cruanes
d6aa1071d7 test: add more regression files 2021-02-22 14:30:43 -05:00
Simon Cruanes
23dcf79560 more regression tests 2020-12-22 15:02:12 -05:00
Simon Cruanes
3d46986161 test: add regression test for xor 2020-12-22 14:59:06 -05:00
Simon Cruanes
f510bfaf25 add regression tests for LRA 2020-10-20 15:43:02 -04:00
Simon Cruanes
c5180f3f63 remove dead symlink 2020-08-18 10:01:15 -04:00
Simon Cruanes
b724882516 test: detail in benchpress config 2020-07-28 15:55:54 -04:00
Simon Cruanes
0b283a384d test: add some regression tests 2020-02-21 16:46:57 -06:00
Simon Cruanes
4e1b35d2c3 test: add regression test 2020-02-17 12:30:58 -06:00
Simon Cruanes
6aae70f15a test: add more regression tests for datatypes 2020-01-17 19:12:50 -06:00
Simon Cruanes
5bcecfd68c Merge branch 'wip-data' 2020-01-14 23:02:49 -06:00
Simon Cruanes
17a09f2cbc test: add some regression tests 2020-01-14 20:23:14 -06:00
Simon Cruanes
48d6b57383 test: enable progress by default 2020-01-08 19:51:25 -06:00
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