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

1024 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Guillaume Bury
381081314e Removed some useless semi-colons 2015-03-16 13:56:28 +01:00
Guillaume Bury
31f5fdd1ae Debugging... 2015-03-16 13:27:51 +01:00
Guillaume Bury
25dae83c6e Still working... 2015-03-15 22:12:21 +01:00
Guillaume Bury
5a61a6c852 Still in extreme debug mode 2015-03-15 22:00:48 +01:00
Guillaume Bury
c5fd429821 Extremely verbose message added (to be removed later) 2015-03-15 21:55:29 +01:00
Guillaume Bury
34141f9d7d Added a few debug messages 2015-03-15 21:52:48 +01:00
Guillaume Bury
1f0fdf65fd Hopefully a fix for restarts 2015-03-15 21:32:07 +01:00
Guillaume Bury
582530b9ee Logging restarts 2015-03-15 20:42:16 +01:00
Guillaume Bury
5047882fc7 Fix for dependencies during proof computing 2015-03-13 15:03:30 +01:00
Guillaume Bury
ee13eb366b Fix for incomplete proofs due to hypothesis not proved 2015-03-13 14:48:20 +01:00
Guillaume Bury
6005652f3f Only pure hypothesis are instantly learned 2015-03-13 14:39:48 +01:00