Main Page | Modules | Namespace List | Class Hierarchy | Alphabetical List | Class List | Directories | File List | Namespace Members | Class Members | File Members | Related Pages | Search for 

CVCL::TheoryQuant Member List

This is the complete list of members for CVCL::TheoryQuant, including all inherited members.

addBoundVar(const std::string &name, const Type &type)CVCL::Theory
addBoundVar(const std::string &name, const Type &type, const Expr &def)CVCL::Theory
addSharedTerm(const Expr &e)CVCL::TheoryQuant [inline, virtual]
addSplitter(const Expr &e, int priority=0)CVCL::Theory
assertEqualities(const Theorem &e)CVCL::Theory [virtual]
assertFact(const Theorem &e)CVCL::TheoryQuant [virtual]
assertTypePred(const Expr &e, const Theorem &pred)CVCL::Theory [inline, virtual]
assignValue(const Expr &t, const Expr &val)CVCL::Theory [virtual]
assignValue(const Theorem &thm)CVCL::Theory [virtual]
boolType()CVCL::Theory [inline]
cacheHeadCVCL::TheoryQuant [private]
checkSat(bool fullEffort)CVCL::TheoryQuant [virtual]
checkType(const Expr &e)CVCL::Theory [inline, virtual]
computeBaseType(const Type &tp)CVCL::Theory [inline, virtual]
computeModel(const Expr &e, std::vector< Expr > &vars)CVCL::Theory [inline, virtual]
computeModelBasic(const std::vector< Expr > &v)CVCL::Theory [inline, virtual]
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVCL::Theory [virtual]
computeTCC(const Expr &e)CVCL::TheoryQuant [virtual]
computeType(const Expr &e)CVCL::TheoryQuant [virtual]
computeTypePred(const Type &t, const Expr &e)CVCL::Theory [inline, virtual]
createProofRules()CVCL::TheoryQuant
d_allInstCountCVCL::TheoryQuant [private]
d_callThisRoundCVCL::TheoryQuant [private]
d_contextCacheCVCL::TheoryQuant [private]
d_contextMapCVCL::TheoryQuant [private]
d_contextTermsCVCL::TheoryQuant [private]
d_instCountCVCL::TheoryQuant [private]
d_instRoundCVCL::TheoryQuant [private]
d_instsCVCL::TheoryQuant [private]
d_instThisRoundCVCL::TheoryQuant [private]
d_maxQuantInstCVCL::TheoryQuant [private]
d_rulesCVCL::TheoryQuant [private]
d_savedCacheCVCL::TheoryQuant [private]
d_savedMapCVCL::TheoryQuant [private]
d_savedTermsCVCL::TheoryQuant [private]
d_savedTermsPosCVCL::TheoryQuant [private]
d_theoryUsedCVCL::Theory [protected]
d_typeExprMapCVCL::TheoryQuant [private]
d_univsCVCL::TheoryQuant [private]
d_univsContextPosCVCL::TheoryQuant [private]
d_univsPosFullCVCL::TheoryQuant [private]
d_univsSavedPosCVCL::TheoryQuant [private]
d_univsTriggersCVCL::TheoryQuant [private]
d_useAtomSemCVCL::TheoryQuant [private]
d_useLazyInstCVCL::TheoryQuant [private]
d_useNewCVCL::TheoryQuant [private]
d_useSemMatchCVCL::TheoryQuant [private]
enqueueEquality(const Theorem &e)CVCL::Theory [virtual]
enqueueFact(const Theorem &e)CVCL::Theory [virtual]
enqueueInst(const Theorem thm)CVCL::TheoryQuant [private]
falseExpr()CVCL::Theory [inline]
find(const Expr &e)CVCL::Theory
findExpr(const Expr &e)CVCL::Theory [inline]
findInstAssumptions(const Theorem &thm)CVCL::TheoryQuant [private]
getBaseType(const Expr &e)CVCL::Theory
getBaseType(const Type &tp)CVCL::Theory
getCommonRules()CVCL::Theory [inline]
getEM()CVCL::Theory [inline]
getHead(const Expr &e)CVCL::TheoryQuant [private]
getModelTerm(const Expr &e, std::vector< Expr > &v)CVCL::Theory
getModelValue(const Expr &e)CVCL::Theory
getName() const CVCL::Theory [inline]
getNumTheories()CVCL::Theory
getTCC(const Expr &e)CVCL::Theory
getTypePred(const Type &t, const Expr &e)CVCL::Theory
goodSynMatch(const Expr &e, const std::vector< Expr > &boundVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)CVCL::TheoryQuant [private]
hasGoodSemInst(const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)CVCL::TheoryQuant [private]
hasGoodSynInst(const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)CVCL::TheoryQuant [private]
hasTheory(int kind)CVCL::Theory
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVCL::Theory [inline]
inconsistent()CVCL::Theory [virtual]
installID(const std::string &name, const Expr &e)CVCL::Theory
instantiate(Theorem univ, bool all, bool savedMap, size_t newIndex)CVCL::TheoryQuant [private]
isLeaf(const Expr &e)CVCL::Theory [inline]
isLeafIn(const Expr &e1, const Expr &e2)CVCL::Theory
leavesAreSimp(const Expr &e)CVCL::Theory
lookupVar(const std::string &name, Type *type)CVCL::Theory
mapTermsByType(const CDList< Expr > &terms)CVCL::TheoryQuant [private]
naiveCheckSat(bool)CVCL::TheoryQuant [private]
newFunction(const std::string &name, const Type &type, bool computeTransClosure)CVCL::Theory
newFunction(const std::string &name, const Type &type, const Expr &def)CVCL::Theory
newTypeExpr(const std::string &name)CVCL::Theory
newTypeExpr(const std::string &name, const Type &def)CVCL::Theory
newVar(const std::string &name, const Type &type)CVCL::Theory
newVar(const std::string &name, const Type &type, const Expr &def)CVCL::Theory
notifyInconsistent(const Theorem &thm)CVCL::TheoryQuant [virtual]
parseExpr(const Expr &e)CVCL::Theory [virtual]
parseExprOp(const Expr &e)CVCL::TheoryQuant [virtual]
print(ExprStream &os, const Expr &e)CVCL::TheoryQuant [virtual]
recGoodSemMatch(const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)CVCL::TheoryQuant [private]
recInstantiate(Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)CVCL::TheoryQuant [private]
recSynMatch(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)CVCL::TheoryQuant [private]
recursiveMap(const Expr &term)CVCL::TheoryQuant [private]
refineCounterExample()CVCL::Theory [inline, virtual]
reflexivityRule(const Expr &a)CVCL::Theory [inline]
registerKinds(Theory *theory, std::vector< int > &kinds)CVCL::Theory
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)CVCL::Theory
resolveID(const std::string &name)CVCL::Theory
rewrite(const Expr &e)CVCL::Theory [inline, virtual]
rewriteAnd(const Expr &e)CVCL::Theory [inline]
rewriteAtomic(const Expr &e)CVCL::Theory [inline, virtual]
rewriteCC(const Expr &e)CVCL::Theory
rewriteOr(const Expr &e)CVCL::Theory [inline]
semCheckSat(bool)CVCL::TheoryQuant [private]
semInst(const Theorem &univ, size_t tBegin)CVCL::TheoryQuant [private]
setIncomplete(const std::string &reason)CVCL::Theory [virtual]
setInconsistent(const Theorem &e)CVCL::Theory [virtual]
setup(const Expr &e)CVCL::TheoryQuant [virtual]
setupCC(const Expr &e)CVCL::Theory
setupTriggers(const Theorem &thm)CVCL::TheoryQuant [private]
simplify(const Expr &e, bool forceRebuild=true)CVCL::Theory [virtual]
simplifyExpr(const Expr &e, bool forceRebuild=true)CVCL::Theory [inline]
simplifyOp(const Expr &e)CVCL::Theory [virtual]
simplifyRec(const Expr &e)CVCL::Theory [virtual]
solve(const Theorem &e)CVCL::Theory [inline, virtual]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVCL::Theory [inline]
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVCL::Theory [inline]
subtypePredicate(const Expr &e)CVCL::Theory
symmetryRule(const Theorem &a1_eq_a2)CVCL::Theory [inline]
synCheckSat(bool)CVCL::TheoryQuant [private]
synInst(const Theorem &univ, size_t tBegin)CVCL::TheoryQuant [private]
Theory(TheoryCore *theoryCore, const std::string &name)CVCL::Theory
theoryCore()CVCL::Theory [inline]
theoryOf(int kind)CVCL::Theory
theoryOf(const Expr &e)CVCL::Theory
TheoryQuant(TheoryCore *core)CVCL::TheoryQuant
theoryUsed()CVCL::Theory [inline, virtual]
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVCL::Theory [inline]
trueExpr()CVCL::Theory [inline]
typeMap typedefCVCL::TheoryQuant [private]
typePred(const Expr &e)CVCL::Theory
update(const Theorem &e, const Expr &d)CVCL::TheoryQuant [virtual]
updateCC(const Theorem &e, const Expr &d)CVCL::Theory
updateHelper(const Expr &e)CVCL::Theory
~Theory(void)CVCL::Theory [virtual]
~TheoryQuant()CVCL::TheoryQuant

Generated on Thu Apr 13 16:57:44 2006 for CVC Lite by  doxygen 1.4.4