How to write a theory in CVC4 (old instructions)

This document is meant as a guide to a theory writer.

CVC4 architecture

A high-level description of the flow of information in CVC4 (TheoryEngine, SMTEngine etc.)

TheoryEngine

• check, propagate - calls check/propagate on all registered theories
• presolve - calls presolve for all theories; stops if there is a conflict
• preprocess - first removes ITEs and then rewrites the node by calling the specific theory rewriter. Then theory preregister is being called on all the subterms after their children have all been registered. It is called in the TheoryEgine on a lemma that is added and when a formula is asserted preprocess is called via the SMTEngine (also in getAssignment and getValue stuff?)

SMTEngine

• preprocess - calls TheoryEngine staticLearning() and then TheoryEngine preprocess on the learned facts (WHAT FORM DO THEY HAVE?)
• check - calls PropEngine checkSat() which calls theoryEngine presolve() and then starts the SAT solver which in turn will call theoryCheck()

Adding a new theory

parser

todo

config and make

todo

types and kinds

todo

Theory API & Invariants

Each theory has to be a subclass of the Theory class defined in src/theory/theory.h. A theory has a Context dependent queue of Nodes (cannot be TNodes because some atoms such as equalities can be send across theories without being stored in a map) called d_facts that consists of the atoms asserted in the theory.

Methods implemented in the base class

The following methods are implemented in the base class:

• Theory - the base class constructor must be overwritten by a constructor of this form TheoryX(context::Context* c, OutputChannel& out) .
• get - returns the next atom the d_facts queue; theory registration is called in reverse topological order on all unregistered subterms of the atom
• assertFact - adds a new term to the queue of facts
• shutdown -

Methods implemented by the derived class

The following should be implemented by the derived classes:

• preregisterTerm - is done only once for a node, called during preprocess in TheoryEngine. Preprocessing is done on all input formulas and on the new formulas resulting from adding new lemmas.
• registerTerm - term registration is called when get() is called and a new fact is pulled of the facts queue. This should be done in a "context escape" mode, that is at context level 0 it must not modify conext-dependent objects it has not created itself.
• check - checks the current assigment's consistency. The most important check() invariant is that when check is called with full effort and the current assignment is unsatisfiable it must either return a conflict or force the solver to split by adding a lemma. This is sound because the theory check will be called again with FULL_EFFORT; it is a system wide invariant that before returning "sat" all the theories' check() will be called with full effort. The returned conflict must consist only from atoms that have literals in the SAT solver. If check() is called with an effort level less than FULL_EFFORT it is left to the latitude of the theory implementer to do whatever they want. However not doing anything and only pulling facts off the queue when full effort check() is called is a bad idea, since we are in a leaf of the search and backtracking will undo all the work.
• propagate - propagate new literal assignments in the current context. Note that it can only propagate theory atoms, or negations of atoms, that already have a literal in the SAT solver. An invariant of propagate() is that it should never propagate a literal that is already assigned to true or false. Should call the output channel d_out->propagate().
• explain - return an explanation for the argument Node n, consisting of a conjunction of facts that lead to the literal being propagated. Because in CVC4 explanations are done lazily this is decoupled from propagate(). An invariant of explain is that the decision level of the atoms in the explanation has to be less than or equal than of n. If they are on the same decision level, special care must be taken to make sure the literals in the explanation have not been propagated after n t hus yielding a circular arguemnt. Report this explanation to the output channel's explain().
• staticLearning - called by the SMTEngine during preprocess() via the TheoryEngine. This is not done to a fixpoint (i.e. re-statically-learning until no new facts are learned) but by iterating once through all the theories in the theory table. staticLearning() receives as a parameter a node consisting of all the facts in the input, before being converted to CNF. It must return in the AND-node-builder learned facts that must be true at decision level 0.
• presolve - called exactly one time per user check-sat, after preregistration, rewriting and boolean propagation but the notified theory has not yet had its check() or propagate() methods called. A theory may empty its assertFact() queue using get(), it can raise conflicts, add lemmas and propagate literals during presolve.
• addSharedTerm - TBA
• notifyEq - called by the shared term manager when a shared term becomes equal to another shared term

Theory rewriting

TODO