22 #ifndef _cvc3__include__theory_simulate_h_
23 #define _cvc3__include__theory_simulate_h_
29 class SimulateProofRules;
~TheorySimulate()
Destructor.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
"Theory" of symbolic simulation.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
SimulateProofRules * d_rules
Our local proof rules.
void computeType(const Expr &e)
Compute and store the type of e.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
TheorySimulate(TheoryCore *core)
Constructor.
Generic API for Theories plus methods commonly used by theories.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
SimulateProofRules * createProofRules()
Create proof rules for this theory.