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
1669 commits 53 branches 1 tag 17 MiB
Commit graph

84 commits

Author SHA1 Message Date
Simon Cruanes
65e876bebc
chore: makefile 2022-07-30 23:58:18 -04:00
Simon Cruanes
fbf7c5e090
chore: makefile 2022-02-08 13:11:36 -05:00
Simon Cruanes
50bfe79b6a
test: use dune options, so, release mode 2022-02-02 16:12:29 -05:00
Simon Cruanes
44ad0935fe
chore: add QF_UFLIA to makefile 2022-01-31 15:45:02 -05:00
Simon Cruanes
5989d686da
chore: add target to makefile 2022-01-13 12:55:36 -05:00
Simon Cruanes
110f3f8527
update benchpress file to actually run proofs 2021-12-07 21:16:12 -05:00
Simon Cruanes
2d081c554b chore: fix makefile 2021-08-02 21:34:37 -04:00
Simon Cruanes
a08cda8c5b test: add a lot more tests (for SAT) 2021-08-02 16:05:35 -04:00
Simon Cruanes
c14070b622 perf: compile in release by default 😡 2021-08-02 16:04:59 -04:00
Simon Cruanes
c7bf4b01e7 feat: optional memtrace support 2021-07-18 10:29:14 -04:00
Simon Cruanes
883b27ccc9 add uflra to makefile targets 2020-11-14 16:59:19 -05:00
Simon Cruanes
f510bfaf25 add regression tests for LRA 2020-10-20 15:43:02 -04:00
Simon Cruanes
93b993825b chore(make): also remove trailing spaces in make reindent 2020-02-15 14:36:39 -06:00
Simon Cruanes
858ffb6f25 chore: add --progress in makefile 2019-12-28 05:19:19 -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
0aa7a4ea25 chore: update test config 2019-11-19 16:16:47 -06:00
Simon Cruanes
1428d43369 test: add some unit tests for mini-cc 2019-10-30 15:00:34 -05:00
Simon Cruanes
2e7ab9ba9b wip: simplify a lot and only keep th-bool-static in the functor 2019-06-05 16:53:13 -05:00
Simon Cruanes
9e5c9056d0 test: add a logitest target 2019-02-10 18:07:06 -06:00
Simon Cruanes
4fadbeb04d chore: migrate to dune 2019-01-18 18:37:26 -06:00
Simon Cruanes
70749155bf cleanup of unused sublibrary 2018-05-09 19:34:53 -05: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
d4646ffd63 makefile 2017-12-28 19:12:32 +01:00
Simon Cruanes
7722319b0a move tseitin transformation into its own lib 2017-12-28 16:01:36 +01:00
Simon Cruanes
64d7314aab details 2017-12-28 15:55:00 +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
1cb5eb3fcb [opam] Install doc conditionally 2017-01-25 18:21:32 +01:00
Guillaume Bury
733e71e332 [opam] Update opam file to add doc building 2017-01-25 17:36:37 +01:00
Simon Cruanes
badf58ffdd update doc by merging everything into one dir 2016-11-21 15:02:35 +01:00
Simon Cruanes
21206cb166 remove useless modules and update doc 2016-11-21 14:58:21 +01:00
Guillaume Bury
9cf13bd7a2 Mcsat now works (for pure equality problems) 2016-09-22 18:31:22 +02:00
Guillaume Bury
2a33534312 Added (dummy) mcsat module for test binary 2016-09-14 19:55:57 +02:00
Guillaume Bury
dfff903f8c Removed additional libs. 2016-09-12 15:32:22 +02:00
Guillaume Bury
9d509241ad [WIP] Some drastic cleanup of code 
Some of these changes are to be reverted, among other the structure of
terms used for the instantiation of the pure SAT solver
 2016-09-09 18:09:04 +02:00
Simon Cruanes
41557a1509 wip: make SMT great again 2016-08-16 17:20:48 +02:00
Simon Cruanes
3e54fac7f9 add some tests for the API 2016-07-27 18:54:56 +02:00
Simon Cruanes
51f10d7ad5 update some files 2016-07-22 11:31:17 +02:00
Guillaume Bury
bbbc29948d Added src directory, moved some files around 2016-07-07 15:48:50 +02:00
Guillaume Bury
f19c6b9b77 Fixed dot printing bug 2016-06-29 21:30:44 +02:00
Guillaume Bury
d06de43789 Removed color flag (because ocaml < 4.03) 2016-05-20 16:26:03 +02:00
Guillaume Bury
6d706f55e5 Tags update + optimizations for ocaml 4.03 2016-05-20 16:21:06 +02:00
Guillaume Bury
cb8092af3b Cleaned makefile a bit + moved the testing binary 2016-01-30 17:02:24 +01:00
Simon Cruanes
2fe5be8317 update Log interface, with real/dummy implementation 
- `make disable_log` to use the dummy
- `make enable_log` to use the real one (slower)
 2016-01-20 21:04:44 +01:00
Guillaume Bury
df1f28ccb1 Fix for when the solver becomes unsat during if_sat 2015-12-11 09:08:10 +01:00
Guillaume Bury
4b51f22464 Changed internal representation of proofs 2015-07-09 16:29:57 +02:00
Simon Cruanes
425043a362 small details 2015-02-09 11:46:52 +01:00
Guillaume Bury
ccebc8c44a Fix for uip unit clause which conflicts with level0 2015-01-26 15:01:26 +01:00