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

  • 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
  • c45fe97ebd micro optim on Vec Simon Cruanes 2016-07-25 13:44:22 +02:00
  • 6757910225 [travis] Ubuntu doesn't have 'time' by default... Guillaume Bury 2016-07-23 14:47:52 +02:00
  • e266134efc Try a different source for opam package in travis Guillaume Bury 2016-07-23 14:39:33 +02:00
  • e2530a25b7 Forgot to remove the sudo:required Guillaume Bury 2016-07-23 14:36:19 +02:00
  • b5f8c7ddf9 Use travis apt addon to install opam Guillaume Bury 2016-07-23 14:35:23 +02:00
  • 202249d75e Remove travis-ci script. Guillaume Bury 2016-07-23 14:22:14 +02:00
  • a0b810f520 Add travis build status to README Guillaume Bury 2016-07-23 14:07:40 +02:00
  • 0a4b812924 Moved more commands in before_install for travis Guillaume Bury 2016-07-23 13:58:45 +02:00
  • 13effa8969 Cleaner way to install opam in travis CI Guillaume Bury 2016-07-23 13:50:13 +02:00
  • fda7b9ef3a Missing env var in travis-ci script Guillaume Bury 2016-07-23 13:32:06 +02:00
  • 33735b5e50 Missing sudo requirement in travis.yml Guillaume Bury 2016-07-23 13:29:25 +02:00
  • f957eb4e0c Added ocaml 4.03.0 to travis CI Guillaume Bury 2016-07-23 13:26:44 +02:00
  • ec4fd911a9 Fixed typo in travis.yml Guillaume Bury 2016-07-23 13:25:50 +02:00
  • 54ba6bc745 Added travis CI Guillaume Bury 2016-07-23 13:23:36 +02:00
  • 3e30a77569 Some more comments Guillaume Bury 2016-07-22 17:27:50 +02:00
  • c4beb7054b spurious assertion Simon Cruanes 2016-07-22 16:51:45 +02:00
  • 895cb9cbfb some additional comments and cleanup Simon Cruanes 2016-07-22 16:40:22 +02:00
  • 891f764ee8 some more cleanup Simon Cruanes 2016-07-22 16:31:00 +02:00
  • c3cfe67696 cleanup boolean propagation Simon Cruanes 2016-07-22 16:00:02 +02:00
  • c1915ba2d3 wip: cleanup and documentation of internal.ml Simon Cruanes 2016-07-22 15:42:17 +02:00
  • 8b1d657695 remove Either Simon Cruanes 2016-07-22 13:19:16 +02:00
  • 51f10d7ad5 update some files Simon Cruanes 2016-07-22 11:30:47 +02:00
  • e251799f8e add some array utils for pre-4.03 compat Simon Cruanes 2016-07-22 11:25:00 +02:00
  • 216ca82fe7 Ensure pushed clauses are added after if_sat slice Guillaume Bury 2016-07-20 11:45:13 +02:00
  • d1ebc59856 Avoid unnecessary atoms array to list conversions Guillaume Bury 2016-07-18 18:49:28 +02:00
  • 38b4fde5c1 Clause atoms are now in an array instead of a vec Guillaume Bury 2016-07-18 18:42:15 +02:00
  • 933943c4e3 Merge branch '0.3.1' Guillaume Bury 2016-07-18 18:13:48 +02:00
  • 9dadb67fc9 [bugfix] Sort false atoms by levels in new clauses Guillaume Bury 2016-07-16 15:55:26 +02:00
  • 1acecc0815 Small printing upgrades Guillaume Bury 2016-07-13 18:14:23 +02:00
  • 2ff1279f26 Better perfs for unsat_core Guillaume Bury 2016-07-13 17:44:04 +02:00
  • ef49d5eaaa Slightly better formatting for clause printing Guillaume Bury 2016-07-13 17:07:03 +02:00
  • c159a60d9b Better premises for clauses Guillaume Bury 2016-07-13 16:43:01 +02:00
  • 245941efdb Remember more added clauses Guillaume Bury 2016-07-13 16:23:34 +02:00
  • 9be4c66911 [bugfix] Clause level now computed at creation Guillaume Bury 2016-07-09 03:06:21 +02:00
  • dcc410c8a0 Added stack to delay adding of pushed clauses Guillaume Bury 2016-07-08 17:54:29 +02:00
  • 510a8aaa34 [bugfix] Clause level now computed at creation Guillaume Bury 2016-07-09 03:06:21 +02:00
  • 291a9d9a7f tags Simon Cruanes 2016-07-09 00:36:37 +02:00
  • eba84fba42 Aliased def of negated in Expr_intf Guillaume Bury 2016-07-08 17:34:46 +02:00
  • b56e4e3355 Added if_sat to Theory_intf Guillaume Bury 2016-07-08 16:15:05 +02:00
  • eb2850caa6 Moved some type def outside Plugins/Theories Guillaume Bury 2016-07-08 14:29:45 +02:00
  • 46b621269c Merlin update Guillaume Bury 2016-07-08 14:29:36 +02:00
  • bbbc29948d Added src directory, moved some files around Guillaume Bury 2016-07-07 15:48:50 +02:00
  • 599a59dda9 Removed unused modules Guillaume Bury 2016-07-07 14:55:48 +02:00
  • 6e6503e793 cleanup: remove labels, use a sum type for negated formulas Simon Cruanes 2016-07-01 15:48:21 +02:00
  • 403347ddaf avoid duplicating the definition of slices in Theory_intf Simon Cruanes 2016-07-01 15:25:10 +02:00
  • 66740e5de8 Adding documentation comments in Internal Guillaume Bury 2016-07-01 12:07:49 +02:00
  • 34b1cda760 Updated README Guillaume Bury 2016-07-01 09:34:34 +02:00
  • 553d320368 Fixed compilation. Refactored some code in external Guillaume Bury 2016-06-30 09:54:21 +02:00
  • 49267897e8 Fixed bad tabls in dot backend Guillaume Bury 2016-06-29 21:25:53 +02:00
  • f19c6b9b77 Fixed dot printing bug Guillaume Bury 2016-06-26 18:49:21 +02:00
  • 1e2dc299ce WIP: add dedukti output (not functional yet) Guillaume Bury 2016-05-20 17:03:22 +02:00
  • d06de43789 Removed color flag (because ocaml < 4.03) Guillaume Bury 2016-05-20 16:26:03 +02:00
  • 6d706f55e5 Tags update + optimizations for ocaml 4.03 Guillaume Bury 2016-05-20 16:21:06 +02:00
  • fd4d52b7a6 Better syntax for functor signature in solver_types Guillaume Bury 2016-04-24 14:14:46 +02:00
  • 1a0fc95147 Fixed functor syntax for ocaml 4.00.1 in solver_types Guillaume Bury 2016-04-23 20:18:25 +02:00
  • 22ebead17a missing change Simon Cruanes 2016-04-15 14:05:42 +02:00
  • 1ce3973f9e [feature] Allow arbitrary proof types in DummyTheory Guillaume Bury 2016-04-15 14:02:18 +02:00
  • 2e6ff522e5 Update to Msat.Solver arguments in readme Guillaume Bury 2016-04-15 13:41:41 +02:00
  • e3fc66919d Put info about Msat.Solver higher in the readme Guillaume Bury 2016-04-15 13:39:09 +02:00
  • f88a5dd514 [bugfix/minor] Ensure generativity of solver_types Guillaume Bury 2016-04-15 13:30:46 +02:00
  • dcde8de10d [bugfix/medium] Fixed printing of the new reasons Guillaume Bury 2016-04-15 13:30:20 +02:00
  • 63d8dc1dc2 [bugfix/major] Clauses can be added at level > 0 Guillaume Bury 2016-04-15 12:49:38 +02:00
  • ec7c6602e9 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2016-04-15 12:11:38 +02:00
  • 815098dde4 Propagation reasons are now far more explicit Guillaume Bury 2016-04-15 12:09:23 +02:00
  • 479f4c1b79 small checks Simon Cruanes 2016-04-15 11:54:00 +02:00
  • 0186edbf34 [feature] Adds proofs for atoms true at level 0 Guillaume Bury 2016-04-06 15:32:12 +02:00
  • 9a5c23d9c5 [bugfix] termination check after full slice was wrong Guillaume Bury 2016-03-04 16:30:51 +01:00