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

1579 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
3b409c8944
feat(proof): add proof_r1 as a pendant to proof_p1 for non-equations 2021-12-17 11:38:07 -05:00
Simon Cruanes
3ab1ddfea8
fix: ensure all functions in SMT solver preprocess their literals 2021-12-16 13:49:43 -05:00
Simon Cruanes
4ac2eb25a6
use TEF in sudoku; improve a bit its ergonomics 2021-12-07 21:29:51 -05:00
Simon Cruanes
e64013c660
chore: upgrade bare autogen-code 2021-12-07 21:16:25 -05:00
Simon Cruanes
110f3f8527
update benchpress file to actually run proofs 2021-12-07 21:16:12 -05:00
Simon Cruanes
2d8fc78bc4
add expect test for the sudoku solver 2021-12-07 14:39:21 -05:00
Simon Cruanes
72d121fa64
add example: the suduko solver, adapted from msat 2021-12-07 14:10:36 -05:00
Simon Cruanes
cfede762c9
feat(sat): provide a proof_dumm module 2021-12-07 14:08:16 -05:00
Simon Cruanes
9517e88467
feat(util): add backtrackable ref 2021-12-07 14:08:06 -05:00
Simon Cruanes
a614fdb2e1
update benchpress file 2021-12-07 10:16:09 -05:00
Simon Cruanes
2abccce985
build flags 2021-11-29 10:33:56 -05:00
Simon Cruanes
bf1f9e7ce1
try to fix CI 2021-11-28 19:08:26 -05:00
Simon Cruanes
b27fdc5507
Merge pull request #16 from c-cube/wip-proof-smt 
wip: proofs for SMT
 2021-11-28 18:21:48 -05:00
Simon Cruanes
2caafdb530
fix test 2021-11-28 18:12:25 -05:00
Simon Cruanes
f909e6bc9e
fix proof production wrt conflict minimization 2021-11-28 18:10:15 -05:00
Simon Cruanes
1bf05d51ce
fix(proof): emit proper result for RUP steps 2021-11-28 16:35:04 -05:00
Simon Cruanes
15e16a515d
refactor(sat): improve code 2021-11-28 16:34:43 -05:00
Simon Cruanes
e9b395b643
feat(proof): do not emit trivial clause_rw steps 
if there is no rewriting going on, we can skip the step.
 2021-11-28 16:33:57 -05:00
Simon Cruanes
aad1daa4e4
feat(quip): remove lit and not-normalization from quip 2021-11-28 13:36:19 -05:00
Simon Cruanes
0233801b95
more debug messages 2021-11-28 11:28:55 -05:00
Simon Cruanes
2e4fd5e1c1
update conflict resolution for better proofs, improve code 2021-11-27 15:30:45 -05:00
Simon Cruanes
c5c5426ead
quip: include all term definitions in proof 
dependency analysis will not catch these, so we include them
unconditionally
 2021-11-19 23:25:21 -05:00
Simon Cruanes
38d90b250a
refactor sat solver 2021-11-19 23:25:09 -05:00
Simon Cruanes
41fe798b23
fix test 2021-11-19 22:50:22 -05:00
Simon Cruanes
7b15ea7280
refactor(sat): fix proof construction at level 0; improve preprocessing 2021-11-19 22:35:48 -05:00
Simon Cruanes
4d3b278754
feat(vec): add append, fix prepend 2021-11-19 22:35:40 -05:00
Simon Cruanes
1f9c43afa8
fix(sat): generate proof in partition for eliminated level-0 lits 2021-11-14 23:08:02 -05:00
Simon Cruanes
69ee322c45
remove dead code 2021-11-14 22:53:34 -05:00
Simon Cruanes
5d18086e53
fix(sat): resolution at level 0 is not recursive 
recursion is implicit in the structure of the proof of the clause
that is unit at level 0, and thus responsible for propagating the
level-0 atom in the first place.
 2021-11-14 22:50:12 -05:00
Simon Cruanes
7d70994758
fix(proof): add neg-normalization 2021-11-14 22:50:05 -05:00
Simon Cruanes
ffa450ba08
proof: normalize clauses in rw 2021-11-10 18:30:12 -05:00
Simon Cruanes
a8a851a7de
feat: ability to produce .gz proof files 2021-11-10 18:23:26 -05:00
Simon Cruanes
8c780e3ed5
quip: add clause in expr_def 2021-11-10 18:04:52 -05:00
Simon Cruanes
0d00629923
more compressed output of equations 2021-11-10 13:23:29 -05:00
Simon Cruanes
f500704905
fix(sat): level-0 resolution needs to be recursive 2021-11-10 13:20:00 -05:00
Simon Cruanes
72d79d7c0a
fix emission of reference terms 2021-10-29 22:35:19 -04:00
Simon Cruanes
6b1b1eb587
feat(proof): process more steps in proof reconstruction 
also, use names for function application terms, so as to preserve
sharing.
 2021-10-28 20:48:39 -04:00
Simon Cruanes
7d5b76a87a
fix tests and warning 2021-10-27 21:54:30 -04:00
Simon Cruanes
0abe4b7020
wip: decode more proof steps to quip 2021-10-27 21:50:28 -04:00
Simon Cruanes
992b93abcf
fix(sat): clause in a unsat result must not contain 0-level literals 2021-10-27 20:19:01 -04:00
Simon Cruanes
5a6019f834
missing module 2021-10-26 22:04:33 -04:00
Simon Cruanes
4a30a06f87
wip: reconstruct quip proof from binary proof-trace 2021-10-26 21:57:17 -04:00
Simon Cruanes
d8518ae942
wip: standalone module for Quip proofs 
the idea here is that Quip proofs will be built from proof traces,
and do not need to depend on any concrete term representation.
Their terms, types, etc. match exactly what we know how to print
to Quip, and bare no relation to concrete representations used during
proof search.
 2021-10-25 19:52:00 -04:00
Simon Cruanes
b5749a1b72
emit many more proof steps 2021-10-22 21:31:44 -04:00
Simon Cruanes
c2b8d93cf4
refactor proof storage 2021-10-21 23:28:53 -04:00
Simon Cruanes
a871192c5e
fix bug in proof emission 2021-10-21 20:53:06 -04:00
Simon Cruanes
84f7a39423
fix doc test 2021-10-21 20:42:12 -04:00
Simon Cruanes
8ac2267595
add a simple binary to dump proof traces 2021-10-21 20:33:10 -04:00
Simon Cruanes
7e40851e1b
use sidekick-base.proof-trace in base 2021-10-21 20:32:47 -04:00
Simon Cruanes
254d6a1906
feat: library for the proof step serialization 2021-10-21 20:32:34 -04:00