simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 19:25:36 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

merge

Browse source
This commit is contained in:
Simon Cruanes 2021-12-07 10:17:46 -05:00
parent faf2af1bac
commit 227df58afd
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
TODO.md
View file

@ -10,7 +10,7 @@
- data oriented congruence closure (all based on VecI32.t) - data oriented congruence closure (all based on VecI32.t)
- new proofs: - new proofs:
* simplify : use subproof * simplify : use subproof (maybe not even there?)
* preprocess: no subproof * preprocess: no subproof
* rule for proving `t=u` by CC modulo all previous unit equalities (needed * rule for proving `t=u` by CC modulo all previous unit equalities (needed
for simp/preprocess) for simp/preprocess)
@ -123,6 +123,8 @@
than resolution with explicit order+pivots) ⇒ used in SAT solver than resolution with explicit order+pivots) ⇒ used in SAT solver
* [x] store proof in temp file, then parse it backward (using adequate framing) * [x] store proof in temp file, then parse it backward (using adequate framing)
to obtain relevant part in memory and produce Quip file to obtain relevant part in memory and produce Quip file
- dyn-trans for CC: add hooks in CC explanation of conflict
so the theory can intercept that
- write theory of datatypes (without acyclicity) with local case splits + injectivity + selectors - write theory of datatypes (without acyclicity) with local case splits + injectivity + selectors
- datatype acyclicity check - datatype acyclicity check
- make CC work on QF_UF - make CC work on QF_UF