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

  • 2bba885266 Prevent semantic propagations at level 0 Guillaume Bury 2018-07-24 23:42:20 +02:00
  • 8cdfe65048 Merge branch 'master' of github.com:Gbury/mSAT Guillaume Bury 2018-07-24 23:02:59 +02:00
  • a5eeaa0edc Propagate consequences at the lowest level possible Guillaume Bury 2018-07-24 21:57:12 +02:00
  • 354f2013b1 Add assertion to check theory conflict clauses Guillaume Bury 2018-07-24 21:51:04 +02:00
  • bf0b5185bd fix: proper proof for clause deduplication Simon Cruanes 2018-07-10 13:54:02 -05:00
  • 74cd2009a3 refactor: small changes Simon Cruanes 2018-07-02 18:55:36 -05:00
  • 54a6a2cc2e update todo Simon Cruanes 2018-07-02 17:38:11 -05:00
  • bf70f9688d refactor(cc): merge the two task queues Simon Cruanes 2018-06-27 21:43:15 -05:00
  • b7518a632a refactor(cc): simplify congruence closure Simon Cruanes 2018-06-27 21:38:16 -05:00
  • fb713aa171 fix(cc): update terms properly Simon Cruanes 2018-06-22 21:28:26 -05:00
  • 0931747404 refactor(cc): better handling of terms that should be ignored by CC Simon Cruanes 2018-06-22 21:02:07 -05:00
  • c125fdafa6 fix(sat): use Conflict exn to signal conflict on add_clause Simon Cruanes 2018-06-22 21:01:22 -05:00
  • 9ac274fc09 refactor: simplify literals; remove useless casts in CC; bit for pending nodes Simon Cruanes 2018-06-22 19:38:04 -05:00
  • b12db3f03e chore: fix travis, only build on >= 4.03 Simon Cruanes 2018-06-17 14:34:18 -05:00
  • 225afb624e fix: add missig module Value Simon Cruanes 2018-06-17 14:26:07 -05:00
  • 83edbe7b48 fix(build): make menhir+zarith mandatory deps Simon Cruanes 2018-06-17 13:40:47 -05:00
  • eec7fdca2b chore: update travis script to use docker Simon Cruanes 2018-06-17 12:32:01 -05:00
  • 6933a7b5d0 refactor: add reset_tasks function to clear caches on backtrack Simon Cruanes 2018-06-16 22:50:03 -05:00
  • c8ca60461a fix: typo in Th_bool Simon Cruanes 2018-06-16 20:47:23 -05:00
  • 1f79809644 fix(cc.model): model building needs special case for bool Simon Cruanes 2018-06-11 21:56:50 -05:00
  • c5f23e32b9 test: proper smtlib for QFUF problems Simon Cruanes 2018-06-11 21:56:34 -05:00
  • 5e380464ce fix(sat): base-level = 1 under assumptions Simon Cruanes 2018-06-11 21:47:37 -05:00
  • 080cde778e feat(model): proper model construction for CC + fun interpretation Simon Cruanes 2018-06-11 20:57:19 -05:00
  • 0425ce6206 Fix typo in the pigeon hole test description Cedric Cellier 2018-06-02 14:36:02 +02:00
  • f3c02ebd58 wip: implement model construction and evaluation Simon Cruanes 2018-05-28 02:43:31 -05:00
  • 20ecdd6c1f remove useless fields Simon Cruanes 2018-05-28 01:31:34 -05:00
  • 10d394a9c3 fix(cc): public add function must also saturate CC Simon Cruanes 2018-05-28 01:22:58 -05:00
  • 1d99547856 rename dir Simon Cruanes 2018-05-26 10:34:12 -05:00
  • cac216da20 fix(cc): update handling of signature table (point to node, not repr) Simon Cruanes 2018-05-26 00:46:27 -05:00
  • aac7879b9d wip: fix CC for theory terms Simon Cruanes 2018-05-26 00:04:41 -05:00
  • 04f25779fa refactor(term): much simpler term model, without builtins or typeclass Simon Cruanes 2018-05-25 23:43:04 -05:00
  • 0b42a34a20 refactor: cleanup SAT Simon Cruanes 2018-05-25 21:32:29 -05:00
  • 9b8c21513a refactor: internalize terms earlier Simon Cruanes 2018-05-25 21:32:24 -05:00
  • 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