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

  • 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
  • 0883615b99 Replaced Either.destruct by explicit matching Guillaume Bury 2016-03-04 15:50:13 +01:00
  • ea518c6ab3 Update for compatibility with ocaml 4.00.1 Guillaume Bury 2016-02-29 13:43:46 +01:00
  • 6ea66dcffe v0.2 release Guillaume Bury 2016-02-29 11:15:05 +01:00
  • b6effe691c Added dummy arguments to some functors Guillaume Bury 2016-02-29 10:54:17 +01:00
  • a6a44445c7 Small update to tool doc Guillaume Bury 2016-02-12 14:08:27 +01:00
  • 94ce8dbd25 Fixed push/pop base level and reset function to do what is said in doc Guillaume Bury 2016-02-05 14:32:41 +01:00
  • 6f02ace5e3 Fixed documentation generation Guillaume Bury 2016-02-05 14:32:31 +01:00
  • e58cfe1c8f Added function to print unsat core in dimacs format Guillaume Bury 2016-02-05 14:30:47 +01:00
  • a2809215ae Update the binary for better output when checking proofs Guillaume Bury 2016-02-04 23:51:53 +01:00
  • 74be6cdc9f Changed timeout message in binary Guillaume Bury 2016-01-31 14:33:51 +01:00
  • ce65f10f9c Big cleanup of interfaces. Breaks retro-compat ! Guillaume Bury 2016-01-31 02:09:16 +01:00
  • beff9ee7c1 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2016-01-30 17:04:23 +01:00
  • 30842da947 Fixed refreshing of clauses with push/pop Guillaume Bury 2016-01-30 17:03:14 +01:00
  • cb8092af3b Cleaned makefile a bit + moved the testing binary Guillaume Bury 2016-01-30 17:02:24 +01:00
  • 60250f2611 add UndecidedLit for eval, eval_level Simon Cruanes 2016-01-29 17:00:05 +01:00
  • f088ef73e1 expose tag_clause in Solver.Make Simon Cruanes 2016-01-29 14:59:48 +01:00
  • f348dcd5ae expose dummy theory in a functor Simon Cruanes 2016-01-29 14:40:43 +01:00
  • e8162fdaf4 details Simon Cruanes 2016-01-29 14:34:45 +01:00
  • 383afcf19f Update README after Log switch Guillaume Bury 2016-01-21 17:19:24 +01:00
  • ddbedc6606 Better unsat_core Guillaume Bury 2016-01-21 16:39:35 +01:00
  • ea1a360148 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2016-01-21 03:52:53 +01:00
  • 9a481f6450 Better proofs Guillaume Bury 2016-01-21 03:34:18 +01:00
  • 2613926ab1 First changes for better persistent proofs Guillaume Bury 2016-01-21 00:06:41 +01:00
  • 756363ffd6 everwhere, use new Log interface and remove the functor on Log_intf Simon Cruanes 2016-01-20 21:05:22 +01:00
  • 2fe5be8317 update Log interface, with real/dummy implementation Simon Cruanes 2016-01-20 21:03:34 +01:00
  • 6e5d737b42 get rid of dependency on unix Simon Cruanes 2016-01-20 20:13:32 +01:00
  • facfe336a1 add eval_level in the API of the SAT solver Simon Cruanes 2016-01-20 20:06:56 +01:00
  • a21807c624 Fix for semantic conflict and decision levels Guillaume Bury 2015-12-11 16:26:51 +01:00
  • df1f28ccb1 Fix for when the solver becomes unsat during if_sat Guillaume Bury 2015-12-11 09:08:10 +01:00
  • 1d1ba51329 Fixed some bugs related to push/pop and propagation Guillaume Bury 2015-12-08 15:58:49 +01:00
  • 3168d4ae2b Fixed bug in if_sat Guillaume Bury 2015-12-08 13:11:05 +01:00
  • 9f421e6b1d Added package name to opam file Guillaume Bury 2015-11-30 15:49:53 +01:00
  • 3f1d9fead6 Prepare for opam release Guillaume Bury 2015-11-27 18:13:10 +01:00