simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-14 23:06:07 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • f9f88e0767 Removed special solver types module for pure SAT Guillaume Bury 2015-11-27 15:23:04 +01:00
  • 656b7d4fd7 Merge pull request #3 from Gbury/refactor_perf Guillaume Bury 2015-11-27 15:16:11 +01:00
  • 19e7179334 wip: remove Log in critical path (improves perf) Simon Cruanes 2015-11-25 10:36:17 +01:00
  • 3f6de07440 Merge branch 'master' into push_pop Guillaume Bury 2015-11-27 14:53:41 +01:00
  • f72f3c44ee Merge pull request #2 from Gbury/refactor Guillaume Bury 2015-11-25 14:01:29 +01:00
  • 99b1f25e4f style Simon Cruanes 2015-11-25 10:28:21 +01:00
  • 15e5a4224d ocp-indent all the files, for the greater good! Simon Cruanes 2015-11-25 10:04:01 +01:00
  • a729d2dafb small changes to the readme Simon Cruanes 2015-11-25 09:55:23 +01:00
  • a32d443b96 Cleaned unused vec Guillaume Bury 2015-11-24 16:09:59 +01:00
  • 3fd91d9751 Fixed push in case of unsat env Renamed some field names of env in solver/internal Guillaume Bury 2015-11-24 14:33:02 +01:00
  • 5911f18cb4 Res module adapted to accomodate puush/pop Guillaume Bury 2015-11-19 14:59:54 +01:00
  • 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... Guillaume Bury 2015-11-18 17:43:26 +01:00
  • 6567d32900 Fixed bad decision level updating during pop Guillaume Bury 2015-11-18 17:37:36 +01:00
  • 763d23146f A *lot* of fixes for push/pop Guillaume Bury 2015-11-17 16:17:14 +01:00
  • e2cac78d39 Fixed typos in clause simplification Guillaume Bury 2015-10-20 16:48:43 +02:00
  • ac5e8a9766 First test (probably unsound) Guillaume Bury 2015-10-19 22:04:15 +02:00
  • fa24d2da6f Small _tags update Guillaume Bury 2015-10-05 15:18:42 +02:00
  • bbbd407631 Res now includes solver type Guillaume Bury 2015-10-02 13:30:32 +02:00
  • 434697ea47 Better dot backend Guillaume Bury 2015-07-28 23:23:05 +02:00
  • aed3aeb17c A bit of restructuring to have cleaner dependencies between fonctors Guillaume Bury 2015-07-21 19:20:40 +02:00
  • 9c1ca06aea Dot output is now available through independent backend Guillaume Bury 2015-07-09 19:03:44 +02:00
  • 4b51f22464 Changed internal representation of proofs Guillaume Bury 2015-07-09 16:29:57 +02:00
  • 393d521478 Version 1.1 release Guillaume Bury 2015-06-26 14:51:23 +02:00
  • e7140d6897 Added some abstraction to allow for more direct types int the pure SAT solver Guillaume Bury 2015-06-26 14:12:47 +02:00
  • ce05d8fe62 Simpler representation of solver types Guillaume Bury 2015-06-26 12:58:00 +02:00
  • 898cfee53e Removed some old, unused legacy code Guillaume Bury 2015-06-25 15:45:18 +02:00
  • 6f384fb80b Big refactoring of code. Some performances were lost on pure SAT Solving. Guillaume Bury 2015-06-25 15:34:39 +02:00
  • 23f627cae3 Removed dependency on zarith and fixed build options. Solves issue #1 Guillaume Bury 2015-05-07 16:07:04 +02:00
  • 383ce09653 add zarith as a dependency (close #1) Simon Cruanes 2015-05-07 15:56:07 +02:00
  • 198890b68c Remove some excessive debug messages Guillaume Bury 2015-03-19 12:47:36 +01:00
  • 8ee66bf88f Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-03-19 12:36:19 +01:00
  • e0ac6b31fd Fix for vector resizing in 'set' Guillaume Bury 2015-03-18 15:13:18 +01:00
  • c1af34823c Fix for compilation on older ocaml compiler Guillaume Bury 2015-03-17 17:33:35 +01:00
  • e059441347 Fixed potential bug in vec.set Removed some excessive logging messages Guillaume Bury 2015-03-17 14:20:11 +01:00
  • 6206ad6378 Added some asserts in vectors/sparse vectors Guillaume Bury 2015-03-16 16:23:30 +01:00
  • e748333693 Assert for growing vectors Guillaume Bury 2015-03-16 16:16:44 +01:00
  • a2e2e15137 Fix for restart increments Guillaume Bury 2015-03-16 15:50:20 +01:00
  • f604401e47 More log messages Guillaume Bury 2015-03-16 15:29:12 +01:00
  • a362505d86 Little test Guillaume Bury 2015-03-16 15:22:18 +01:00
  • 381081314e Removed some useless semi-colons Guillaume Bury 2015-03-16 13:56:28 +01:00
  • 31f5fdd1ae Debugging... Guillaume Bury 2015-03-16 13:27:51 +01:00
  • 25dae83c6e Still working... Guillaume Bury 2015-03-15 22:12:21 +01:00
  • 5a61a6c852 Still in extreme debug mode Guillaume Bury 2015-03-15 22:00:48 +01:00
  • c5fd429821 Extremely verbose message added (to be removed later) Guillaume Bury 2015-03-15 21:55:29 +01:00
  • 34141f9d7d Added a few debug messages Guillaume Bury 2015-03-15 21:52:48 +01:00
  • 1f0fdf65fd Hopefully a fix for restarts Guillaume Bury 2015-03-15 21:32:07 +01:00
  • 582530b9ee Logging restarts Guillaume Bury 2015-03-15 20:42:16 +01:00
  • 5047882fc7 Fix for dependencies during proof computing Guillaume Bury 2015-03-13 15:03:30 +01:00
  • ee13eb366b Fix for incomplete proofs due to hypothesis not proved Guillaume Bury 2015-03-13 14:48:20 +01:00
  • 6005652f3f Only pure hypothesis are instantly learned Guillaume Bury 2015-03-13 14:39:48 +01:00
  • 5786e26705 Typo Guillaume Bury 2015-03-13 14:35:00 +01:00
  • 0050fdae3c Better clause names Guillaume Bury 2015-03-13 14:31:46 +01:00
  • cddf914ce6 Better proving of hypothesis Guillaume Bury 2015-03-13 14:23:40 +01:00
  • d7c5077c0a Log module is passed down to proof module in solvers Guillaume Bury 2015-03-13 14:09:16 +01:00
  • 9b41aab1b1 Tautological input clauses are now accepted Guillaume Bury 2015-03-10 18:02:31 +01:00
  • a17d83eb1d Fixed location of debug message Guillaume Bury 2015-03-10 17:57:48 +01:00
  • 1b5038e620 New clauses are memorized, and redundant ones eliminated. Guillaume Bury 2015-03-10 17:43:41 +01:00
  • 51a74c6505 First release Guillaume Bury 2015-03-03 17:22:49 +01:00
  • f6fbd874ec Fixed bug in sat example in readme Guillaume Bury 2015-03-03 17:09:39 +01:00
  • cdf8371394 Added info about solver functor Guillaume Bury 2015-03-03 17:06:16 +01:00
  • 926948d693 Fixed typo + added ocaml annotation in markdown Guillaume Bury 2015-03-03 17:00:06 +01:00
  • 68edd9916e Updated README + some more doc Guillaume Bury 2015-03-03 16:54:28 +01:00
  • e20876ad02 Added some convenience functions in pure sat solver Guillaume Bury 2015-02-18 16:45:36 +01:00
  • d58c5c0756 Made sat atom type private Guillaume Bury 2015-02-18 16:32:18 +01:00
  • e584e0979d A bit of cleanup of dead code Guillaume Bury 2015-02-09 17:43:45 +01:00
  • 714e0988e3 [bugfix] some late unsat conflicts were not handled correctly Guillaume Bury 2015-02-09 17:25:58 +01:00
  • 07c62fc5bc Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-02-09 17:11:36 +01:00
  • 9c8e970b8d [bugfix] level 0 conflict in mcsat weren't detected Guillaume Bury 2015-02-09 17:10:45 +01:00
  • 1062297389 fix usage of Log in Solver Simon Cruanes 2015-02-09 15:47:41 +01:00
  • 5f155f6bde Simplified proof generation Guillaume Bury 2015-02-09 16:07:28 +01:00
  • 74238bbed8 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-02-09 15:43:26 +01:00
  • 23d18fe609 Added log functor to Sat.Make Guillaume Bury 2015-02-09 15:42:28 +01:00
  • 317a7c73d9 don't run tests in opam file Simon Cruanes 2015-02-09 15:38:29 +01:00
  • 3d951db181 Small update for clause info about proofs Guillaume Bury 2015-02-09 15:34:49 +01:00
  • a7951ea143 Small change for clause names Guillaume Bury 2015-02-09 15:12:04 +01:00
  • 3ec4f6f2e3 [bugfix] semantic backtrack added decision with wrong level Guillaume Bury 2015-02-09 14:15:15 +01:00
  • 4ff01d2a7e Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-02-09 14:01:59 +01:00
  • 312758ce1b [bugfix] tag were not properly set when assuming new clauses Guillaume Bury 2015-02-09 14:01:29 +01:00
  • 425043a362 small details Simon Cruanes 2015-02-09 11:35:55 +01:00
  • c2cfa14e86 small perf change Simon Cruanes 2015-02-06 17:47:29 +01:00
  • ce8920bf88 Revert "[bugfix] uip clause detection was wrong" Guillaume Bury 2015-02-06 17:16:58 +01:00
  • 7a5e8e082d [bugfix] uip clause detection was wrong Guillaume Bury 2015-02-06 17:05:37 +01:00
  • 3203dadb8d Replaced clause number by tag in solver.assume Guillaume Bury 2015-02-06 15:46:56 +01:00
  • 00b894acef Min/max typo Guillaume Bury 2015-02-06 14:36:09 +01:00
  • 0d66605afd Fix for empty arguments lemma printing in dot proofs Guillaume Bury 2015-02-06 14:33:35 +01:00
  • 5067274b4c Replaced maps by hashtbl for mcsat Guillaume Bury 2015-02-06 09:56:29 +01:00
  • c9657cc795 Small log message update Guillaume Bury 2015-02-04 14:58:00 +01:00
  • 07b49c8481 Added 'if_sat' possibility for plugins Guillaume Bury 2015-02-03 17:37:36 +01:00
  • cef1cef703 Fix typo in resolution error message Guillaume Bury 2015-01-30 10:28:46 +01:00
  • 0e84c5bfb3 Revert "Removed an error that was raised for tautological conflict clauses" Guillaume Bury 2015-01-29 15:49:01 +01:00
  • 436dc49111 Better error message Guillaume Bury 2015-01-29 15:44:54 +01:00
  • 803b61c7dc Removed an error that was raised for tautological conflict clauses Guillaume Bury 2015-01-29 15:39:48 +01:00
  • a0ae0ca90c Forgot to end a 'TR' Guillaume Bury 2015-01-29 15:16:51 +01:00
  • b6089e67c3 Fix for bad html printing Guillaume Bury 2015-01-29 15:14:24 +01:00
  • 863a49a0a4 Update for proof output in dot Guillaume Bury 2015-01-29 15:00:52 +01:00
  • 676ed7eed9 Better proof output for dot format Guillaume Bury 2015-01-29 14:44:23 +01:00
  • 6995cf90e1 Fix for iheap size Guillaume Bury 2015-01-26 15:56:05 +01:00
  • a5c67c7545 Fix for lack of insertion of new atoms in iheap. Guillaume Bury 2015-01-26 15:54:28 +01:00
  • db0bd8c2df Fix for late propagation of theories when it conflicts with boolean propagtion. Printing fix Guillaume Bury 2015-01-26 15:49:27 +01:00
  • 3ed5d26ac7 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-01-26 15:02:44 +01:00