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
1468 commits 53 branches 1 tag 17 MiB
Commit graph

1468 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Simon Cruanes
63e7d6659e
wip: dump more steps to the trace file 2021-10-20 20:41:51 -04:00
Simon Cruanes
f5172a7927
wip: emit proof steps 2021-10-19 22:52:34 -04:00
Simon Cruanes
3589592296
wip: use real proofs 2021-10-16 22:00:29 -04:00
Simon Cruanes
29d1fd5cf3
fix bug in veci32 2021-10-16 21:41:10 -04:00
Simon Cruanes
597a6c378e
wip: split VecI32 and VecSmallInt 
- use VecSmallInt for small integers of type `int`
- use VecI32 to store actual int32 (in particular for proof steps)
 2021-10-16 20:31:56 -04:00
Simon Cruanes
af1ef089af
wip: proper proof production using Proof_ser-based traces 2021-10-15 23:00:09 -04:00
Simon Cruanes
ca4a42f28a
improve API of chunk_stack 2021-10-14 23:40:58 -04:00
Simon Cruanes
7df124f94c
test: add a test using a file backend 2021-10-14 23:40:51 -04:00
Simon Cruanes
73cca4ca18
move chunk_stack to util, fix some bugs 2021-10-14 23:18:21 -04:00
Simon Cruanes
3a56fb0763
test file for chunk stack 2021-10-14 23:18:08 -04:00
Simon Cruanes
beda972def
wip: feat(base): proof chunk storage 2021-10-14 21:41:47 -04:00