diff --git a/TODO.md b/TODO.md deleted file mode 100644 index 1fb09926..00000000 --- a/TODO.md +++ /dev/null @@ -1,221 +0,0 @@ - -## TODO - -### 2022-07-20 - -- cc: - * fail on reentrant call (like concurrentModifExn in java) - * in events, provide an `EventAction.t` object rather than the CC; - it provides find,is_eq,explain_eq,etc. as well as modifications - that are pushed into the queue instead of done on the fly. - - main thrust: plugins all observe the same immutable CC, their changes are - performed in batch afterwards - * egg: provide an extended CC plugin API instead (with enough hooks that - it can implement the recompute-if-children-changed thing + early exit - if data didn't change) - * egg: CC provides a associated data API; hide bitfields, just provide - a `make_sparse_data` - + `get: node -> data option` - + `set: node -> data -> unit` (delayed, use an action queue) - + automatic backtracking - ⇒ this should be enough to implement current plugins or even egg itself - * go beyond egg so that the merge `is-some(t) = true` can modify the class - of `t` - * use this to implement booleans! remove true/false custom code -- cc proofs: - * do not ask for `proof_trace` or rules - + instead ask for a type of custom explanations (with pp) - + custom expls are used for both theory in-CC propagations, and - for model construction (semantic merges) - * provide own type of proofs, shaped as an indexed list of steps - * each step proves `t=u` from previous steps using a rule - * rules are Horn hyper-resolution, congruence, by-assertion(lit), - trans(list of steps), or custom(custom_expl) - * theory propagations are annotated with a custom expl and a (T-valid) horn clause - whose head is the propagated equation - -### old - -- self-contained proofs (add axioms and type declarations) - -- add Egg - * use for existing theories (at least datatypes) - * integrate proofs using cc-lemma (no resolution, no intermediate clause) - -- new proofs: - * 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) - * [x] to prove `if a b b = b`, do `a => if a b b = b`, - `¬a => if a b b = b`, and use resolution on these to remove conditions. - -- stronger preprocessing: - * first, split conjunction eagerly - * add every toplevel `x=t` where x atomic to a congruence closure; - then replace toplevel `assert p` with `assert [p]` where `[p]` is - the nested representative of `p` (replace each subterm by its representative). - proof is just `x1=t1 … xn=tn |- p=[p]` - * using Egg, should be possible to integrate theory preprocessing this way - - * then: - - one-point rule for LRA and UF (`x = t /\ F[x]` becomes `x=t /\ F[t]` and - we forget `x` in practice) - - eliminate LRA equations true at level 0 (why is alt-ergo faster on uart7?) - - preprocess LRA for: - `./sidekick tests/unsat/pb_real_50_150_30_47.smt2` - `./sidekick tests/unsat/clocksynchro_9clocks.main_invar.base.smt2` - -- sidekick-check: - * implement deletion - * seems like drat-trim is much faster in backward checking mode, see why - * implement checking of CC/preprocess - * checking of LRA - * checking of DT - -- proof production: - * [x] produce Quip - * [x] have it proofchecked - * [x] do not produce stuff like `(cc-imply (refl tseitin0) (= tseitin0 ))` - * [x] do not produce stuff like `(hres (init (assert t)) (p1 (refl t)))` - (just `assert t` is enough) - * [ ] theory lemmas - -- [x] functor for mapping equiv classes to values of some monoid, code to be - used in 99% of the theories - * [ ] also allow to register to "joins" between distinct classes - (useful for injectivity or array reduction or selector reduction) - → in a way this must become a (backtracking) query API for making theories - easy to write - * [x] use it in th-data for cstors - * [x] use it in th-data for select - * [x] use it in th-data for is-a - * [ ] use it in th-array - * [ ] use it in th-define-subsort - ⇒ **NOTE** this is actually subsumed by Egg - - -- provide a notion of smtlib theory, with `smtlib.ast --> Term.t option` - and typing rule (extensible parsing+typing) - * use if for th-bool - * use if for th-distinct - -- cleanup of CC/optims - * store lits directly in (boolean) classes - -- add terms of input goals pre-emptively to the CC/theories - -- add `CC.add_rw_step t u` work, where `t-->u` - (keep `t` in sig table, but flag is so it's inert and will not - be pushed into `cc.pending` ever, should have almost 0 overhead after that) - * use it for local simplifications - * use it for function evaluation (i.e. rewrite rules) - -- design evaluation system (guards + `eval:(term -> value) option` in custom TC) -- compilation of rec functions to defined constants -- theory of defined constants relying on congruence closure + evaluation - of guards of each case - -- abstract domain propagation in CC -- domain propagation (intervals) for ℚ arith - -## Main goals - -- Allow to plug one's code into boolean propagation - * react upon propagation (possibly by propagating more, or side-effect) - * more advanced/specific propagation (2-clauses)? - * implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf ) - -## Long term goals - -- max-sat/max-smt -- coq proofs ? - -## Done - -- refactor: - * revamp msat proofs - (store proofs in allocator, also encoded as 0-terminated series of ints - indicating clause numbers? - this way we can GC them just like we GC clauses) - ⇒ keep arrays, simpler - + means the type of proofs is independent of variables - + actually: try to use RUP (side buffer to store a representation of - a list of clauses, each "line" is `c_i := l1…ln 0` like dimacs. - Add delete lines to get DRUP.) - proof reconstruction to get, _if wanted_, proper resolution. - + or just store clause premises in a set, use local RUP to reconstruct - (assert ¬C and propagate) - * fix proof production for minimized conflicts (or come back after proof are better) -- enable conflict minimization (from branch) in SAT solver -- emit proofs for SMT; - * [x] add a clause preprocessing rule - (combines all the `… |- t=u` - proofs for preprocessing literals, to rewrite C into D) - * [x] add a RUP rule into Quip, with explicit hyps (fast but more lenient - 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 - * [x] public `add` function should push_pending then call main CC loop - (internal one is called within the loop so no need) - * [x] 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)?~~ -- use `stmlib-utils` -- parser for cstors (`declare-cstor`, same as `declare-fun`) -- refactor: - 1. have sidekick.env with only the signature that is instance-dependent + notion of theory (as module sig); - 2. solver takes this env and SAT solver with compatible lits - 3. move concrete terms, etc. into smtlib lib - 4. update theories -- fix: have normal theories `on_new_term` work properly (callback in the CC?) -- proper statistics -- make the core library entirely functorized - * current term/cst/lit/… would become an implementation library to - be used in the binary -- theory for `ite` -- theory for constructors -- do a `th-distinct` package - * in CC, use payload to store set of distinct tags (if non empty) - * if `¬distinct(t1…tn)` asserted, make big disjunction of cases (split on demand) -- in CC, store literal associated with term, for bool propagation -- in CC, propagation of boolean terms -- in CC, merge classes eagerly -- when CC merging two classes, if one is a value then pick it as representative - (i.e. values are always representatives) -- large refactoring of CC -- 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 - * NOTE: clauses should never be added twice - (or else: what if a clause is added, removed (but not filtered from watched lits) then re-added? duplicate?) -- backtrackable addition of clauses/atoms in Sat solver -- remove tseitin lib -- typing and translation Ast -> Term (from mc2?) -- main executable for SMT solver -- base types (Term, Lit, …) -- theory combination -- basic design of theories - -## Cancelled - -- dynamic ackermannization and transitivity (and maybe datatype acyclicity) - * clause pool for each type of dynamic inference (dynamic ack, etc.), with - its own GC limit. - * Probably need removable atoms too, once all clauses containing it are gone, - for atoms not added by the user explicitely.