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

1704 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
0afdb06f6c
Merge branch 'wip-datatype-proofs' 2022-01-04 09:46:10 -05:00
Simon Cruanes
b6df2cd974
clause-less steps in proofs 
these steps are checked only once, to accelerate checking, but the
result isn't known.
 2022-01-03 22:59:43 -05:00
Simon Cruanes
88f57d213a
rename stat 2022-01-03 17:13:55 -05:00
Simon Cruanes
dbba6719bc
fix compilation after rebase 2022-01-03 17:13:55 -05:00
Simon Cruanes
9d3da47f3b
fix: missing implied bound update 2022-01-03 17:13:55 -05:00
Simon Cruanes
73c9878554
wip: feat(lra): clarify construction of bounds; fix sign error 2022-01-03 17:13:55 -05:00
Simon Cruanes
721c01d12c
feat(lra): make Erat.{plus,minus}_inf saturating 2022-01-03 17:13:54 -05:00
Simon Cruanes
34b1aa1799
wip: feat(lra): propagate literals based on implied bounds for basic vars 2022-01-03 17:13:54 -05:00
Simon Cruanes
63f50d03fa
feat: proper proof production for theory merges in CC 
this involves resolution steps between the lemma (typically a kind of
horn clause with the merge as conclusion) and a bunch of literals
responsible for some equational hypotheses of this horn clause, being true
 2021-12-29 15:56:54 -05:00
Simon Cruanes
80cb096e8a
feat: change signature of explanations for CC theory merges 2021-12-28 23:07:27 -05:00
Simon Cruanes
be1c1573b1
feat(proof): emit is-a terms properly 
these occur in datatypes proofs.
 2021-12-28 16:46:59 -05:00
Simon Cruanes
8958301a8e
fix: update quip CLI arguments 2021-12-28 10:57:30 -05:00
Simon Cruanes
b2e8f8b29d
chore: disable CI on windows temporarily 2021-12-21 11:31:53 -05:00
Simon Cruanes
584b56075f
feat: add push/pop for assumptions; add check_sat_propagation_only 
this gives the user the possibility of controlling search by mostly
using assumptions (and the underlying assumption stack) as well as
boolean+theory propagation. The result is **not** complete, but can
still help as a beefed-up contextual simplifier.
 2021-12-20 15:34:34 -05:00
Simon Cruanes
5d2f8a1d3d
feat(api): add callbacks to measure progress or ask solver to stop 2021-12-20 13:51:59 -05:00
Simon Cruanes
c03fc97f00
better debug in CC 2021-12-17 16:41:00 -05:00
Simon Cruanes
be2d57a717
feat(cc): add an invariant check before returning a model 2021-12-17 16:41:00 -05:00
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