mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
delete todo
This commit is contained in:
Simon Cruanes
parent
ad8c6a9351
commit
f96967b0da
1 changed files with 0 additions and 221 deletions
221
TODO.md
221
TODO.md
|
|
@ -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 <the term>))`
|
||||
* [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.
|
||||
Loading…
Add table
Reference in a new issue