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

485 commits

This branch
This branch
All branches
Author SHA1 Message Date
Guillaume Bury
2613926ab1 First changes for better persistent proofs 
This commit ensures that clauses now contain
all necessary information to construct the proof
graph (without relying on propagation reasons).
 2016-01-21 00:06:41 +01:00
Simon Cruanes
756363ffd6 everwhere, use new Log interface and remove the functor on Log_intf 2016-01-20 21:05:22 +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
Simon Cruanes
6e5d737b42 get rid of dependency on unix 2016-01-20 20:13:32 +01:00
Simon Cruanes
facfe336a1 add eval_level in the API of the SAT solver 2016-01-20 20:06:56 +01:00
Guillaume Bury
a21807c624 Fix for semantic conflict and decision levels 
When faced with a semantic conflict, a new decision
must be made to solve the conflict, however, because
we just backtracked, it is not ensured that the solver
is in a correct state to add a new level, so the decision
is now delayed until propagation has been done.
 2015-12-11 16:26:51 +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
1d1ba51329 Fixed some bugs related to push/pop and propagation 2015-12-08 15:58:49 +01:00
Guillaume Bury
3168d4ae2b Fixed bug in if_sat 
The trick using a bool ref to see if a new clause has been pushed
did not detect cases where new clauses were added using assume.
 2015-12-08 13:11:05 +01:00
Guillaume Bury
9f421e6b1d Added package name to opam file 2015-11-30 15:49:53 +01:00
Guillaume Bury
3f1d9fead6 Prepare for opam release 2015-11-27 18:13:10 +01:00
Guillaume Bury
f9f88e0767 Removed special solver types module for pure SAT 
This specialisation was there to have better performances,
but it doesn't seem to have any impact anymore.
 2015-11-27 15:23:04 +01:00
Guillaume Bury
656b7d4fd7 Merge pull request #3 from Gbury/refactor_perf 
wip: remove Log in critical path (improves perf)
 2015-11-27 15:16:11 +01:00
Simon Cruanes
19e7179334 wip: remove Log in critical path (improves perf) 2015-11-27 14:59:33 +01:00
Guillaume Bury
3f6de07440 Merge branch 'master' into push_pop 2015-11-27 14:53:41 +01:00
Guillaume Bury
f72f3c44ee Merge pull request #2 from Gbury/refactor 
Indentation and style fix
 2015-11-25 14:01:29 +01:00
Simon Cruanes
99b1f25e4f style 2015-11-25 10:28:21 +01:00
Simon Cruanes
15e5a4224d ocp-indent all the files, for the greater good! 2015-11-25 10:04:01 +01:00
Simon Cruanes
a729d2dafb small changes to the readme 2015-11-25 09:55:23 +01:00
Guillaume Bury
a32d443b96 Cleaned unused vec 2015-11-24 16:09:59 +01:00
Guillaume Bury
3fd91d9751 Fixed push in case of unsat env 
Renamed some field names of env in solver/internal
 2015-11-24 14:33:02 +01:00
Guillaume Bury
5911f18cb4 Res module adapted to accomodate puush/pop 2015-11-19 14:59:54 +01:00
Guillaume Bury
28f32de24c Removed assertion 
Long explanation: when backtracking to level 0,
while already being at level 0, very strange
things might happen, most notably there might still
be facts left to propagate...
 2015-11-18 17:43:26 +01:00
Guillaume Bury
6567d32900 Fixed bad decision level updating during pop 2015-11-18 17:37:36 +01:00
Guillaume Bury
763d23146f A *lot* of fixes for push/pop 2015-11-17 16:17:14 +01:00
Guillaume Bury
e2cac78d39 Fixed typos in clause simplification 2015-10-20 16:48:43 +02:00
Guillaume Bury
ac5e8a9766 First test (probably unsound) 2015-10-19 22:04:15 +02:00
Guillaume Bury
fa24d2da6f Small _tags update 2015-10-05 15:18:42 +02:00
Guillaume Bury
bbbd407631 Res now includes solver type 2015-10-02 13:30:32 +02:00
Guillaume Bury
434697ea47 Better dot backend 2015-07-28 23:23:05 +02:00
Guillaume Bury
aed3aeb17c A bit of restructuring to have cleaner dependencies between fonctors 2015-07-21 19:20:40 +02:00
Guillaume Bury
9c1ca06aea Dot output is now available through independent backend 2015-07-09 19:03:44 +02:00
Guillaume Bury
4b51f22464 Changed internal representation of proofs 2015-07-09 16:29:57 +02:00
Guillaume Bury
393d521478 Version 1.1 release 2015-06-26 14:51:23 +02:00
Guillaume Bury
e7140d6897 Added some abstraction to allow for more direct types int the pure SAT 
solver
 2015-06-26 14:12:47 +02:00
Guillaume Bury
ce05d8fe62 Simpler representation of solver types 2015-06-26 12:58:00 +02:00
Guillaume Bury
898cfee53e Removed some old, unused legacy code 2015-06-25 15:45:18 +02:00
Guillaume Bury
6f384fb80b Big refactoring of code. Some performances were lost on pure SAT Solving. 2015-06-25 15:37:29 +02:00
Guillaume Bury
23f627cae3 Removed dependency on zarith and fixed build options. Solves issue #1 2015-05-07 16:07:04 +02:00
Simon Cruanes
383ce09653 add zarith as a dependency (close #1) 2015-05-07 15:56:07 +02:00
Guillaume Bury
198890b68c Remove some excessive debug messages 2015-03-19 12:47:36 +01:00
Guillaume Bury
8ee66bf88f Merge branch 'master' of github.com:Gbury/mSAT 2015-03-19 12:36:19 +01:00
Guillaume Bury
e0ac6b31fd Fix for vector resizing in 'set' 2015-03-18 15:13:18 +01:00
Guillaume Bury
c1af34823c Fix for compilation on older ocaml compiler 2015-03-17 17:33:35 +01:00
Guillaume Bury
e059441347 Fixed potential bug in vec.set 
Removed some excessive logging messages
 2015-03-17 14:20:11 +01:00
Guillaume Bury
6206ad6378 Added some asserts in vectors/sparse vectors 2015-03-16 16:23:30 +01:00
Guillaume Bury
e748333693 Assert for growing vectors 2015-03-16 16:16:44 +01:00
Guillaume Bury
a2e2e15137 Fix for restart increments 2015-03-16 15:50:20 +01:00
Guillaume Bury
f604401e47 More log messages 2015-03-16 15:29:12 +01:00
Guillaume Bury
a362505d86 Little test 2015-03-16 15:22:18 +01:00