simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
694 commits 53 branches 1 tag 17 MiB
Commit graph

694 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
e6de1de949 main: print backtraces properly 2019-02-01 21:12:26 -06:00
Simon Cruanes
668bd36311 test: remove API test, which belongs in msat 2019-02-01 21:12:26 -06:00
Simon Cruanes
3f24e9cfe3 fix (tmp): in travis, pin msat's branch 2019-02-01 21:12:26 -06:00
Simon Cruanes
1c8c22fc63 chore: faster recompilation on travis 2019-02-01 20:58:24 -06:00
Simon Cruanes
a57fdcdeda refactor: use msat 0.8 2019-02-01 20:57:44 -06:00
Simon Cruanes
27d1841f6b wip: migrate to msat 0.8 2019-01-28 21:09:57 -06:00
Simon Cruanes
4fadbeb04d chore: migrate to dune 2019-01-18 18:37:26 -06:00
Simon Cruanes
73c7db2b4e feat(cc): boolean propagation of literals in CC 2018-08-18 19:56:22 -05:00
Simon Cruanes
0e467e058c fix: disable checking of invariants 2018-08-18 19:56:12 -05:00
Simon Cruanes
c1a662e2c8 refactor(sat): improve style of theory propagation handler 2018-08-18 19:55:30 -05:00
Simon Cruanes
324c9d2e36 fix(sat): allow proofs with unary resolution history 
can happen if the conflict clause is a theory lemma
 2018-08-18 19:54:46 -05:00
Simon Cruanes
400f2e02f1 refactor(th-combine): simplify handling of theory conflicts 2018-08-18 18:55:17 -05:00
Simon Cruanes
dd58fa21ef fix(sat): fix bug in restarts, we need to solve again after one 2018-08-18 18:08:42 -05:00
Simon Cruanes
ca531d73a6 refactor(cc): fix bugs, use list of nodes in equiv class 2018-08-18 18:06:16 -05:00
Simon Cruanes
c2d79b2e6a fix(main): properly handle option no-restarts 2018-08-18 18:05:22 -05:00
Simon Cruanes
e6a96df0d9 chore: remove dead code in sat 2018-08-18 17:47:20 -05:00
Simon Cruanes
72750b9e1a fix(sat): bugfix about adding clauses with true lits 2018-08-18 17:47:04 -05:00
Simon Cruanes
46ff8c3ba6 fix(sat): bug with re-internalization of terms upon backtracking 2018-08-18 17:20:20 -05:00
Simon Cruanes
162b6fad98 refactor(term): notion of is_value, which are kept as representatives 2018-08-18 17:19:50 -05:00
Simon Cruanes
04eea28cfc chore: disable some warning in Solver 2018-08-18 16:39:38 -05:00
Simon Cruanes
2b2765c67f chore: debug msg 2018-08-18 15:04:29 -05:00
Simon Cruanes
8ea844a5a0 chore: improve debug msg in check invariants 2018-08-18 15:02:44 -05:00
Simon Cruanes
d5ca5c2c81 chore: minor debug msg 2018-08-18 14:56:28 -05:00
Simon Cruanes
6d2d1c91e8 refactor(cc): disable path compression 2018-08-18 14:52:44 -05:00
Simon Cruanes
1d212350ef refactor(cc): internal refactorings 2018-08-18 14:52:44 -05:00
Simon Cruanes
b8445d0ca3 refactor: introduce check_invariants in CC 
costly, but helps find bugs
 2018-08-18 14:52:44 -05:00
Simon Cruanes
ce9bcb234d refactor(term): printing utils 2018-08-18 14:52:44 -05:00
Simon Cruanes
446690eb11 chore: rename main symlink 2018-08-18 13:22:28 -05:00
Simon Cruanes
a88f0d62f4 fix(typecheck): support application of function symbols 2018-08-18 13:22:10 -05:00
Simon Cruanes
ea9f374a7a perf(vec): minor improvements to Vec 2018-08-18 13:14:36 -05:00
Simon Cruanes
c9ab548a5a detail in debug 2018-08-17 14:22:36 -05:00
Simon Cruanes
bf0b5185bd fix: proper proof for clause deduplication 2018-07-10 13:54:02 -05:00
Simon Cruanes
74cd2009a3 refactor: small changes 2018-07-02 18:55:36 -05:00
Simon Cruanes
bf70f9688d refactor(cc): merge the two task queues 2018-06-27 21:43:15 -05:00
Simon Cruanes
b7518a632a refactor(cc): simplify congruence closure 2018-06-27 21:38:16 -05:00
Simon Cruanes
fb713aa171 fix(cc): update terms properly 2018-06-22 21:28:26 -05:00
Simon Cruanes
0931747404 refactor(cc): better handling of terms that should be ignored by CC 2018-06-22 21:02:07 -05:00
Simon Cruanes
c125fdafa6 fix(sat): use Conflict exn to signal conflict on add_clause 2018-06-22 21:01:22 -05:00
Simon Cruanes
9ac274fc09 refactor: simplify literals; remove useless casts in CC; bit for pending nodes 2018-06-22 19:38:04 -05:00
Simon Cruanes
b12db3f03e chore: fix travis, only build on >= 4.03 2018-06-17 14:34:18 -05:00
Simon Cruanes
225afb624e fix: add missig module Value 2018-06-17 14:26:07 -05:00
Simon Cruanes
83edbe7b48 fix(build): make menhir+zarith mandatory deps 2018-06-17 13:54:12 -05:00
Simon Cruanes
eec7fdca2b chore: update travis script to use docker 2018-06-17 12:54:16 -05:00
Simon Cruanes
6933a7b5d0 refactor: add reset_tasks function to clear caches on backtrack 
also refactor CC a bit
 2018-06-16 22:50:03 -05:00
Simon Cruanes
c8ca60461a fix: typo in Th_bool 2018-06-16 20:47:23 -05:00
Simon Cruanes
1f79809644 fix(cc.model): model building needs special case for bool 2018-06-11 21:56:50 -05:00
Simon Cruanes
c5f23e32b9 test: proper smtlib for QFUF problems 2018-06-11 21:56:34 -05:00
Simon Cruanes
5e380464ce fix(sat): base-level = 1 under assumptions 2018-06-11 21:47:37 -05:00
Simon Cruanes
080cde778e feat(model): proper model construction for CC + fun interpretation 2018-06-11 21:42:02 -05:00
Simon Cruanes
f3c02ebd58 wip: implement model construction and evaluation 2018-05-28 02:43:31 -05:00