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
addSharedTerm(const Expr &e)CVC3::TheoryCore [inline, virtual]
addSplitter(const Expr &e, int priority=0)CVC3::Theory
addToVarDB(const Expr &e)CVC3::TheoryCore
assertEqualities(const Theorem &e)CVC3::TheoryCore [private, virtual]
assertFact(const Theorem &e)CVC3::TheoryCore [virtual]
assertFactCore(const Theorem &e)CVC3::TheoryCore [private]
assertFormula(const Theorem &e)CVC3::TheoryCore [private]
assertTypePred(const Expr &e, const Theorem &pred)CVC3::Theory [inline, virtual]
assignValue(const Expr &t, const Expr &val)CVC3::TheoryCore [virtual]
assignValue(const Theorem &thm)CVC3::TheoryCore [virtual]
boolType()CVC3::Theory [inline]
buildModel(ExprMap< Expr > &m)CVC3::TheoryCore
checkAssertEqInvariant(const Theorem &e)CVC3::Theory [inline, virtual]
checkRewriteType(const Theorem &thm)CVC3::TheoryCore [private]
checkSat(bool fullEffort)CVC3::TheoryCore [inline, virtual]
checkSATCore()CVC3::TheoryCore
checkType(const Expr &e)CVC3::TheoryCore [virtual]
collectBasicVars()CVC3::TheoryCore
collectModelValues(const Expr &e, ExprMap< Expr > &m)CVC3::TheoryCore
computeBaseType(const Type &t)CVC3::TheoryCore [virtual]
computeModel(const Expr &e, std::vector< Expr > &vars)CVC3::Theory [inline, virtual]
computeModelBasic(const std::vector< Expr > &v)CVC3::TheoryCore [virtual]
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory [virtual]
computeTCC(const Expr &e)CVC3::TheoryCore [virtual]
computeType(const Expr &e)CVC3::TheoryCore [virtual]
computeTypePred(const Type &t, const Expr &e)CVC3::TheoryCore [virtual]
CoreNotifyObj classCVC3::TheoryCore [friend]
createProofRules(TheoremManager *tm)CVC3::TheoryCore [private]
d_basicModelVarsCVC3::TheoryCore [private]
d_boundVarMapCVC3::TheoryCore [private]
d_boundVarStackCVC3::TheoryCore [private]
d_cmCVC3::TheoryCore [private]
d_coreSatAPICVC3::TheoryCore [private]
d_currentRecursiveSimplifierCVC3::TheoryCore [private]
d_exprTransCVC3::TheoryCore [private]
d_flagsCVC3::TheoryCore [private]
d_globalsCVC3::TheoryCore [private]
d_impliedLiteralsCVC3::TheoryCore [private]
d_impliedLiteralsIdxCVC3::TheoryCore [private]
d_inAddFactCVC3::TheoryCore [private]
d_inCheckSATCoreCVC3::TheoryCore [private]
d_incompleteCVC3::TheoryCore [private]
d_inconsistentCVC3::TheoryCore [private]
d_incThmCVC3::TheoryCore [private]
d_inRegisterAtomCVC3::TheoryCore [private]
d_notifyObjCVC3::TheoryCore [private]
d_parseCacheCVC3::TheoryCore [private]
d_predicatesCVC3::TheoryCore [private]
d_printerCVC3::TheoryCore [private]
d_queueCVC3::TheoryCore [private]
d_queueSECVC3::TheoryCore [private]
d_resourceLimitCVC3::TheoryCore [private]
d_rulesCVC3::TheoryCore [private]
d_simplifiedModelVarsCVC3::TheoryCore [private]
d_simplifyInPlaceCVC3::TheoryCore [private]
d_simpStackCVC3::TheoryCore [private]
d_solverCVC3::TheoryCore [private]
d_statisticsCVC3::TheoryCore [private]
d_tccCacheCVC3::TheoryCore [private]
d_termsCVC3::TheoryCore [private]
d_termTheoremsCVC3::TheoryCore [private]
d_theoriesCVC3::TheoryCore [private]
d_theoryMapCVC3::TheoryCore [private]
d_theoryUsedCVC3::Theory [protected]
d_tmCVC3::TheoryCore [private]
d_translatorCVC3::TheoryCore [private]
d_typeComputerCVC3::TheoryCore [private]
d_update_dataCVC3::TheoryCore [private]
d_update_thmsCVC3::TheoryCore [private]
d_varAssignmentsCVC3::TheoryCore [private]
d_varModelMapCVC3::TheoryCore [private]
d_varsCVC3::TheoryCore [private]
difference(const std::vector< Expr > &a, const std::vector< Expr > &b, std::vector< Expr > &res)CVC3::TheoryCore [private]
EffortLevel enum nameCVC3::TheoryCore [private]
enqueueFact(const Theorem &e)CVC3::TheoryCore [virtual]
enqueueSE(const Theorem &thm)CVC3::TheoryCore [private]
falseExpr()CVC3::Theory [inline]
find(const Expr &e)CVC3::Theory
findExpr(const Expr &e)CVC3::Theory [inline]
findReduced(const Expr &e)CVC3::Theory
findRef(const Expr &e)CVC3::Theory
FULL enum valueCVC3::TheoryCore [private]
getBaseType(const Expr &e)CVC3::Theory
getBaseType(const Type &tp)CVC3::Theory
getCM() constCVC3::TheoryCore [inline]
getCommonRules()CVC3::Theory [inline]
getCoreRules() constCVC3::TheoryCore [inline]
getEM()CVC3::Theory [inline]
getExprTrans() constCVC3::TheoryCore [inline]
getFlags() constCVC3::TheoryCore [inline]
getImpliedLiteral(void)CVC3::TheoryCore
getImpliedLiteralByIndex(unsigned index)CVC3::TheoryCore
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::TheoryCore [private]
getName() constCVC3::Theory [inline]
getNumTheories()CVC3::Theory
getPredicates()CVC3::TheoryCore [inline]
getQuantLevelForTerm(const Expr &e)CVC3::TheoryCore
getResource()CVC3::TheoryCore [inline, private]
getResourceLimit()CVC3::TheoryCore [inline]
getStatistics() constCVC3::TheoryCore [inline]
getTCC(const Expr &e)CVC3::Theory
getTerms()CVC3::TheoryCore [inline]
getTheoremForTerm(const Expr &e)CVC3::TheoryCore
getTM() constCVC3::TheoryCore [inline]
getTranslator() constCVC3::TheoryCore [inline]
getTypePred(const Type &t, const Expr &e)CVC3::Theory
hasTheory(int kind)CVC3::Theory
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::Theory [inline]
incomplete()CVC3::TheoryCore [inline]
incomplete(std::vector< std::string > &reasons)CVC3::TheoryCore
inconsistent()CVC3::TheoryCore [inline, virtual]
inconsistentThm()CVC3::TheoryCore [inline]
installID(const std::string &name, const Expr &e)CVC3::Theory
intersect(const std::vector< Expr > &a, const std::vector< Expr > &b, std::vector< Expr > &res)CVC3::TheoryCore [private]
isBasicKind(int kind)CVC3::TheoryCore [private]
isLeaf(const Expr &e)CVC3::Theory [inline]
isLeafIn(const Expr &e1, const Expr &e2)CVC3::Theory
isSorted(const std::vector< Expr > &v)CVC3::TheoryCore [private]
leavesAreSimp(const Expr &e)CVC3::Theory
lookupVar(const std::string &name, Type *type)CVC3::Theory
LOW enum valueCVC3::TheoryCore [private]
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::TheoryCore [private]
notifyInconsistent(const Theorem &thm)CVC3::Theory [inline, virtual]
numImpliedLiterals()CVC3::TheoryCore [inline]
outOfResources()CVC3::TheoryCore [inline]
parseExpr(const Expr &e)CVC3::TheoryCore [virtual]
parseExprOp(const Expr &e)CVC3::TheoryCore [virtual]
parseExprTop(const Expr &e)CVC3::TheoryCore [inline]
print(ExprStream &os, const Expr &e)CVC3::TheoryCore [virtual]
processCond(const Expr &e, int i)CVC3::TheoryCore [private]
processEquality(const Theorem &thm, ExprMap< Theorem > &q)CVC3::TheoryCore [private]
processFactQueue(EffortLevel effort=NORMAL)CVC3::TheoryCore [private]
processNotify(const Theorem &e, NotifyList *L)CVC3::TheoryCore [private]
processUpdates()CVC3::TheoryCore [private]
refineCounterExample()CVC3::TheoryCore [virtual]
reflexivityRule(const Expr &a)CVC3::Theory [inline]
registerAtom(const Expr &e, const Theorem &thm)CVC3::TheoryCore
CVC3::Theory::registerAtom(const Expr &e)CVC3::Theory [inline, virtual]
registerCoreSatAPI(CoreSatAPI *coreSatAPI)CVC3::TheoryCore [inline]
registerKinds(Theory *theory, std::vector< int > &kinds)CVC3::Theory
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)CVC3::Theory
resolveID(const std::string &name)CVC3::Theory
rewrite(const Expr &e)CVC3::TheoryCore [virtual]
rewriteAnd(const Expr &e)CVC3::Theory [inline]
rewriteAtomic(const Expr &e)CVC3::Theory [inline, virtual]
rewriteCC(const Expr &e)CVC3::Theory
rewriteCore(const Theorem &e)CVC3::TheoryCore [private]
rewriteCore(const Expr &e)CVC3::TheoryCore [private]
rewriteIte(const Expr &e)CVC3::TheoryCore [private]
rewriteLitCore(const Expr &e)CVC3::TheoryCore [private]
rewriteLiteral(const Expr &e)CVC3::TheoryCore
rewriteN(const Expr &e, int n)CVC3::TheoryCore [private]
rewriteOr(const Expr &e)CVC3::Theory [inline]
setFindLiteral(const Theorem &thm)CVC3::TheoryCore [private]
setIncomplete(const std::string &reason)CVC3::TheoryCore [private, virtual]
setInconsistent(const Theorem &e)CVC3::TheoryCore [virtual]
setResourceLimit(unsigned limit)CVC3::TheoryCore [inline]
setup(const Expr &e)CVC3::TheoryCore [inline, virtual]
setupCC(const Expr &e)CVC3::Theory
setupSubFormulas(const Expr &s, const Expr &e, const Theorem &thm)CVC3::TheoryCore [private]
setupTerm(const Expr &e, Theory *i, const Theorem &thm)CVC3::TheoryCore
setUsed()CVC3::Theory [inline, virtual]
simplify(const Expr &e)CVC3::TheoryCore [virtual]
simplifyExpr(const Expr &e)CVC3::Theory [inline]
simplifyOp(const Expr &e)CVC3::TheoryCore [virtual]
solve(const Theorem &e)CVC3::TheoryCore [virtual]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::Theory [inline]
substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2)CVC3::Theory [inline]
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVC3::Theory [inline]
substitutivityRule(const Expr &e, int changed, const Theorem &thm)CVC3::Theory [inline]
symmetryRule(const Theorem &a1_eq_a2)CVC3::Theory [inline]
Theory classCVC3::TheoryCore [friend]
CVC3::Theory::Theory(TheoryCore *theoryCore, const std::string &name)CVC3::Theory
TheoryCore(ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics)CVC3::TheoryCore
theoryCore()CVC3::Theory [inline]
theoryOf(int kind)CVC3::Theory
theoryOf(const Expr &e)CVC3::Theory
theoryUsed()CVC3::Theory [inline, virtual]
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::Theory [inline]
trueExpr()CVC3::Theory [inline]
typePred(const Expr &e)CVC3::TheoryCore [private]
update(const Theorem &e, const Expr &d)CVC3::TheoryCore [virtual]
updateCC(const Theorem &e, const Expr &d)CVC3::Theory
updateHelper(const Expr &e)CVC3::Theory
~Theory(void)CVC3::Theory [virtual]
~TheoryCore()CVC3::TheoryCore

Generated on Tue Jul 3 14:38:53 2007 for CVC3 by  doxygen 1.5.1