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

Commit graph

  • ea5bce9635 refactor(cc): simplify explanations Simon Cruanes 2018-05-25 20:51:37 -05:00
  • 47ddce5960 refactor: use 1st class for theory actions Simon Cruanes 2018-05-25 20:20:43 -05:00
  • edeb28c8ad refactor(smt): use list of lits as explanations for propagations Simon Cruanes 2018-05-25 19:35:33 -05:00
  • b73e900839 sat: only re-internalize atoms of permanent clauses, on backtrack Simon Cruanes 2018-05-25 19:35:06 -05:00
  • 6302d13fe8 wip: use Lit.Set.t for explanations Simon Cruanes 2018-05-23 22:24:35 -05:00
  • d1c88e73f7 wip: fix main solver Simon Cruanes 2018-05-23 22:24:24 -05:00
  • 39be2c260e fixes Simon Cruanes 2018-05-20 15:32:06 -05:00
  • 208f51276d fix: some fixes in SAT Simon Cruanes 2018-05-20 14:43:33 -05:00
  • fade033458 refactor: get SAT properly again on some problems Simon Cruanes 2018-05-20 14:30:13 -05:00
  • 4a39192846 refactor(sat): wip: simpler clauses Simon Cruanes 2018-05-20 13:38:39 -05:00
  • f69d5cd9f1 refactor(sat): wip: simplify SAT solver Simon Cruanes 2018-05-20 13:09:51 -05:00
  • 5860612cd9 wip: refactor SAT solver Simon Cruanes 2018-05-11 20:33:36 -05:00
  • 3968688a35 large refactor of SAT solver, all internal code in Internal now Simon Cruanes 2018-05-09 22:47:21 -05:00
  • 36df2d952b delay addition of clauses to internal sat solver until solve() Simon Cruanes 2018-05-09 21:09:55 -05:00
  • 186f167885 update doc Simon Cruanes 2018-05-09 20:34:17 -05:00
  • 441ca61465 remove annoying spelling mistake Simon Cruanes 2018-05-09 19:58:04 -05:00
  • c44e9bc16d remove dead library Simon Cruanes 2018-05-09 19:51:45 -05:00
  • 190ee3c503 add dev doc Simon Cruanes 2018-05-09 19:48:25 -05:00
  • 70749155bf cleanup of unused sublibrary Simon Cruanes 2018-05-09 19:34:53 -05:00
  • 4628bff514 remove some files Simon Cruanes 2018-05-09 19:30:44 -05:00
  • 24bbe97ceb rename to sidekick Simon Cruanes 2018-05-09 19:28:41 -05:00
  • eb40cfa5e3 wip Simon Cruanes 2018-05-09 18:14:06 -05:00
  • 1722730e26 Fix typo in doc Guillaume Bury 2018-04-18 11:53:55 +02:00
  • d19b798ee9 add ability to parse and process dimacs files Simon Cruanes 2018-04-11 19:57:51 -05:00
  • d47d619265 add dimacs sub-library Simon Cruanes 2018-04-11 19:57:23 -05:00
  • c82099731d remove todo file Simon Cruanes 2018-04-11 09:03:09 -05:00
  • 6418d3112c add todo file Simon Cruanes 2018-04-11 09:02:54 -05:00
  • da77d3ab3b add todo Simon Cruanes 2018-04-11 09:02:36 -05:00
  • 4e215e3d01 fix(cc): fix bugs in congruence closure and explanations Simon Cruanes 2018-04-02 21:08:03 -05:00
  • bc1a573407 chore: better error printing Simon Cruanes 2018-04-02 21:07:54 -05:00
  • 543f8a5a99 add distinct handling to congruence closure Simon Cruanes 2018-02-23 00:44:23 -06:00
  • dac3378198 improve SAT solver messages, remove semantic reason Simon Cruanes 2018-02-23 00:43:56 -06:00
  • f21d373620 minor refactoring, removing useless field in nodes Simon Cruanes 2018-02-22 21:19:54 -06:00
  • 77af72e739 fix bugs in SAT solver Simon Cruanes 2018-02-19 21:27:26 -06:00
  • 20a85a1f35 th_bool: fix polarity issues Simon Cruanes 2018-02-19 21:27:15 -06:00
  • 2be10fb907 first implementation of on-the-fly Tseitin transformation Simon Cruanes 2018-02-19 20:48:02 -06:00
  • d7fc5cf29d fix problems with slices in the SAT core Simon Cruanes 2018-02-19 20:47:43 -06:00
  • d53bd8671a lower overhead for adding clauses to the SAT solver Simon Cruanes 2018-02-19 19:47:03 -06:00
  • 582f1aad18 improve IArray Simon Cruanes 2018-02-19 19:46:08 -06:00
  • 57591ba042 better normalization of terms in Th_bool Simon Cruanes 2018-02-17 15:33:32 -06:00
  • 9e52183b45 reexport more types in Term Simon Cruanes 2018-02-17 15:33:24 -06:00
  • e1717f3afe wip: heavy refactoring of SAT solver, making most things backtrackable Simon Cruanes 2018-02-11 22:49:33 -06:00
  • fb7e422413 some improvements to Vec Simon Cruanes 2018-02-11 22:40:45 -06:00
  • bc562242c9 add Heap.remove Simon Cruanes 2018-02-11 21:52:31 -06:00
  • dd708b1583 todo Simon Cruanes 2018-02-11 20:42:55 -06:00
  • 2fcef323b3 move back process to dagon_smtlib Simon Cruanes 2018-02-11 10:43:38 -06:00
  • 98934ab74f move boolean builtins to a sublibrary Simon Cruanes 2018-02-08 23:19:18 -06:00
  • 7b44146102 make it compile! with stubs for conversion parse ast -> ast -> term Simon Cruanes 2018-02-08 22:19:32 -06:00
  • f52883f059 update tests Simon Cruanes 2018-02-08 22:19:28 -06:00
  • d73684902f wip: have a proper smtlib parser Simon Cruanes 2018-02-05 23:09:13 -06:00
  • 221ed7dcdb continue large refactoring, progress in theory combination Simon Cruanes 2018-02-01 22:44:40 -06:00
  • 3377d05383 add Shostak solving in CC Simon Cruanes 2018-01-30 22:19:05 -06:00
  • 50fe488dcb refactor types for terms and congruence closure Simon Cruanes 2018-01-30 21:55:37 -06:00
  • 696002bcf7 [travis] Fix faulty conditional for dolmen pinning Guillaume Bury 2018-01-30 17:23:57 +01:00
  • fd75f536fa Fix typo in opam file Guillaume Bury 2018-01-30 17:15:41 +01:00
  • 7cd541b243 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2018-01-30 17:05:19 +01:00
  • 16e6be0c0d [travis] Force installation of dev version Guillaume Bury 2018-01-30 17:04:58 +01:00
  • 2aab43f95d comments and doc Simon Cruanes 2018-01-29 23:37:50 -06:00
  • 25b8c97fa0
         Typo in travis.yml Guillaume Bury 2018-01-29 19:39:13 +01:00
  • 3e50a3fc5d some updates to core lib Simon Cruanes 2018-01-26 21:32:21 -06:00
  • 8821b7767f New shiny travis script + test dep on dolmen.dev Guillaume Bury 2018-01-26 14:20:50 +01:00
  • 14c92bbe31 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2018-01-26 13:50:05 +01:00
  • c8321b4098 Added ICFP presentation in README Guillaume Bury 2018-01-26 13:49:38 +01:00
  • 1d5c1c187c wip: basic SMT infrastructure Simon Cruanes 2018-01-25 23:32:36 -06:00
  • e5e147eaed draft of design doc for the CC Simon Cruanes 2018-01-23 23:08:48 -06:00
  • 9e3484d2b3 update readme Simon Cruanes 2018-01-22 22:14:01 -06:00
  • ac396e8cf5 rename to cdcl Simon Cruanes 2018-01-22 22:09:47 -06:00
  • 8c8209c08c large refactoring to keep only a simpler, easier CDCL(T) interface Simon Cruanes 2018-01-21 18:46:28 -06:00
  • d723aee809 large refactoring to keep only a simpler, easier CDCL(T) interface cdclt Simon Cruanes 2018-01-21 18:46:28 -06:00
  • 7324647fb1 doc msat-refactor Simon Cruanes 2018-01-03 22:08:55 +01:00
  • 53cc8b35a0 more controled API for Res Simon Cruanes 2018-01-03 22:07:40 +01:00
  • 3f4f7ec7e4 a bit of doc Simon Cruanes 2018-01-03 22:01:12 +01:00
  • a9d762673a fix small linter issue in opam Simon Cruanes 2017-12-30 21:10:25 +01:00
  • c7015450a1 typo Simon Cruanes 2017-12-29 22:10:01 +01:00
  • 2caf53c24f expose {push,pop} in main solver Simon Cruanes 2017-12-29 21:29:43 +01:00
  • be929d056a remove useless functions Simon Cruanes 2017-12-29 19:12:17 +01:00
  • d47071c4f0 reinstate better way of picking watch literals Simon Cruanes 2017-12-29 19:00:32 +01:00
  • 70fcded713 reset some record accesses, for perf Simon Cruanes 2017-12-29 18:53:26 +01:00
  • 38b670ebc0 detail Simon Cruanes 2017-12-29 18:35:27 +01:00
  • d415f8ed20 do not expose St in solver, but only expose a restricted API. Simon Cruanes 2017-12-29 18:29:56 +01:00
  • c14f0ba020 make Solver.t more lightweight by removing some useless fields Simon Cruanes 2017-12-29 17:29:24 +01:00
  • a65309d5e6 add optional size argument to create functions Simon Cruanes 2017-12-29 17:24:09 +01:00
  • 99078b2335 make state explicit and add type t state-wrapper in most modules Simon Cruanes 2017-12-29 16:48:26 +01:00
  • 148c1da3cc wip: use submodules of Solver_types to clean up code Simon Cruanes 2017-12-29 15:29:04 +01:00
  • 06af58e6f3 faster addition of clauses' watch literals Simon Cruanes 2017-12-29 12:32:27 +01:00
  • 1592196c72 dependencies in opam files; put binary in minismt package Simon Cruanes 2017-12-28 19:47:05 +01:00
  • 1cd70b048c split some features into minismt lib Simon Cruanes 2017-12-28 19:43:54 +01:00
  • d6c84b93bf restrict what Msat core lib exposes, provide shortcuts Simon Cruanes 2017-12-28 19:23:36 +01:00
  • 1037c06636 use generative functors, remove a layer of nesting for SMT libs Simon Cruanes 2017-12-28 19:12:41 +01:00
  • d4646ffd63 makefile Simon Cruanes 2017-12-28 19:12:32 +01:00
  • b3e9b640f0 ocpindent config Simon Cruanes 2017-12-28 18:55:01 +01:00
  • 4aed7762a7 remove useless dir Simon Cruanes 2017-12-28 18:48:21 +01:00
  • 875efa33c6 update opam files Simon Cruanes 2017-12-28 18:14:32 +01:00
  • db54c8e9b2 cleanup in fields Simon Cruanes 2017-12-28 18:03:00 +01:00
  • d884c9fe41 travis Simon Cruanes 2017-12-28 17:33:03 +01:00
  • 2a3afe7ec1 update travis Simon Cruanes 2017-12-28 16:08:49 +01:00
  • 5e12b26fc0 fix warnings Simon Cruanes 2017-12-28 16:02:47 +01:00
  • 7722319b0a move tseitin transformation into its own lib Simon Cruanes 2017-12-28 16:01:36 +01:00
  • 64d7314aab details Simon Cruanes 2017-12-28 15:55:00 +01:00
  • ac50e10788 big refactoring Simon Cruanes 2017-12-28 15:51:04 +01:00