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

Commit graph

  • 2b1bef9e3c ocpindent config Simon Cruanes 2017-12-28 18:55:01 +01:00
  • b92d8b39e7 remove useless dir Simon Cruanes 2017-12-28 18:48:21 +01:00
  • f5b4f5d0cb update opam files Simon Cruanes 2017-12-28 18:14:32 +01:00
  • d9ceba72d4 cleanup in fields Simon Cruanes 2017-12-28 18:03:00 +01:00
  • cb45782eed travis Simon Cruanes 2017-12-28 17:33:03 +01:00
  • a978ec97a3 update travis Simon Cruanes 2017-12-28 16:08:49 +01:00
  • ec7fa9e01a fix warnings Simon Cruanes 2017-12-28 16:02:47 +01:00
  • 2707215aa2 move tseitin transformation into its own lib Simon Cruanes 2017-12-28 16:01:36 +01:00
  • f64a1556b1 details Simon Cruanes 2017-12-28 15:55:00 +01:00
  • 768f59f88b big refactoring Simon Cruanes 2017-12-28 15:51:04 +01:00
  • 48ec2d732c capitalization of files; add new Log Simon Cruanes 2017-12-28 14:03:23 +01:00
  • 9e5c9056d0 test: add a logitest target Simon Cruanes 2019-02-10 18:07:06 -06:00
  • 8614d9bb0c feat: use gc alarm to check resources Simon Cruanes 2019-02-10 17:11:29 -06:00
  • 26b4f677e0 test: update some tests Simon Cruanes 2019-02-10 17:00:38 -06:00
  • 5865151247 refactor: return optional proof, do not store if if -no-check was given Simon Cruanes 2019-02-10 16:59:27 -06:00
  • 62ea8fd0cb fix(thbool): fix non-termination issue by creating clauses at most once Simon Cruanes 2019-02-10 16:24:04 -06:00
  • b5208da56c fix(tseitin): use final check to push axioms Simon Cruanes 2019-02-09 23:35:49 -06:00
  • bf0171fec1 fix(cc): merge parents properly Simon Cruanes 2019-02-09 22:11:50 -06:00
  • 1328d043e3 fix(cc): restore distinct Simon Cruanes 2019-02-09 21:59:25 -06:00
  • a463dbb4b5 feat(cc): split sub-library sidekick.cc, make it fully functorized Simon Cruanes 2019-02-09 20:24:29 -06:00
  • de1653bdcc chore: remove ocamlinit file Simon Cruanes 2019-02-09 16:43:37 -06:00
  • 431d8fe4ac small style change Simon Cruanes 2019-02-09 16:17:15 -06:00
  • 9d90b7ef66 refactor(cc): add some todos, fix a bug Simon Cruanes 2019-02-09 16:17:01 -06:00
  • 7b00a9d9e5 feat: expose mini-cc compatible API in Term Simon Cruanes 2019-02-09 16:16:44 -06:00
  • 40186a6c76 refactor: renaming `Eq{uiv,}_class Simon Cruanes 2019-02-08 19:45:20 -06:00
  • 0326c07c16 refactor: add Sidekick_util with some re-exports Simon Cruanes 2019-02-08 19:44:59 -06:00
  • a7a5e1d7e1 wip: mini congruence closure to check the main one Simon Cruanes 2019-02-08 19:44:39 -06:00
  • f2eecaa758 feat(th-bool): flattening of and/or also removes neutral elts Simon Cruanes 2019-02-01 21:42:44 -06:00
  • f76f6bb0d9 feat(solver): assert true and ¬false Simon Cruanes 2019-02-01 21:42:28 -06:00
  • e08bb7b5ac fix(cc): polarity error in distinct-conflict Simon Cruanes 2019-02-01 21:42:11 -06:00
  • 3eabeb4e2e fix(bstack): another stupid error Simon Cruanes 2019-02-01 21:41:54 -06:00
  • d95047b65a refactor: a debug msg Simon Cruanes 2019-02-01 21:26:32 -06:00
  • 91389d2b5e fix(bstack): fix bug in n-levels Simon Cruanes 2019-02-01 21:25:50 -06:00
  • a2e177abe8 fix(cc): polarity error in conflicts Simon Cruanes 2019-02-01 21:12:08 -06:00
  • e6de1de949 main: print backtraces properly Simon Cruanes 2019-02-01 21:12:00 -06:00
  • 668bd36311 test: remove API test, which belongs in msat Simon Cruanes 2019-02-01 21:01:06 -06:00
  • 3f24e9cfe3 fix (tmp): in travis, pin msat's branch Simon Cruanes 2019-02-01 20:59:00 -06:00
  • 1c8c22fc63 chore: faster recompilation on travis Simon Cruanes 2019-02-01 20:58:24 -06:00
  • a57fdcdeda refactor: use msat 0.8 Simon Cruanes 2019-02-01 20:57:44 -06:00
  • 27d1841f6b wip: migrate to msat 0.8 Simon Cruanes 2019-01-28 21:09:57 -06:00
  • 4fadbeb04d chore: migrate to dune Simon Cruanes 2019-01-18 18:32:23 -06:00
  • 4bb1f5b793 Update for latest version of dolmen Guillaume Bury 2018-09-11 14:19:37 +02:00
  • 5e57bfc827 Bugfix for user lvl push when already unsat Guillaume Bury 2018-09-11 14:19:22 +02:00
  • 73c7db2b4e feat(cc): boolean propagation of literals in CC Simon Cruanes 2018-08-18 19:56:22 -05:00
  • 0e467e058c fix: disable checking of invariants Simon Cruanes 2018-08-18 19:56:12 -05:00
  • c1a662e2c8 refactor(sat): improve style of theory propagation handler Simon Cruanes 2018-08-18 19:55:30 -05:00
  • 324c9d2e36 fix(sat): allow proofs with unary resolution history Simon Cruanes 2018-08-18 19:54:46 -05:00
  • 400f2e02f1 refactor(th-combine): simplify handling of theory conflicts Simon Cruanes 2018-08-18 18:55:17 -05:00
  • dd58fa21ef fix(sat): fix bug in restarts, we need to solve again after one Simon Cruanes 2018-08-18 18:08:42 -05:00
  • ca531d73a6 refactor(cc): fix bugs, use list of nodes in equiv class Simon Cruanes 2018-08-18 18:06:16 -05:00
  • c2d79b2e6a fix(main): properly handle option no-restarts Simon Cruanes 2018-08-18 18:04:56 -05:00
  • e6a96df0d9 chore: remove dead code in sat Simon Cruanes 2018-08-18 17:47:20 -05:00
  • 72750b9e1a fix(sat): bugfix about adding clauses with true lits Simon Cruanes 2018-08-18 17:47:04 -05:00
  • 46ff8c3ba6 fix(sat): bug with re-internalization of terms upon backtracking Simon Cruanes 2018-08-18 17:20:20 -05:00
  • 162b6fad98 refactor(term): notion of is_value, which are kept as representatives Simon Cruanes 2018-08-18 17:19:50 -05:00
  • 04eea28cfc chore: disable some warning in Solver Simon Cruanes 2018-08-18 16:39:38 -05:00
  • 2b2765c67f chore: debug msg Simon Cruanes 2018-08-18 15:04:29 -05:00
  • 8ea844a5a0 chore: improve debug msg in check invariants Simon Cruanes 2018-08-18 15:02:44 -05:00
  • d5ca5c2c81 chore: minor debug msg Simon Cruanes 2018-08-18 14:56:28 -05:00
  • 6d2d1c91e8 refactor(cc): disable path compression Simon Cruanes 2018-08-18 14:52:00 -05:00
  • 1d212350ef refactor(cc): internal refactorings Simon Cruanes 2018-08-18 14:51:49 -05:00
  • b8445d0ca3 refactor: introduce check_invariants in CC Simon Cruanes 2018-08-18 14:50:03 -05:00
  • ce9bcb234d refactor(term): printing utils Simon Cruanes 2018-08-18 14:47:39 -05:00
  • 446690eb11 chore: rename main symlink Simon Cruanes 2018-08-18 13:22:28 -05:00
  • a88f0d62f4 fix(typecheck): support application of function symbols Simon Cruanes 2018-08-18 13:22:10 -05:00
  • ea9f374a7a perf(vec): minor improvements to Vec Simon Cruanes 2018-08-18 13:14:36 -05:00
  • c9ab548a5a detail in debug Simon Cruanes 2018-08-17 14:22:36 -05:00
  • 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