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

33 commits

Author SHA1 Message Date
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
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
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
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
Simon Cruanes
8b1d657695 remove Either 2016-07-22 13:19:16 +02:00
Simon Cruanes
e251799f8e add some array utils for pre-4.03 compat 2016-07-22 11:25:00 +02:00
Guillaume Bury
216ca82fe7 Ensure pushed clauses are added after if_sat slice 2016-07-20 11:45:13 +02:00
Guillaume Bury
d1ebc59856 Avoid unnecessary atoms array to list conversions 2016-07-18 18:49:28 +02:00
Guillaume Bury
38b4fde5c1 Clause atoms are now in an array instead of a vec 2016-07-18 18:42:15 +02:00
Guillaume Bury
933943c4e3 Merge branch '0.3.1' 2016-07-18 18:13:48 +02:00
Guillaume Bury
9be4c66911 [bugfix] Clause level now computed at creation 
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
 2016-07-09 03:20:38 +02:00
Guillaume Bury
dcc410c8a0 Added stack to delay adding of pushed clauses 2016-07-09 03:20:38 +02:00
Guillaume Bury
eba84fba42 Aliased def of negated in Expr_intf 2016-07-08 17:34:46 +02:00
Guillaume Bury
b56e4e3355 Added if_sat to Theory_intf 2016-07-08 16:15:05 +02:00
Guillaume Bury
eb2850caa6 Moved some type def outside Plugins/Theories 2016-07-08 14:29:45 +02:00
Guillaume Bury
bbbc29948d Added src directory, moved some files around 2016-07-07 15:48:50 +02:00