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

1392 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
632bec0e66 feat: embed micro theories in theories, fix th-distinct 2019-03-22 20:37:30 -05:00
Simon Cruanes
14992f07ec fix: model evaluation must prioritize defined constants' semantics 2019-03-22 20:26:06 -05:00
Simon Cruanes
539186bfe6 feat: modular statistics aggregate 2019-03-22 20:14:28 -05:00
Simon Cruanes
fadf76d944 chore: migrate from sequence to iter 2019-03-22 19:43:05 -05:00
Simon Cruanes
d58759aa8c fix: integrate negation into CC; map boolean subterms to literals 2019-03-22 19:41:05 -05:00
Simon Cruanes
866249deb1 test: add more tests 2019-03-22 18:49:25 -05:00
Simon Cruanes
90eedeaf8d chore: use msat 0.8 in opam 2019-03-22 18:43:21 -05:00
Simon Cruanes
338a84bf3a chore: use iter, not sequence, in dune 2019-03-16 13:54:38 -05:00
Simon Cruanes
9aa4159f2b chore: fix travis 2019-03-10 12:11:59 -05:00
Simon Cruanes
47a7142a3c prepare for 0.8 2019-03-10 11:36:01 -05:00
Simon Cruanes
fb219fb415 refactor: use iter instead of sequence 2019-03-10 11:33:44 -05:00
Simon Cruanes
6e8cedd790 cleanup some files 2019-03-10 11:27:37 -05:00
Simon Cruanes
d3702d1e1f refactor: fix issues found by @gbury 2019-03-10 12:12:39 +01:00
Simon Cruanes
7e9693348a fix: ensure that the mdx test doesn't run too early 2019-03-10 12:12:39 +01:00
Simon Cruanes
2aa9b3d4bc refactor: modifications asked by @gbury in review 2019-03-10 12:12:39 +01:00
Simon Cruanes
7a050df902 fix readme to account for new sudoku output 2019-03-10 12:12:39 +01:00
Simon Cruanes
34f64d2d69 detail: sudoku solver prints total time 2019-03-10 12:12:39 +01:00
Simon Cruanes
5bfd975ed3 refactor: move constant parameters outside of the solver 2019-03-10 12:12:39 +01:00
Simon Cruanes
efe93c3647 feat: Proof.check_empty_conclusion as a separate function 
this allows the validity checking of proofs of 0-level lits
 2019-03-10 12:12:39 +01:00
Simon Cruanes
591298e296 refactor: remove dimacs backend 2019-03-10 12:12:39 +01:00
Simon Cruanes
28afd6eefe fix lazy propagation 2019-03-10 12:12:39 +01:00
Simon Cruanes
ed64e6b69d chore: try to fix the mdx test; cleanup makefile 2019-03-10 12:12:39 +01:00
Simon Cruanes
c2a6c2d47b refactor(propagate): make propagation clause lazy 2019-03-10 12:12:39 +01:00
Simon Cruanes
b1c687faac chore: make default target build, not dev 2019-03-10 12:12:39 +01:00
Simon Cruanes
596034d16a fix(dot): proper labelling of hyper-res nodes 2019-03-10 12:12:39 +01:00
Simon Cruanes
cdb52ee757 fix(proof): unsat conflicts now call Proof.prove_unsat 
this does the last bit of proof recording when a conflict is reached
during propagation
 2019-03-10 12:12:39 +01:00
Simon Cruanes
2e2bbfd4d0 fix(proof.check): ensure that the proof is an empty clause 2019-03-10 12:12:39 +01:00
Simon Cruanes
92ca9c328f refactor(main): catch resolution errors properly; style 2019-03-10 12:12:39 +01:00
Simon Cruanes
e30c54e11b refactor: use hyper-res steps in proofs 
- accelerates proof checking significantly
- provide a way to expand hyper-res steps into individual resolutions
  (eg for the Coq backend)
 2019-03-10 12:12:39 +01:00
Simon Cruanes
b2cec9eaa2 perf: use mutable flags on atoms to perform proof checking 2019-03-10 12:12:39 +01:00
Simon Cruanes
7a2f59e9dd feat: add basic theory of constructors 2019-03-09 16:51:57 -06:00
Simon Cruanes
cb0b5cbcbd refactor: change signature of CC.Theory.on_new_term 2019-03-09 16:51:39 -06:00
Simon Cruanes
314bd7f8b2 feat: add ite theory 2019-03-09 16:16:21 -06:00
Simon Cruanes
431988d5e4 feat: more expressive theories, also plug distinct in 2019-03-09 16:15:24 -06:00
Simon Cruanes
d4758a2fcf cleanup 2019-03-03 16:22:14 -06:00
Simon Cruanes
f58bdb5f30 feat: first working version of th-distinct as a separate theory 2019-03-03 15:17:06 -06:00
Simon Cruanes
23c0e3c087 wip: new "distinct" theory 2019-02-26 22:46:43 -06:00
Simon Cruanes
342dba4533 wip: new micro-theories in CC 2019-02-26 22:46:40 -06:00
Simon Cruanes
57147cea85 chore: add common dune file 2019-02-26 22:46:13 -06:00
Simon Cruanes
c79a5a4798 wip: micro theories 2019-02-22 20:57:17 -06:00
Simon Cruanes
77a5475862 wip: cleanup cc 2019-02-22 18:54:56 -06:00
Simon Cruanes
de1cc952a5 refactor: use new msat lazy propagation 2019-02-16 19:09:43 -06:00
Simon Cruanes
3873718174 refactor: require state in Lit.atom, and in Term.abs 
allows abs(false)=true
 2019-02-16 17:43:49 -06:00
Simon Cruanes
4d2bddc660 refactor(cc): smaller explanations for congruence-based merges 2019-02-16 17:43:04 -06:00
Simon Cruanes
14255f94a7 refactor(cc): remove dead code 2019-02-16 15:32:35 -06:00
Simon Cruanes
365aedb138 perf(cc): path compression 2019-02-16 15:28:16 -06:00
Simon Cruanes
ac030641db refactor(ty): use Hashcons with weak table for types 2019-02-16 15:23:57 -06:00
Simon Cruanes
3b671aa7a4 refactor(term): use hashconsing with a weak table 2019-02-16 15:08:49 -06:00
Simon Cruanes
1ef0cf4183 refactor: small cleanup in terms 2019-02-16 14:58:13 -06:00
Simon Cruanes
a14fe25ba0 chore: add tools, update gitignore 2019-02-16 14:50:34 -06:00