simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 17:04:39 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 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
  • ccebc8c44a Fix for uip unit clause which conflicts with level0 Guillaume Bury 2015-01-26 15:01:26 +01:00
  • 51339eccf8 Bug fixed (hopefully) Guillaume Bury 2015-01-24 21:43:23 +01:00
  • 8fcf90b5c9 Some more debug logging Guillaume Bury 2015-01-24 21:31:45 +01:00
  • 8afdc59ced Tentative fix for absurd slice size Guillaume Bury 2015-01-24 21:24:03 +01:00
  • f85714537e Some more logging messages Guillaume Bury 2015-01-24 21:10:01 +01:00
  • 6b70dd413c Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-01-24 18:11:24 +01:00
  • 508698fd33 Better log levels Guillaume Bury 2015-01-24 18:11:01 +01:00
  • 23a3b3e72d Fixed a bug in printing Guillaume Bury 2015-01-20 16:03:01 +01:00
  • d227d4c8b5 Solver modules are paramtrized by log module Guillaume Bury 2015-01-20 12:58:28 +01:00
  • 24b9362b30 [bugfix] when picking a new term to be assigned, it is possible it is already assigned Guillaume Bury 2015-01-13 18:08:19 +01:00
  • b05b21ac34 [bugfix] semantic variables weren't reset when backtracking Guillaume Bury 2015-01-13 18:02:06 +01:00
  • 017bcaad78 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2015-01-13 17:37:11 +01:00
  • cf578d1868 Removed useless level in plugin_intf Guillaume Bury 2015-01-13 17:36:13 +01:00
  • ff25fae192 Fixed an interface omission Guillaume Bury 2015-01-09 15:04:06 +01:00
  • a499d65fde Added model output for Mcsolver Guillaume Bury 2015-01-09 14:53:46 +01:00
  • fe41b38501 Added propagation function in slice Guillaume Bury 2015-01-06 19:28:53 +01:00
  • 4b25650c4d Updated version number in opam to 0.1 Guillaume Bury 2014-12-18 16:17:52 +01:00
  • 4e34bbdf59 Added some headers, and an interface for Expr Guillaume Bury 2014-12-18 16:04:17 +01:00
  • 2ed541d528 Faster iterating over subterms Guillaume Bury 2014-12-18 15:34:01 +01:00
  • aacae0883b Bundled both smt and mcsat in sat_solve; updated the tests in Makefile Guillaume Bury 2014-12-16 21:32:18 +01:00
  • ca70f87973 Mcsat now works Guillaume Bury 2014-12-16 17:30:14 +01:00
  • aee73abd47 Progressing. Conflict clause computing is broken Guillaume Bury 2014-12-15 17:09:01 +01:00
  • a0d6be1057 Modifications in progress.... Guillaume Bury 2014-12-12 17:14:06 +01:00
  • 8e8a592475 Some reorganization of files/folders Guillaume Bury 2014-12-11 15:31:25 +01:00
  • ff83cb70e9 Fix for mid-solving clause adding Guillaume Bury 2014-11-23 20:49:16 +01:00
  • be4ce92d08 Fix in filenames during bench log parsing Guillaume Bury 2014-11-20 20:38:19 +01:00
  • d52c6d7965 Small update to bench/makefile Guillaume Bury 2014-11-20 20:18:45 +01:00
  • 02b5c61ee1 Better color scheme for dot output Guillaume Bury 2014-11-20 14:38:25 +01:00
  • 8f2ae64b1a Small modifications to colors in dot proof output Guillaume Bury 2014-11-20 00:39:37 +01:00
  • 4636a94ce2 Fix for theory propagated clauses Guillaume Bury 2014-11-20 00:05:06 +01:00
  • 5752a9f139 Changed theory interface to allow pushing of clauses Guillaume Bury 2014-11-19 21:56:24 +01:00
  • 5654414bfa Small fixes Guillaume Bury 2014-11-18 18:41:32 +01:00
  • 460df56d4b fix makefile (bis) Simon Cruanes 2014-11-18 17:56:29 +01:00
  • 50b62b4802 fix redundancies in Makefile Simon Cruanes 2014-11-18 17:53:45 +01:00
  • 1eb8cc62a0 TODO Update Guillaume Bury 2014-11-18 17:26:02 +01:00
  • 8e0dfc539c Check now also whecks model if sat. Guillaume Bury 2014-11-18 16:16:02 +01:00
  • 4ee3566aa0 Catched exception unkown_status in parselog Guillaume Bury 2014-11-17 17:20:20 +01:00
  • 5bcb8ae99f Added a few features in bench_stats Guillaume Bury 2014-11-17 17:07:40 +01:00
  • b992794a77 Added diff computing in bench_stats Guillaume Bury 2014-11-17 15:48:41 +01:00
  • ee86da6329 Added minimal utility for getting bench stats Guillaume Bury 2014-11-17 13:52:53 +01:00
  • d0ca516eb0 Fix for iteration on variables Guillaume Bury 2014-11-16 21:23:54 +01:00
  • 3e74eaaaa5 Moved vars vector from solver to solver_types Guillaume Bury 2014-11-16 14:32:10 +01:00
  • 36e0466304 push/pop: restore trail, causes, learnts Simon Cruanes 2014-11-15 21:26:49 +01:00
  • bfce3e54a2 Fixed incomplete proofs due to level 0 propagation Guillaume Bury 2014-11-15 20:23:11 +01:00
  • c6dd201014 Fixed bug in smtlib translation Guillaume Bury 2014-11-15 19:42:09 +01:00
  • 384bcb7270 Better explanations in equivalence closure Guillaume Bury 2014-11-15 18:39:19 +01:00
  • dbf0646171 Bugfix in proof generation Guillaume Bury 2014-11-15 18:38:24 +01:00
  • 6801acdafd Normalisation is now done in constructors for smt Guillaume Bury 2014-11-15 12:20:34 +01:00
  • e92740e75e Better integration of smt into sat-solve (sic) Guillaume Bury 2014-11-15 00:59:09 +01:00
  • 37d8ddbd7b Trivial tests for smt Guillaume Bury 2014-11-14 18:01:07 +01:00
  • 8ae3277cb3 Fixed a bug in documentaion placement in html Guillaume Bury 2014-11-14 17:59:50 +01:00
  • fcbcf5a9d4 Small fix for tautologies in cc for smt Guillaume Bury 2014-11-14 17:53:16 +01:00
  • 566c30bdcc Added Smt module Guillaume Bury 2014-11-14 17:40:29 +01:00
  • b7c5b39e02 moved smt folder to old Guillaume Bury 2014-11-14 11:58:43 +01:00
  • 6dc90d5f3f TODO Update Guillaume Bury 2014-11-13 00:13:12 +01:00
  • 55c5c3f0f0 Fix in doc Guillaume Bury 2014-11-12 23:39:04 +01:00
  • c963145b8f Replaced True and false as pure formulas in tseitin Guillaume Bury 2014-11-12 23:38:05 +01:00
  • ec32a67e54 Better doc for theory interface Guillaume Bury 2014-11-12 21:29:15 +01:00
  • 752fcbe2ba Tail-rec version of sform in tseitin. Guillaume Bury 2014-11-12 18:56:56 +01:00
  • e2d4f4fdc5 Added theory lemma as possible premise for clauses Guillaume Bury 2014-11-12 17:29:11 +01:00
  • aad20489cd Fix in doc comment Guillaume Bury 2014-11-12 16:53:19 +01:00
  • b44c3c3559 Fixed indentation Guillaume Bury 2014-11-12 16:51:41 +01:00
  • 73c9082b3a Removed solver_types module in solver.Make functor Guillaume Bury 2014-11-12 16:48:44 +01:00
  • 2b2631b1c3 Removed a few warnings Guillaume Bury 2014-11-12 16:27:52 +01:00
  • 35ce540684 Progressing on new theory interface Guillaume Bury 2014-11-12 16:24:08 +01:00
  • 68a1249527 New interface for theories (still needs work in solver.ml) Guillaume Bury 2014-11-11 23:52:36 +01:00
  • 9b733851c6 Removed useless argument to Th.assume Guillaume Bury 2014-11-11 15:34:10 +01:00