From 54a6a2cc2e68a4bd93675b6ad8af8c64a1148b02 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 2 Jul 2018 17:38:11 -0500 Subject: [PATCH] update todo --- TODO.md | 52 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 33 insertions(+), 19 deletions(-) diff --git a/TODO.md b/TODO.md index c41dc4c1..9a99345c 100644 --- a/TODO.md +++ b/TODO.md @@ -2,31 +2,37 @@ ## TODO -- SAT: - * merge all clause vectors into one - * remove all simplifications at level 0 - * addition of clauses: should be much simpler +- per-theory trail, with push/pop as in the SAT solver (generic trail?) + * in CC, clear pending tasks upon backtrack -- explicit lifecycle for SAT atoms (dead/assigned/in-heap) -- simplify addition of clauses: - * do not simplify at level 0 - * steps on addition: - 1. internalize all atoms (dead -> in-heap) - 2. unit-propagate/do nothing/add clause - 3. remove clause on backtracking if not at level 0 +- in CC, merge classes eagerly + +- rethink backtracking: instead of a pure stack, consider the theory as separated from the SAT solver. + When a new term is added, unwind theory back to level 0, add term, then up + to current trail level again. + +- in terms, remove `Bool` case and add `Value of value` instead + **OR**: turn every term into `apply` with a `cst` and a `args: term IArray.t`, make bool such a constant, + and have `is_value` predicate in custom constants (or `as_value: self -> value option?`) + +- when CC merging two classes, if one is a value then pick it as representative + (i.e. values are always representatives) + +- fix: + ./main.exe tests/unsat/eq_diamond10.smt2 -- merge Solver_types.ml with Internal.ml - make CC work on QF_UF - * internalize terms on the fly (backtrackable) + * public `add` function should push_pending then call main CC loop + (internal one is called within the loop so no need) + * internalize terms on the fly (backtrackable) OR: at the beginning, backtrack to 0 to add a new term and then add trail again * basic notion of activity (of subterms) for `ite` (and recfuns, later)? -- redo_down_to_level_0 should actually redo down to `base_level` - - add `CC.add_rw_step t u` work, where `t-->u` (remove `t` from sig table, should have almost 0 overhead after that) - * use it for + * use it for `if a b c --> b` when `a=true` + * use it for local simplifications + * use it for function evaluation (i.e. rewrite rules) -- notion of `value` (V_true,V_false,V_custom, + maybe undefined some day) - write theory of datatypes (without acyclicity) with local case splits + `value` + injectivity - design evaluation system (guards + `eval:(term -> value) option` in custom TC) - compilation of rec functions to defined constants @@ -35,8 +41,6 @@ - datatype acyclicity check -- Shostak theory of eq-ℚ - - abstract domain propagation in CC - domain propagation (intervals) for ℚ arith - full ℚ theory: shostak + domains + if-sat simplex @@ -59,6 +63,16 @@ ## Done +- simplify CC by separating cleanly public/internal API, remove excess batching +- notion of `value` (V_true,V_false,V_custom, + maybe undefined some day) +- checking models (for each clause, at least one true lit also evals to true in model) + * have a `function` section in the model with `(id*value list) -> value`, + extracted from congruence closure +- simplify terms a lot, remove solving/semantic terms +- remove `detach_clause`. never detach a clause until it's really dead; + instead, do (and re-do) `internalize_clause` for its atoms. +- remove push/pop +- merge Solver_types.ml with Internal.ml - theory of boolean constructs (on the fly Tseitin using local clauses) * test `Sat_solver.add_clause` and `new_atom` behavior upon backtracking → when we backtrack an atom, its Tseitin encoding should be removed