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

1887 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
b19d80e443
debug 2021-12-17 16:40:59 -05:00
Simon Cruanes
44c63d4c13
debug 2021-12-17 16:40:52 -05:00
Simon Cruanes
f9f471ce12
details 2021-12-17 13:46:48 -05:00
Simon Cruanes
46b13d08d0
add regression test 2021-12-17 13:21:30 -05:00
Simon Cruanes
2d24a21908
fix: do not preprocess but add equations eagerly for single-cstor terms 2021-12-17 11:58:39 -05:00
Simon Cruanes
6d72203437
fix: avoid preprocessing loops 2021-12-17 11:48:41 -05:00
Simon Cruanes
0841bddbaf
feat(data): preprocessing step for single-cstor types 
if t:ty where ty has exactly one constructor `c`, we replace
t at preprocessing by `c(sel-c-0(t), … sel-c-n(t))`
 2021-12-17 11:39:25 -05:00
Simon Cruanes
63eeb81290
refactor: modify interface of Th_data 2021-12-17 11:39:22 -05:00
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