sidekick/TODO.md

Goals

TODO

• 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
  • use it in th-data
  • use it in th-array
  • use it in th-define-subsort

• write theory of datatypes (without acyclicity) with local case splits + injectivity + selectors

• datatype acyclicity check

• 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

• use funarith for basic Q arith

  • as a smtlib theory, too

• 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

• full ℚ theory: shostak + domains + if-sat simplex

Main goals

• Add a backend to send proofs to dedukti
  • First, pure resolution proofs
  • Then, require theories to output lemma proofs for dedukti (in some format yet to be decided)
• 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

• make CC work on QF_UF
  • 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)?
• 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