21 #ifndef _cvc3__include__theory_datatype_h_
22 #define _cvc3__include__theory_datatype_h_
30 class DatatypeProofRules;
80 unsigned position,
bool positive);
93 virtual void checkSat(
bool fullEffort);
100 bool enumerate,
bool computeSize);
109 const std::vector<std::string>& constructors,
110 const std::vector<std::vector<std::string> >& selectors,
111 const std::vector<std::vector<Expr> >& types);
115 const std::vector<std::vector<std::string> >& constructors,
116 const std::vector<std::vector<std::vector<std::string> > >& selectors,
117 const std::vector<std::vector<std::vector<Expr> > >& types);
120 const std::vector<Expr>& args);
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
bool isConstructor(const Expr &e)
TheoryCore * theoryCore()
Get a pointer to theoryCore.
bool isDatatype(const Type &t)
CDMap< Expr, SmartCDO< Unsigned > > d_labels
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr datatypeTestExpr(const std::string &constructor, const Expr &arg)
void checkType(const Expr &e)
Check that e is a valid Type expr.
const bool & d_smartSplits
CDList< Expr > d_splitters
virtual void mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr getConstructor(const Expr &e)
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
DatatypeProofRules * d_rules
MS C++ specific settings.
Expr getConstant(const Type &t)
DatatypeKinds
Local kinds for datatypes.
bool isSelector(const Expr &e)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
#define DebugAssert(cond, str)
ExprMap< ExprMap< unsigned > > d_datatypes
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
bool canCollapse(const Expr &e)
unsigned getConsPos(const Expr &e)
Expr getConsForTester(const Expr &e)
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
void computeType(const Expr &e)
Compute and store the type of e.
const Op & getReachablePredicate(const Type &t)
const Expr & getExpr() const
virtual void initializeLabels(const Expr &e, const Type &t)
CDO< unsigned > d_splittersIndex
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
This theory handles datatypes.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
ExprMap< Expr > d_testerMap
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
const std::pair< Expr, unsigned > & getSelectorInfo(const Expr &e)
virtual void instantiate(const Expr &e, const Unsigned &u)
bool isTester(const Expr &e)
CDList< Theorem > d_facts
Expr datatypeSelExpr(const std::string &selector, const Expr &arg)
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Generic API for Theories plus methods commonly used by theories.
CDO< bool > d_splitterAsserted
TheoryDatatype(TheoryCore *theoryCore)
Theorem solve(const Theorem &e)
An optional solver.
Expr datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)
Cardinality
Enum for cardinality of types.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
DatatypeProofRules * createProofRules()
Type getType() const
Get the type. Recursively compute if necessary.
ExprMap< std::pair< Expr, unsigned > > d_selectorMap
virtual ~TheoryDatatype()
ExprMap< std::vector< Expr > > d_constructorMap
virtual void checkSat(bool fullEffort)
Check for satisfiability in the theory.
ExprMap< bool > d_getConstantStack
Expr dataType(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)
Smart context-dependent object wrapper.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.