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

454 commits

This branch
This branch
All branches
Author SHA1 Message Date
Guillaume Bury
7d57b3f1b5 Accept late conflict clauses, closes #4 2016-08-04 21:34:17 +02:00
Simon Cruanes
12fed8a811 do not ask for comparison on terms and formulas 2016-08-03 20:27:51 +02:00
Simon Cruanes
66707b58fc optimize Vec.{get,set} 2016-07-29 23:43:06 +02:00
Guillaume Bury
6f54604dc9 Optim for non-mcsat solvers 2016-07-29 23:20:31 +02:00
Simon Cruanes
7016bb1825 add an inlining parameter for non-flambda versions of OCaml 2016-07-29 23:02:23 +02:00
Simon Cruanes
af55371eb4 change the caching mechanism for var's assignable subterms 2016-07-29 22:50:37 +02:00
Simon Cruanes
c70c102de9 optim in a bottleneck in Vec 2016-07-29 22:50:26 +02:00
Guillaume Bury
5fdffe1f85 Handle new clauses unsat at level >0 && <=base_lvl 2016-07-29 21:00:24 +02:00
Simon Cruanes
6eeaa8513c fix bug 2016-07-29 20:45:30 +02:00
Simon Cruanes
85c290c0ce small changes 2016-07-29 20:15:53 +02:00
Simon Cruanes
672b5945ce expose true_at_level0 in Solver_intf 2016-07-29 17:51:00 +02:00
Guillaume Bury
9d6634d621 Better interface for Msat.Internal 2016-07-29 15:47:51 +02:00
Simon Cruanes
38a6d8c481 small fix 2016-07-29 15:11:53 +02:00
Guillaume Bury
bc200474eb Simpler code for clause simplification 
Simplify_zero is a strict subset of partition_aux
 2016-07-29 14:40:42 +02:00
Guillaume Bury
a32b35e994 Fix proofs with local assumptions 2016-07-29 13:35:05 +02:00
Guillaume Bury
51c76479b9 Better logging in proofs 2016-07-29 12:58:21 +02:00
Simon Cruanes
d6c6331d85 check proofs in test_api 2016-07-28 11:10:31 +02:00
Simon Cruanes
5a04fa49ed for proofs, represent assumptions as propagations 2016-07-28 10:56:19 +02:00
Simon Cruanes
eb14a1e229 fix 2016-07-28 10:47:59 +02:00
Simon Cruanes
ac706f3e56 fix bug 2016-07-28 10:18:07 +02:00
Simon Cruanes
2e8b45edbc many small changes 2016-07-28 00:51:36 +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
Simon Cruanes
73c2500b05 allow propagation of lits under base_level 2016-07-27 18:16:26 +02:00
Simon Cruanes
3e9c0d3a1e forgot to pop before assume 2016-07-27 17:58:15 +02:00
Simon Cruanes
563e9027e1 first draft of replacing push/pop by assumptions 2016-07-27 17:50:03 +02:00
Guillaume Bury
09166d0370 Removed Stack.fold for compat with ocaml < 4.03 2016-07-26 15:35:22 +02:00
Guillaume Bury
3c6da0ffdc Clause buffer must be fitered when popping 
Indeed imagine the following case:
"push; assume [c]; pop; push; solve"
since c has user-level 1, in the current state, it would
have been wrongfully added to the solver state when solve
is run.
 2016-07-26 14:34:42 +02:00
Guillaume Bury
defcb67aad Use a buffer for adding clauses (to avoid exceptions) 2016-07-26 14:22:32 +02:00
Simon Cruanes
c45fe97ebd micro optim on Vec 2016-07-25 13:44:22 +02:00
Guillaume Bury
6757910225 [travis] Ubuntu doesn't have 'time' by default... 2016-07-23 14:47:52 +02:00
Guillaume Bury
e266134efc Try a different source for opam package in travis 2016-07-23 14:39:33 +02:00
Guillaume Bury
e2530a25b7 Forgot to remove the sudo:required 2016-07-23 14:36:19 +02:00
Guillaume Bury
b5f8c7ddf9 Use travis apt addon to install opam 2016-07-23 14:35:23 +02:00
Guillaume Bury
202249d75e Remove travis-ci script. 2016-07-23 14:23:34 +02:00
Guillaume Bury
a0b810f520 Add travis build status to README 2016-07-23 14:07:40 +02:00
Guillaume Bury
0a4b812924 Moved more commands in before_install for travis 2016-07-23 13:58:45 +02:00
Guillaume Bury
13effa8969 Cleaner way to install opam in travis CI 2016-07-23 13:50:13 +02:00
Guillaume Bury
fda7b9ef3a Missing env var in travis-ci script 2016-07-23 13:32:06 +02:00
Guillaume Bury
33735b5e50 Missing sudo requirement in travis.yml 2016-07-23 13:29:25 +02:00
Guillaume Bury
f957eb4e0c Added ocaml 4.03.0 to travis CI 2016-07-23 13:26:44 +02:00
Guillaume Bury
ec4fd911a9 Fixed typo in travis.yml 2016-07-23 13:25:50 +02:00
Guillaume Bury
54ba6bc745 Added travis CI 2016-07-23 13:24:17 +02:00
Guillaume Bury
3e30a77569 Some more comments 2016-07-22 17:28:12 +02:00
Simon Cruanes
c4beb7054b spurious assertion 2016-07-22 16:51:45 +02:00
Simon Cruanes
895cb9cbfb some additional comments and cleanup 2016-07-22 16:40:22 +02:00
Simon Cruanes
891f764ee8 some more cleanup 2016-07-22 16:31:00 +02:00
Simon Cruanes
c3cfe67696 cleanup boolean propagation 2016-07-22 16:00:02 +02:00
Simon Cruanes
c1915ba2d3 wip: cleanup and documentation of internal.ml 2016-07-22 15:42:17 +02:00