21 #ifndef _cvc3__include__theory_uf_h_
22 #define _cvc3__include__theory_uf_h_
89 bool enumerate,
bool computeSize);
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
Data structure of expressions in CVC3.
ExprMap< CDList< Theorem > * > appearsFirstMap
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
ExprMap< CDList< Theorem > * > appearsSecondMap
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
CDO< size_t > d_sharedIdx2
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
MS C++ specific settings.
This theory handles uninterpreted functions.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
CDMap< Expr, bool > d_sharedTermsMap
The set of all shared terms.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
TheoryUF(TheoryCore *core)
CDList< Expr > d_funApplications
Backtracking list of function applications.
const bool & d_applicationsInModel
Flag to include function applications to the concrete model.
CDO< size_t > d_funApplicationsIdx
Pointer to the last unprocessed element (for lambda expansions)
void computeType(const Expr &e)
Compute and store the type of e.
void checkType(const Expr &e)
Check that e is a valid Type expr.
ExprMap< TCMapPair * > d_transClosureMap
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
CDO< size_t > d_sharedIdx1
The pointers to the last unprocessed shared pair.
Expr lambdaExpr(const std::vector< Expr > &vars, const Expr &body)
Create a new LAMBDA-abstraction.
Expr transClosureExpr(const std::string &name, const Expr &e1, const Expr &e2)
Create a transitive closure expression.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
struct CVC3::TheoryUF::TCMapPair TCMapPair
UFProofRules * createProofRules()
Generic API for Theories plus methods commonly used by theories.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Cardinality
Enum for cardinality of types.
UFKinds
Local kinds for transitive closure of binary relations.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
void printSmtLibShared(ExprStream &os, const Expr &e)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.