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

Commit graph

  • 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
  • b50246d55d Some more doc + indentation Guillaume Bury 2014-11-11 13:54:24 +01:00
  • 6338f682df Added unsat-core option in sat_solve Cleaned up a bit soler_types and added some doc Guillaume Bury 2014-11-11 12:25:16 +01:00
  • ccfbe72bdf Safer code for input format auto-detection Guillaume Bury 2014-11-11 10:45:01 +01:00
  • 172ff8bca3 Added smtlib unsat tests to test script Guillaume Bury 2014-11-10 20:01:51 +01:00
  • 562fcc1930 Added auto-detection of input format Guillaume Bury 2014-11-10 19:59:40 +01:00
  • 625c0ad309 Fix for tseitin cnf conversion Guillaume Bury 2014-11-10 19:47:42 +01:00
  • e74dddc4b0 Removed outdated .depend Guillaume Bury 2014-11-10 19:28:52 +01:00
  • b109924bc1 New option to print cnf after conversion. Guillaume Bury 2014-11-10 00:24:41 +01:00
  • 4c040ccbde Added smtlib input option Guillaume Bury 2014-11-09 23:39:54 +01:00
  • a28cf4098c Removed useless dir in Makefile Guillaume Bury 2014-11-09 18:43:33 +01:00
  • ff34f5c6f0 Added tseitin cnf conversion Guillaume Bury 2014-11-08 15:28:26 +01:00
  • d6cfd27f32 Fixed a bug in proof dot printer (+ indent) Guillaume Bury 2014-11-07 17:46:32 +01:00
  • cac9df4510 Parametric input/output in sat_solve Guillaume Bury 2014-11-07 16:05:38 +01:00
  • e1486b416d Lots of fixes for proof generation. Guillaume Bury 2014-11-07 15:11:32 +01:00
  • 7d7859010e Removed unsat_core from solver.ml Guillaume Bury 2014-11-07 13:48:12 +01:00
  • 6073622a8c Unit hyp clauses are now added as assumptions in the proof Guillaume Bury 2014-11-07 09:37:36 +01:00
  • 19ebfeb866 Now using unicode characters Guillaume Bury 2014-11-06 21:24:11 +01:00
  • fd4a618c2a Better dot output for unsat proofs Guillaume Bury 2014-11-06 21:05:45 +01:00
  • 62835b35d0 Indentation + some debug output in res.ml Guillaume Bury 2014-11-06 18:56:39 +01:00
  • a13029f96c Added proof building and output for pure sat. Guillaume Bury 2014-11-06 18:25:55 +01:00
  • f36aa78a35 In sat/sat, replaced theory state with type unit Guillaume Bury 2014-11-06 00:20:40 +01:00
  • f9fde897e0 Better logging in index when benchmarking (again) Guillaume Bury 2014-11-05 23:50:29 +01:00
  • 7288f6ece2 Better logging in log/index when running benchs on same commit New sync target in bench/Makefile (untested though) Guillaume Bury 2014-11-05 23:38:50 +01:00
  • a31285d3ad New bench target in root Makefile bench/Makefile now builds the test utility if not already built Guillaume Bury 2014-11-05 23:00:23 +01:00
  • 51f5a00224 sat_solve is now build in 'all', test replacfes test-full in Makefile targets. Guillaume Bury 2014-11-05 21:19:28 +01:00
  • fad14a7e4f use Neperien for logging log Simon Cruanes 2014-11-05 21:15:06 +01:00
  • b614e743e2 follow symlinks in bench/makefile Simon Cruanes 2014-11-05 20:02:38 +01:00
  • f9d4b9a00e new Sparse_vec structure, used for vectors with "holes" Simon Cruanes 2014-11-05 17:41:16 +01:00
  • b6aa6ed2fc Makefile for benchs. Guillaume Bury 2014-11-05 15:59:04 +01:00
  • 3422634923 Replaced List.map with List.rev_map Added Vec.set_unsafe and fixed a few bugs Guillaume Bury 2014-11-05 15:57:48 +01:00
  • ea1757875a Now building with debug flag Guillaume Bury 2014-11-05 15:56:37 +01:00
  • 4cde71cce2 Added skeleton for bench makefile Guillaume Bury 2014-11-05 13:17:55 +01:00
  • f1a9245953 Fixed indentation of new options documentation Guillaume Bury 2014-11-05 00:50:28 +01:00