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

413 commits

This branch
This branch
All branches
Author SHA1 Message Date
Guillaume Bury
a0d8bd5457 Added dolmen dependency 2016-09-12 17:11:05 +02:00
Guillaume Bury
0631135bd5 Smt solver with dummy theory now builds 2016-09-12 15:43:57 +02:00
Guillaume Bury
fa8957784a Restored simple expressions for pure SAT 2016-09-12 15:37:06 +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
Guillaume Bury
954892ac4a [WIP] Strange compiler bug 2016-09-09 12:07:13 +02:00
Guillaume Bury
742f8c469d Added Expr and typing module from ArchSat 2016-09-07 17:58:07 +02:00
Simon Cruanes
bb2c931d68 wip 2016-08-24 18:23:01 +02:00
Simon Cruanes
41557a1509 wip: make SMT great again 2016-08-16 17:20:48 +02:00
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