From 227df58afd48d544eb475d437a66726387ea75d4 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 7 Dec 2021 10:17:46 -0500 Subject: [PATCH] merge --- TODO.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/TODO.md b/TODO.md index 93b7dde8..b497e530 100644 --- a/TODO.md +++ b/TODO.md @@ -10,7 +10,7 @@ - data oriented congruence closure (all based on VecI32.t) - new proofs: - * simplify : use subproof + * simplify : use subproof (maybe not even there?) * preprocess: no subproof * rule for proving `t=u` by CC modulo all previous unit equalities (needed for simp/preprocess) @@ -123,6 +123,8 @@ than resolution with explicit order+pivots) ⇒ used in SAT solver * [x] store proof in temp file, then parse it backward (using adequate framing) 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 - datatype acyclicity check - make CC work on QF_UF