update todo

TODO.md

@@ -2,31 +2,37 @@
 
 ## TODO
 
-- SAT:
+- per-theory trail, with push/pop as in the SAT solver (generic trail?)
-  * merge all clause vectors into one
+  * in CC, clear pending tasks upon backtrack
-  * remove all simplifications at level 0
-  * addition of clauses: should be much simpler
 
-- explicit lifecycle for SAT atoms  (dead/assigned/in-heap)
+- in CC, merge classes eagerly
-- simplify addition of clauses:
+
-  * do not simplify at level 0
+- rethink backtracking: instead of a pure stack, consider the theory as separated from the SAT solver.
-  * steps on addition:
+  When a new term is added, unwind theory back to level 0, add term, then up
-    1. internalize all atoms (dead -> in-heap)
+  to current trail level again.
-    2. unit-propagate/do nothing/add clause
+
-    3. remove clause on backtracking if not at level 0
+- 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