CVC3  2.4.1
CVC3::TheoryDatatypeLazy Member List

This is the complete list of members for CVC3::TheoryDatatypeLazy, including all inherited members.

addBoundVar(const std::string &name, const Type &type)CVC3::Theory
addBoundVar(const std::string &name, const Type &type, const Expr &def)CVC3::Theory
addGlobalLemma(const Theorem &thm, int priority=0)CVC3::Theory
addSharedTerm(const Expr &e)CVC3::TheoryDatatypevirtual
addSplitter(const Expr &e, int priority=0)CVC3::Theory
assertEqualities(const Theorem &e)CVC3::Theoryvirtual
assertFact(const Theorem &e)CVC3::TheoryDatatypevirtual
assertTypePred(const Expr &e, const Theorem &pred)CVC3::Theoryinlinevirtual
assignValue(const Expr &t, const Expr &val)CVC3::Theoryvirtual
assignValue(const Theorem &thm)CVC3::Theoryvirtual
boolType()CVC3::Theoryinline
canCollapse(const Expr &e)CVC3::TheoryDatatype
checkAssertEqInvariant(const Theorem &e)CVC3::Theoryinlinevirtual
checkSat(bool fullEffort)CVC3::TheoryDatatypeLazyvirtual
checkType(const Expr &e)CVC3::TheoryDatatypevirtual
computeBaseType(const Type &tp)CVC3::Theoryinlinevirtual
computeModel(const Expr &e, std::vector< Expr > &vars)CVC3::Theoryinlinevirtual
computeModelBasic(const std::vector< Expr > &v)CVC3::Theoryinlinevirtual
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::TheoryDatatypevirtual
computeTCC(const Expr &e)CVC3::TheoryDatatypevirtual
computeType(const Expr &e)CVC3::TheoryDatatypevirtual
computeTypePred(const Type &t, const Expr &e)CVC3::Theoryinlinevirtual
createProofRules()CVC3::TheoryDatatype
d_constructorMapCVC3::TheoryDatatypeprotected
d_datatypesCVC3::TheoryDatatypeprotected
d_factsCVC3::TheoryDatatypeprotected
d_getConstantStackCVC3::TheoryDatatypeprotected
d_labelsCVC3::TheoryDatatypeprotected
d_processIndexCVC3::TheoryDatatypeLazyprivate
d_processQueueCVC3::TheoryDatatypeLazyprivate
d_processQueueKindCVC3::TheoryDatatypeLazyprivate
d_reachCVC3::TheoryDatatypeprotected
d_rulesCVC3::TheoryDatatypeprotected
d_selectorMapCVC3::TheoryDatatypeprotected
d_smartSplitsCVC3::TheoryDatatypeprotected
d_splitterAssertedCVC3::TheoryDatatypeprotected
d_splittersCVC3::TheoryDatatypeprotected
d_splittersIndexCVC3::TheoryDatatypeprotected
d_testerMapCVC3::TheoryDatatypeprotected
d_theoryUsedCVC3::Theoryprotected
d_typeCompleteCVC3::TheoryDatatypeLazyprivate
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)CVC3::TheoryDatatype
dataType(const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types)CVC3::TheoryDatatype
datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)CVC3::TheoryDatatype
datatypeSelExpr(const std::string &selector, const Expr &arg)CVC3::TheoryDatatype
datatypeTestExpr(const std::string &constructor, const Expr &arg)CVC3::TheoryDatatype
ENQUEUE enum valueCVC3::TheoryDatatypeLazyprivate
enqueueFact(const Theorem &e)CVC3::Theoryvirtual
enqueueSE(const Theorem &e)CVC3::Theoryvirtual
falseExpr()CVC3::Theoryinline
find(const Expr &e)CVC3::Theory
findExpr(const Expr &e)CVC3::Theoryinline
findReduce(const Expr &e)CVC3::Theory
findReduced(const Expr &e)CVC3::Theory
findRef(const Expr &e)CVC3::Theory
finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)CVC3::TheoryDatatypevirtual
getBaseType(const Expr &e)CVC3::Theory
getBaseType(const Type &tp)CVC3::Theory
getCommonRules()CVC3::Theoryinline
getConsForTester(const Expr &e)CVC3::TheoryDatatype
getConsPos(const Expr &e)CVC3::TheoryDatatype
getConstant(const Type &t)CVC3::TheoryDatatype
getEM()CVC3::Theoryinline
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::Theory
getName() const CVC3::Theoryinline
getNumTheories()CVC3::Theory
getReachablePredicate(const Type &t)CVC3::TheoryDatatype
getSelectorInfo(const Expr &e)CVC3::TheoryDatatype
getTCC(const Expr &e)CVC3::Theory
getTypePred(const Type &t, const Expr &e)CVC3::Theory
hasTheory(int kind)CVC3::Theory
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::Theoryinline
inconsistent()CVC3::Theoryvirtual
initializeLabels(const Expr &e, const Type &t)CVC3::TheoryDatatypeLazyprivatevirtual
installID(const std::string &name, const Expr &e)CVC3::Theory
instantiate(const Expr &e, const Unsigned &u)CVC3::TheoryDatatypeLazyprivatevirtual
isLeaf(const Expr &e)CVC3::Theoryinline
isLeafIn(const Expr &e1, const Expr &e2)CVC3::Theory
leavesAreSimp(const Expr &e)CVC3::Theory
lookupFunction(const std::string &name, Type *type)CVC3::Theory
lookupTypeExpr(const std::string &name)CVC3::Theory
lookupVar(const std::string &name, Type *type)CVC3::Theory
MERGE1 enum valueCVC3::TheoryDatatypeLazyprivate
MERGE2 enum valueCVC3::TheoryDatatypeLazyprivate
mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)CVC3::TheoryDatatypeLazyprivatevirtual
mergeLabels(const Theorem &thm, const Expr &e, unsigned position, bool positive)CVC3::TheoryDatatypeLazyprivatevirtual
newFunction(const std::string &name, const Type &type, bool computeTransClosure)CVC3::Theory
newFunction(const std::string &name, const Type &type, const Expr &def)CVC3::Theory
newSubtypeExpr(const Expr &pred, const Expr &witness)CVC3::Theory
newTypeExpr(const std::string &name)CVC3::Theory
newTypeExpr(const std::string &name, const Type &def)CVC3::Theory
newVar(const std::string &name, const Type &type)CVC3::Theory
newVar(const std::string &name, const Type &type, const Expr &def)CVC3::Theory
notifyInconsistent(const Theorem &thm)CVC3::Theoryinlinevirtual
parseExpr(const Expr &e)CVC3::Theoryvirtual
parseExprOp(const Expr &e)CVC3::TheoryDatatypevirtual
print(ExprStream &os, const Expr &e)CVC3::TheoryDatatypevirtual
ProcessKinds enum nameCVC3::TheoryDatatypeLazyprivate
refineCounterExample()CVC3::Theoryinlinevirtual
reflexivityRule(const Expr &a)CVC3::Theoryinline
registerAtom(const Expr &e, const Theorem &thm)CVC3::Theoryvirtual
registerAtom(const Expr &e)CVC3::Theoryinlinevirtual
registerKinds(Theory *theory, std::vector< int > &kinds)CVC3::Theory
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)CVC3::Theory
renameExpr(const Expr &e)CVC3::Theory
resolveID(const std::string &name)CVC3::Theory
rewrite(const Expr &e)CVC3::TheoryDatatypevirtual
rewriteAnd(const Expr &e)CVC3::Theoryinline
rewriteAtomic(const Expr &e)CVC3::Theoryinlinevirtual
rewriteCC(const Expr &e)CVC3::Theory
rewriteIte(const Expr &e)CVC3::Theory
rewriteOr(const Expr &e)CVC3::Theoryinline
setIncomplete(const std::string &reason)CVC3::Theoryvirtual
setInconsistent(const Theorem &e)CVC3::Theoryvirtual
setup(const Expr &e)CVC3::TheoryDatatypeLazyvirtual
setupCC(const Expr &e)CVC3::Theory
setUsed()CVC3::Theoryinlinevirtual
simplify(const Expr &e)CVC3::Theoryvirtual
simplifyExpr(const Expr &e)CVC3::Theoryinline
simplifyOp(const Expr &e)CVC3::Theoryvirtual
solve(const Theorem &e)CVC3::TheoryDatatypevirtual
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::Theoryinline
substitutivityRule(const Expr &e, const Theorem &t)CVC3::Theoryinline
substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2)CVC3::Theoryinline
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVC3::Theoryinline
substitutivityRule(const Expr &e, int changed, const Theorem &thm)CVC3::Theoryinline
symmetryRule(const Theorem &a1_eq_a2)CVC3::Theoryinline
Theory(TheoryCore *theoryCore, const std::string &name)CVC3::Theory
theoryCore()CVC3::Theoryinline
TheoryDatatype(TheoryCore *theoryCore)CVC3::TheoryDatatype
TheoryDatatypeLazy(TheoryCore *theoryCore)CVC3::TheoryDatatypeLazy
theoryOf(int kind)CVC3::Theory
theoryOf(const Type &e)CVC3::Theory
theoryOf(const Expr &e)CVC3::Theory
theoryPreprocess(const Expr &e)CVC3::Theoryinlinevirtual
theoryUsed()CVC3::Theoryinlinevirtual
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::Theoryinline
trueExpr()CVC3::Theoryinline
typePred(const Expr &e)CVC3::Theory
unregisterKinds(Theory *theory, std::vector< int > &kinds)CVC3::Theory
unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver)CVC3::Theory
update(const Theorem &e, const Expr &d)CVC3::TheoryDatatypeLazyvirtual
updateCC(const Theorem &e, const Expr &d)CVC3::Theory
updateHelper(const Expr &e)CVC3::Theory
~Theory(void)CVC3::Theoryvirtual
~TheoryDatatype()CVC3::TheoryDatatypevirtual
~TheoryDatatypeLazy()CVC3::TheoryDatatypeLazyinline