CVC3  2.4.1
CVC3::TheoryCore Member List

This is the complete list of members for CVC3::TheoryCore, 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
addFact(const Theorem &e)CVC3::TheoryCore
addGlobalLemma(const Theorem &thm, int priority=0)CVC3::Theory
addNotifyEq(Theory *t, const Expr &e)CVC3::TheoryCoreinline
addSharedTerm(const Expr &e)CVC3::TheoryCoreinlinevirtual
addSplitter(const Expr &e, int priority=0)CVC3::Theory
addToVarDB(const Expr &e)CVC3::TheoryCore
assertEqualities(const Theorem &e)CVC3::TheoryCoreprivatevirtual
assertFact(const Theorem &e)CVC3::TheoryCorevirtual
assertFactCore(const Theorem &e)CVC3::TheoryCoreprivate
assertFormula(const Theorem &e)CVC3::TheoryCoreprivate
assertTypePred(const Expr &e, const Theorem &pred)CVC3::Theoryinlinevirtual
assignValue(const Expr &t, const Expr &val)CVC3::TheoryCorevirtual
assignValue(const Theorem &thm)CVC3::TheoryCorevirtual
boolType()CVC3::Theoryinline
buildModel(ExprMap< Expr > &m)CVC3::TheoryCore
buildModel(Theorem &thm)CVC3::TheoryCore
callTheoryPreprocess(const Expr &e)CVC3::TheoryCore
checkAssertEqInvariant(const Theorem &e)CVC3::Theoryinlinevirtual
checkEquation(const Theorem &thm)CVC3::TheoryCoreprivate
checkSat(bool fullEffort)CVC3::TheoryCoreinlinevirtual
checkSATCore()CVC3::TheoryCore
checkSolved(const Theorem &thm)CVC3::TheoryCoreprivate
checkType(const Expr &e)CVC3::TheoryCorevirtual
clearInPP()CVC3::TheoryCoreinline
collectBasicVars()CVC3::TheoryCore
collectModelValues(const Expr &e, ExprMap< Expr > &m)CVC3::TheoryCore
computeBaseType(const Type &t)CVC3::TheoryCorevirtual
computeModel(const Expr &e, std::vector< Expr > &vars)CVC3::Theoryinlinevirtual
computeModelBasic(const std::vector< Expr > &v)CVC3::TheoryCorevirtual
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theoryvirtual
computeTCC(const Expr &e)CVC3::TheoryCorevirtual
computeType(const Expr &e)CVC3::TheoryCorevirtual
computeTypePred(const Type &t, const Expr &e)CVC3::TheoryCorevirtual
CoreNotifyObj classCVC3::TheoryCorefriend
createProofRules(TheoremManager *tm)CVC3::TheoryCoreprivate
d_assignmentCVC3::TheoryCoreprivate
d_basicModelVarsCVC3::TheoryCoreprivate
d_boundVarMapCVC3::TheoryCoreprivate
d_boundVarStackCVC3::TheoryCoreprivate
d_cmCVC3::TheoryCoreprivate
d_coreSatAPICVC3::TheoryCoreprivate
d_currentRecursiveSimplifierCVC3::TheoryCoreprivate
d_exprTransCVC3::TheoryCoreprivate
d_flagsCVC3::TheoryCoreprivate
d_globalsCVC3::TheoryCoreprivate
d_impliedLiteralsCVC3::TheoryCoreprivate
d_impliedLiteralsIdxCVC3::TheoryCoreprivate
d_inAddFactCVC3::TheoryCoreprivate
d_inCheckSATCoreCVC3::TheoryCoreprivate
d_incompleteCVC3::TheoryCoreprivate
d_inconsistentCVC3::TheoryCoreprivate
d_incThmCVC3::TheoryCoreprivate
d_inPPCVC3::TheoryCoreprivate
d_inRegisterAtomCVC3::TheoryCoreprivate
d_inUpdateCVC3::TheoryCoreprivate
d_notifyEqCVC3::TheoryCoreprivate
d_notifyObjCVC3::TheoryCoreprivate
d_parseCacheCVC3::TheoryCoreprivate
d_parseCacheOtherCVC3::TheoryCoreprivate
d_parseCacheTopCVC3::TheoryCoreprivate
d_predicatesCVC3::TheoryCoreprivate
d_printerCVC3::TheoryCoreprivate
d_queueCVC3::TheoryCoreprivate
d_queueSECVC3::TheoryCoreprivate
d_resourceLimitCVC3::TheoryCoreprivate
d_rulesCVC3::TheoryCoreprivate
d_simplifiedModelVarsCVC3::TheoryCoreprivate
d_simplifyInPlaceCVC3::TheoryCoreprivate
d_solverCVC3::TheoryCoreprivate
d_statisticsCVC3::TheoryCoreprivate
d_tccCacheCVC3::TheoryCoreprivate
d_termsCVC3::TheoryCoreprivate
d_termTheoremsCVC3::TheoryCoreprivate
d_theoriesCVC3::TheoryCoreprivate
d_theoryMapCVC3::TheoryCoreprivate
d_theoryUsedCVC3::Theoryprotected
d_timeBaseCVC3::TheoryCoreprivate
d_timeLimitCVC3::TheoryCoreprivate
d_tmCVC3::TheoryCoreprivate
d_translatorCVC3::TheoryCoreprivate
d_typeComputerCVC3::TheoryCoreprivate
d_update_dataCVC3::TheoryCoreprivate
d_update_thmsCVC3::TheoryCoreprivate
d_varAssignmentsCVC3::TheoryCoreprivate
d_varModelMapCVC3::TheoryCoreprivate
d_varsCVC3::TheoryCoreprivate
EffortLevel enum nameCVC3::TheoryCoreprivate
enqueueFact(const Theorem &e)CVC3::TheoryCorevirtual
enqueueSE(const Theorem &thm)CVC3::TheoryCorevirtual
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::TheoryCorevirtual
FULL enum valueCVC3::TheoryCoreprivate
getAssignment()CVC3::TheoryCore
getBaseType(const Expr &e)CVC3::Theory
getBaseType(const Type &tp)CVC3::Theory
getCM() const CVC3::TheoryCoreinline
getCommonRules()CVC3::Theoryinline
getCoreRules() const CVC3::TheoryCoreinline
getCurQuantLevel()CVC3::TheoryCore
getEM()CVC3::Theoryinline
getExprTrans() const CVC3::TheoryCoreinline
getFlags() const CVC3::TheoryCoreinline
getImpliedLiteral(void)CVC3::TheoryCore
getImpliedLiteralByIndex(unsigned index)CVC3::TheoryCore
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::TheoryCoreprivate
getName() const CVC3::Theoryinline
getNumTheories()CVC3::Theory
getPredicates()CVC3::TheoryCoreinline
getQuantLevelForTerm(const Expr &e)CVC3::TheoryCore
getResource()CVC3::TheoryCoreinline
getResourceLimit()CVC3::TheoryCoreinline
getStatistics() const CVC3::TheoryCoreinline
getTCC(const Expr &e)CVC3::Theory
getTerms()CVC3::TheoryCoreinline
getTheoremForTerm(const Expr &e)CVC3::TheoryCore
getTM() const CVC3::TheoryCoreinline
getTranslator() const CVC3::TheoryCoreinline
getTypePred(const Type &t, const Expr &e)CVC3::Theory
getValue(Expr e)CVC3::TheoryCore
hasTheory(int kind)CVC3::Theory
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::Theoryinline
incomplete()CVC3::TheoryCoreinline
incomplete(std::vector< std::string > &reasons)CVC3::TheoryCore
inconsistent()CVC3::TheoryCoreinlinevirtual
inconsistentThm()CVC3::TheoryCoreinline
initTimeLimit()CVC3::TheoryCore
installID(const std::string &name, const Expr &e)CVC3::Theory
inUpdate()CVC3::TheoryCoreinline
isBasicKind(int kind)CVC3::TheoryCoreprivate
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
LOW enum valueCVC3::TheoryCoreprivate
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
NORMAL enum valueCVC3::TheoryCoreprivate
notifyInconsistent(const Theorem &thm)CVC3::Theoryinlinevirtual
numImpliedLiterals()CVC3::TheoryCoreinline
okToEnqueue()CVC3::TheoryCoreinline
outOfResources()CVC3::TheoryCoreinline
parseExpr(const Expr &e)CVC3::TheoryCorevirtual
parseExprOp(const Expr &e)CVC3::TheoryCorevirtual
parseExprTop(const Expr &e)CVC3::TheoryCoreinline
print(ExprStream &os, const Expr &e)CVC3::TheoryCorevirtual
printSmtLibShared(ExprStream &os, const Expr &e)CVC3::TheoryCoreprivate
processCond(const Expr &e, int i)CVC3::TheoryCoreprivate
processFactQueue(EffortLevel effort=NORMAL)CVC3::TheoryCoreprivate
processNotify(const Theorem &e, NotifyList *L)CVC3::TheoryCoreprivate
processUpdates()CVC3::TheoryCoreprivate
refineCounterExample()CVC3::TheoryCorevirtual
refineCounterExample(Theorem &thm)CVC3::TheoryCore
reflexivityRule(const Expr &a)CVC3::Theoryinline
registerAtom(const Expr &e, const Theorem &thm)CVC3::TheoryCorevirtual
CVC3::Theory::registerAtom(const Expr &e)CVC3::Theoryinlinevirtual
registerCoreSatAPI(CoreSatAPI *coreSatAPI)CVC3::TheoryCoreinline
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::TheoryCorevirtual
rewriteAnd(const Expr &e)CVC3::Theoryinline
rewriteAtomic(const Expr &e)CVC3::Theoryinlinevirtual
rewriteCC(const Expr &e)CVC3::Theory
rewriteCore(const Theorem &e)CVC3::TheoryCoreprivate
rewriteCore(const Expr &e)CVC3::TheoryCoreprivate
rewriteIte(const Expr &e)CVC3::Theory
rewriteLitCore(const Expr &e)CVC3::TheoryCoreprivate
rewriteLiteral(const Expr &e)CVC3::TheoryCore
rewriteOr(const Expr &e)CVC3::Theoryinline
setFindLiteral(const Theorem &thm)CVC3::TheoryCoreprivate
setIncomplete(const std::string &reason)CVC3::TheoryCoreprivatevirtual
setInconsistent(const Theorem &e)CVC3::TheoryCorevirtual
setInPP()CVC3::TheoryCoreinline
setResourceLimit(unsigned limit)CVC3::TheoryCoreinline
setTimeLimit(unsigned limit)CVC3::TheoryCore
setup(const Expr &e)CVC3::TheoryCoreinlinevirtual
setupCC(const Expr &e)CVC3::Theory
setupSubFormulas(const Expr &s, const Expr &e, const Theorem &thm)CVC3::TheoryCoreprivate
setupTerm(const Expr &e, Theory *i, const Theorem &thm)CVC3::TheoryCore
setUsed()CVC3::Theoryinlinevirtual
simplify(const Expr &e)CVC3::TheoryCorevirtual
simplifyExpr(const Expr &e)CVC3::Theoryinline
simplifyOp(const Expr &e)CVC3::TheoryCorevirtual
solve(const Theorem &e)CVC3::TheoryCorevirtual
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
tccCache()CVC3::TheoryCoreinline
Theory classCVC3::TheoryCorefriend
CVC3::Theory::Theory(TheoryCore *theoryCore, const std::string &name)CVC3::Theory
theoryCore()CVC3::Theoryinline
TheoryCore(ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics)CVC3::TheoryCore
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
timeLimitReached()CVC3::TheoryCoreprivate
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::Theoryinline
trueExpr()CVC3::Theoryinline
typePred(const Expr &e)CVC3::TheoryCoreprivate
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::TheoryCorevirtual
updateCC(const Theorem &e, const Expr &d)CVC3::Theory
updateHelper(const Expr &e)CVC3::Theory
~Theory(void)CVC3::Theoryvirtual
~TheoryCore()CVC3::TheoryCore