22 #ifndef _cvc3__include__theory_h_
23 #define _cvc3__include__theory_h_
102 virtual void setUsed() { d_theoryUsed =
true; }
149 virtual void checkSat(
bool fullEffort) = 0;
253 bool enumerate,
bool computeSize)
390 #ifdef _CVC3_DEBUG_MODE
392 virtual void debug(
int i) { }
394 virtual int help(
int i) {
return 9999 ;} ;
427 virtual Theorem
simplify(
const Expr& e);
476 bool hasSolver=
false);
597 bool computeTransClosure);
687 const std::vector<Theorem>& thms)
703 const std::vector<unsigned>& changed,
704 const std::vector<Theorem>& thms)
715 return d_commonRules->
iffMP(e1, e1_iff_e2);
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
TheoryCore * d_theoryCore
Provides the core functionality.
virtual void setUsed()
Set the "used" flag on this theory (for smtlib translator)
virtual Theorem rewriteAtomic(const Expr &e)
Theory-specific rewrites for atomic formulas.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
TheoryCore * theoryCore()
Get a pointer to theoryCore.
bool leavesAreSimp(const Expr &e)
Test if all i-leaves of e are simplified.
Data structure of expressions in CVC3.
virtual void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem typePred(const Expr &e)
Return BOOLEAN type.
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
bool isLeafIn(const Expr &e1, const Expr &e2)
Test if e1 is an i-leaf in e2.
ExprManager * getEM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
bool isLeaf(const Expr &e)
Test if e is an i-leaf term for the current theory.
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
virtual void setIncomplete(const std::string &reason)
Mark the current decision branch as possibly incomplete.
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
Theorem substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2)
Special case for binary operators.
bool hasTheory(int kind)
Test whether a kind maps to any theory.
Type newSubtypeExpr(const Expr &pred, const Expr &witness)
Create a new subtype expression.
std::string d_name
Name of the theory (for debugging)
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
virtual Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
MS C++ specific settings.
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
virtual Theorem rewriteAnd(const Expr &e)=0
==> AND(e1,e2) IFF [simplified expr]
virtual void enqueueSE(const Theorem &e)
Check if the current context is inconsistent.
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver)
Unregister a theory.
Theorem substitutivityRule(const Expr &e, int changed, const Theorem &thm)
Optimized: only a single position changed.
virtual Theorem reflexivityRule(const Expr &a)=0
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
void registerKinds(Theory *theory, std::vector< int > &kinds)
Register new kinds with the given theory.
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
virtual void checkType(const Expr &e)
Check that e is a valid Type expr.
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
virtual ~Theory(void)
Destructor.
Theorem renameExpr(const Expr &e)
Derived rule to create a new name for an expression.
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
Type lookupTypeExpr(const std::string &name)
Lookup type by name. Return Null if no such type exists.
Op newFunction(const std::string &name, const Type &type, bool computeTransClosure)
Create a new uninterpreted function.
void addGlobalLemma(const Theorem &thm, int priority=0)
Add a global lemma.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
std::string toString() const
Print the expression to a string.
virtual void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Expr newVar(const std::string &name, const Type &type)
Create a new variable given its name and type.
void unregisterKinds(Theory *theory, std::vector< int > &kinds)
Unregister kinds for a theory.
virtual void computeType(const Expr &e)
Compute and store the type of e.
virtual void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
const Expr & falseExpr()
FALSE Expr.
virtual void registerAtom(const Expr &e)
Theory-specific registration of atoms.
virtual void assertFact(const Theorem &e)=0
Assert a new fact to the decision procedure.
Theorem substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
Optimized: only positions which changed are included.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
const Expr & getRHS() const
const std::string & getName() const
Get the name of the theory (for debugging purposes)
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
const Theorem & findRef(const Expr &e)
Return the find as a reference: expr must have a find.
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Type newTypeExpr(const std::string &name)
Create a new uninterpreted type with the given name.
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
const Expr & trueExpr()
TRUE Expr.
const Expr & falseExpr()
Return FALSE Expr.
const Expr & trueExpr()
Return TRUE Expr.
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
virtual ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
virtual Type computeBaseType(const Type &tp)
Compute the base type of the top-level operator of an arbitrary type.
virtual void assertTypePred(const Expr &e, const Theorem &pred)
Receives all the type predicates for the types of the given theory.
void installID(const std::string &name, const Expr &e)
Install name as a new identifier associated with Expr e.
ExprManager * getEM()
Access to ExprManager.
virtual void checkSat(bool fullEffort)=0
Check for satisfiability in the theory.
void getModelTerm(const Expr &e, std::vector< Expr > &v)
Calls the correct theory to get all of the terms that need to be assigned values in the concrete mode...
virtual Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
virtual Theorem solve(const Theorem &e)
An optional solver.
Theorem updateHelper(const Expr &e)
Update the children of the term e.
virtual void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
virtual bool theoryUsed()
Get whether theory has been used (for smtlib translator)
Op lookupFunction(const std::string &name, Type *type)
Look up a function by name.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
void updateCC(const Theorem &e, const Expr &d)
Update a term w.r.t. congruence closure (must be setup with setupCC())
virtual void refineCounterExample()
Process disequalities from the arrangement for model generation.
virtual Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool findReduced(const Expr &e)
Return true iff e is find-reduced.
Theorem findReduce(const Expr &e)
Return find-reduced version of e.
int getNumTheories()
Return the number of registered theories.
virtual bool inconsistent()
Check if the current context is inconsistent.
virtual void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Type boolType()
Return BOOLEAN type.
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
virtual Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
(same for IFF)
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
virtual void registerAtom(const Expr &e, const Theorem &thm)
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
virtual Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
Theorem reflexivityRule(const Expr &a)
==> a == a
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
CommonProofRules * d_commonRules
Commonly used proof rules.
Cardinality
Enum for cardinality of types.
Expr lookupVar(const std::string &name, Type *type)
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
virtual void notifyInconsistent(const Theorem &thm)
Notification of conflict.
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
virtual Theorem rewriteOr(const Expr &e)=0
==> OR(e1,...,en) IFF [simplified expr]
Theory(void)
Private default constructor.
static Type typeBool(ExprManager *em)
Theorem substitutivityRule(const Expr &e, const Theorem &t)
Special case for unary operators.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1