21 #ifndef _cvc3__include__theory_datatype_lazy_h_
22 #define _cvc3__include__theory_datatype_lazy_h_
60 unsigned position,
bool positive);
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
MS C++ specific settings.
TheoryDatatypeLazy(TheoryCore *theoryCore)
This theory handles datatypes.
CDO< bool > d_typeComplete
This theory handles datatypes.
CDO< unsigned > d_processIndex
void initializeLabels(const Expr &e, const Type &t)
void mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Generic API for Theories plus methods commonly used by theories.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
void instantiate(const Expr &e, const Unsigned &u)
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
CDList< ProcessKinds > d_processQueueKind
CDList< Theorem > d_processQueue
Smart context-dependent object wrapper.