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

  • 61eb921f05 Added iCNF export to external Guillaume Bury 2016-11-25 10:34:31 +01:00
  • 15efe4aceb Revert "change strategy for vec reallocation" Simon Cruanes 2016-11-24 17:38:09 +01:00
  • 20b4692e18 more accurate assertion Simon Cruanes 2016-11-24 14:21:51 +01:00
  • 7407669834 change strategy for vec reallocation Simon Cruanes 2016-11-24 14:14:21 +01:00
  • 6be7e7c71a rename a Vec function Simon Cruanes 2016-11-24 14:11:58 +01:00
  • c64a94c2aa Updated some logging levels Guillaume Bury 2016-11-22 18:07:32 +01:00
  • 3124d55209 [bugfix?] Avoid forgetting theory conflict clauses Guillaume Bury 2016-11-22 17:04:18 +01:00
  • 9a393c130a Some more info in debug logging Guillaume Bury 2016-11-22 17:00:39 +01:00
  • 73ea4fea30 Removed useless check option in test_api Guillaume Bury 2016-11-22 16:58:02 +01:00
  • 9a6d07e097 [bugfix] Do not forget conflict at level 0 Guillaume Bury 2016-11-22 16:53:47 +01:00
  • e3d8513286 [bugfix] late propagations need to be re-propagated Guillaume Bury 2016-11-22 16:43:49 +01:00
  • 0dc44b1173 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2016-11-21 15:53:08 +01:00
  • b88b906da9 Added test for bug (conflict at level 0) Guillaume Bury 2016-11-21 15:51:55 +01:00
  • 1ccf13b89b fix url Simon Cruanes 2016-11-21 15:18:14 +01:00
  • c7d9f8190f update readme Simon Cruanes 2016-11-21 15:05:20 +01:00
  • badf58ffdd update doc by merging everything into one dir Simon Cruanes 2016-11-21 15:02:35 +01:00
  • 21206cb166 remove useless modules and update doc Simon Cruanes 2016-11-21 14:58:21 +01:00
  • 31659c5d73 minor typos Simon Cruanes 2016-11-21 14:47:42 +01:00
  • 38972d7fc6 Typos in doc Guillaume Bury 2016-11-21 14:40:51 +01:00
  • 0ec4288d7c Added some documentation on solver_types Guillaume Bury 2016-11-21 14:37:19 +01:00
  • 03dd2f9e38 Removed some commented code Guillaume Bury 2016-11-17 16:12:34 +01:00
  • 6c0148016d Merge branch 'wip-analyze' Guillaume Bury 2016-11-17 16:11:18 +01:00
  • e7b22b9c3e Merge branch 'wip-basic-smt' Guillaume Bury 2016-11-17 15:22:28 +01:00
  • 7dd04204ed [travis] Only build the bin for tests Guillaume Bury 2016-11-17 00:19:40 +01:00
  • c2887b2e29 [travis] Try and build on old ocaml versions Guillaume Bury 2016-11-17 00:11:26 +01:00
  • 66f250a57e [travis] Changed ocaml test versions Guillaume Bury 2016-11-16 19:52:26 +01:00
  • b4d62d6f3b [breaking] Changed if_sat interface Guillaume Bury 2016-11-16 17:33:10 +01:00
  • 3af700bbd0 [bugfix] Better fix for propagation at level 0 Guillaume Bury 2016-11-09 14:27:50 +01:00
  • 443a3b0731 [bugfix] Attempt at fixing enqueue bug Guillaume Bury 2016-11-09 00:24:41 +01:00
  • d681e247ed Added some debug logging Guillaume Bury 2016-11-04 12:19:43 +01:00
  • d5d7234afc [bugfix] Avoid forgetting 1 atom clauses Guillaume Bury 2016-11-03 16:04:51 +01:00
  • b8d4ee198a Better dimacs printing Guillaume Bury 2016-11-03 10:38:03 +01:00
  • 42b4c00861 wip Simon Cruanes 2016-11-02 16:16:34 +01:00
  • 33ea26c4f5 small fix Simon Cruanes 2016-11-02 16:17:49 +01:00
  • bf5e6cf67c better dimacs printing Simon Cruanes 2016-11-02 16:11:37 +01:00
  • 3321f556d6 Better way of keeping track of local hyps Guillaume Bury 2016-10-19 17:09:13 +02:00
  • e6f3e79acc [bugfix] Grow heap when adding local hyps Guillaume Bury 2016-10-19 17:07:19 +02:00
  • 64af636341 [doc] Updated inference rules Guillaume Bury 2016-10-18 19:10:31 +02:00
  • f237851e89 Added Model definitions in msat doc Guillaume Bury 2016-10-18 17:39:10 +02:00
  • ee2a80bc4f [wip] Documentation update Guillaume Bury 2016-10-14 14:12:29 +02:00
  • ff6e9cb8f0 [wip] adding documentation about msat Guillaume Bury 2016-10-12 19:11:08 +02:00
  • f35d3a9f23 Fixed uninterpreted predicates for mcsat solver Guillaume Bury 2016-09-23 15:57:38 +02:00
  • 1656995097 Added uninterpreted functions to mcsat solver Guillaume Bury 2016-09-23 15:39:23 +02:00
  • 4fae86c81d Fixed typo in smt typechecker Guillaume Bury 2016-09-23 14:02:12 +02:00
  • 88b8c9f895 Optimisation for mcsat solver Guillaume Bury 2016-09-23 13:30:51 +02:00
  • 41f1ec0e82 For travis, dolmen is now pinned to github/dev version Guillaume Bury 2016-09-23 13:30:19 +02:00
  • 9cf13bd7a2 Mcsat now works (for pure equality problems) Guillaume Bury 2016-09-22 18:31:22 +02:00
  • 4f5bb640ca [WIP] All is setup, remains to have real theories Guillaume Bury 2016-09-16 15:49:33 +02:00
  • 2a33534312 Added (dummy) mcsat module for test binary Guillaume Bury 2016-09-14 19:55:57 +02:00
  • 4522aa3ddc Removed Expr module from msat lib Guillaume Bury 2016-09-12 17:54:10 +02:00
  • a0d8bd5457 Added dolmen dependency Guillaume Bury 2016-09-12 17:11:05 +02:00
  • 0631135bd5 Smt solver with dummy theory now builds Guillaume Bury 2016-09-12 15:43:57 +02:00
  • fa8957784a Restored simple expressions for pure SAT Guillaume Bury 2016-09-12 15:37:06 +02:00
  • dfff903f8c Removed additional libs. Guillaume Bury 2016-09-12 15:32:22 +02:00
  • 9baa3f0716 fix bug in add_clause Simon Cruanes 2016-09-12 10:38:13 +02:00
  • 1751f71f83 wip wip-no-simps Simon Cruanes 2016-09-12 10:30:56 +02:00
  • 68e6740fe3 wip Simon Cruanes 2016-09-12 09:50:45 +02:00
  • dc8371547d wip: remove simplifications Simon Cruanes 2016-09-11 17:43:54 +02:00
  • 9d509241ad [WIP] Some drastic cleanup of code Guillaume Bury 2016-09-09 18:09:04 +02:00
  • 954892ac4a [WIP] Strange compiler bug Guillaume Bury 2016-09-09 12:07:13 +02:00
  • 742f8c469d Added Expr and typing module from ArchSat Guillaume Bury 2016-09-07 17:58:07 +02:00
  • 18a3478926 Give access to the trail Guillaume Bury 2016-09-06 14:29:25 +02:00
  • bb2c931d68 wip Simon Cruanes 2016-08-24 18:23:01 +02:00
  • 9eee458c2a External.assume no longer needs to catch Unsat Guillaume Bury 2016-08-19 01:06:22 +02:00
  • 119f3a8566 New function to export a problem to dimacs format Guillaume Bury 2016-08-18 18:19:14 +02:00
  • 56f98d9a82 Explicit status for local assumption clauses Guillaume Bury 2016-08-17 19:20:05 +02:00
  • 41557a1509 wip: make SMT great again Simon Cruanes 2016-08-16 17:20:48 +02:00
  • 035002fd95 Add forgetful propagation wip-propagation Guillaume Bury 2016-08-04 22:18:39 +02:00
  • ec6ced9809 Unify analyze code for sat and mcsat Guillaume Bury 2016-08-04 22:16:52 +02:00
  • 7d57b3f1b5 Accept late conflict clauses, closes #4 Guillaume Bury 2016-08-04 21:31:51 +02:00
  • 12fed8a811 do not ask for comparison on terms and formulas Simon Cruanes 2016-08-03 20:25:08 +02:00
  • 66707b58fc optimize Vec.{get,set} Simon Cruanes 2016-07-29 23:43:06 +02:00
  • 6f54604dc9 Optim for non-mcsat solvers Guillaume Bury 2016-07-29 23:20:31 +02:00
  • 7016bb1825 add an inlining parameter for non-flambda versions of OCaml Simon Cruanes 2016-07-29 22:55:26 +02:00
  • af55371eb4 change the caching mechanism for var's assignable subterms Simon Cruanes 2016-07-29 22:50:37 +02:00
  • c70c102de9 optim in a bottleneck in Vec Simon Cruanes 2016-07-29 22:50:26 +02:00
  • d30797c1c1 expose a way for theories to bump literal activity (heuristics) wip-expose-bump-lit Simon Cruanes 2016-07-26 20:19:13 +02:00
  • 5fdffe1f85 Handle new clauses unsat at level >0 && <=base_lvl Guillaume Bury 2016-07-29 21:00:24 +02:00
  • 6eeaa8513c fix bug Simon Cruanes 2016-07-29 20:45:30 +02:00
  • 85c290c0ce small changes Simon Cruanes 2016-07-29 20:04:54 +02:00
  • 672b5945ce expose true_at_level0 in Solver_intf Simon Cruanes 2016-07-29 17:07:54 +02:00
  • 9d6634d621 Better interface for Msat.Internal Guillaume Bury 2016-07-29 15:45:24 +02:00
  • 38a6d8c481 small fix Simon Cruanes 2016-07-29 15:11:53 +02:00
  • bc200474eb Simpler code for clause simplification Guillaume Bury 2016-07-29 13:36:05 +02:00
  • a32b35e994 Fix proofs with local assumptions Guillaume Bury 2016-07-29 13:35:05 +02:00
  • 51c76479b9 Better logging in proofs Guillaume Bury 2016-07-29 12:58:21 +02:00
  • d6c6331d85 check proofs in test_api Simon Cruanes 2016-07-28 11:10:31 +02:00
  • 5a04fa49ed for proofs, represent assumptions as propagations Simon Cruanes 2016-07-28 10:56:19 +02:00
  • eb14a1e229 fix Simon Cruanes 2016-07-28 10:47:59 +02:00
  • ac706f3e56 fix bug Simon Cruanes 2016-07-28 10:18:07 +02:00
  • 2e8b45edbc many small changes Simon Cruanes 2016-07-28 00:51:36 +02:00
  • 09b13be78d reflect test_api result in its errcode Simon Cruanes 2016-07-27 23:24:01 +02:00
  • 98d5074da6 updates to tests Simon Cruanes 2016-07-27 19:09:11 +02:00
  • 3e54fac7f9 add some tests for the API Simon Cruanes 2016-07-27 18:52:48 +02:00
  • 73c2500b05 allow propagation of lits under base_level Simon Cruanes 2016-07-27 18:16:26 +02:00
  • 3e9c0d3a1e forgot to pop before assume Simon Cruanes 2016-07-27 17:58:15 +02:00
  • 563e9027e1 first draft of replacing push/pop by assumptions Simon Cruanes 2016-07-27 16:40:36 +02:00
  • 09166d0370 Removed Stack.fold for compat with ocaml < 4.03 Guillaume Bury 2016-07-26 15:35:22 +02:00
  • 3c6da0ffdc Clause buffer must be fitered when popping Guillaume Bury 2016-07-26 14:27:22 +02:00
  • defcb67aad Use a buffer for adding clauses (to avoid exceptions) Guillaume Bury 2016-07-26 14:22:32 +02:00