CVC3

CVC3::TheoryQuant Member List

This is the complete list of members for CVC3::TheoryQuant, including all inherited members.
add_parent(const Expr &parent)CVC3::TheoryQuant [inline, private]
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
addNotify(const Expr &e)CVC3::TheoryQuant [private]
addSharedTerm(const Expr &e)CVC3::TheoryQuant [inline, virtual]
addSplitter(const Expr &e, int priority=0)CVC3::Theory
arrayHeuristic(const Trigger &trig, size_t univid)CVC3::TheoryQuant [private]
arrayIndexName(const Expr &e)CVC3::TheoryQuant [private]
assertEqualities(const Theorem &e)CVC3::Theory [virtual]
assertFact(const Theorem &e)CVC3::TheoryQuant [virtual]
assertTypePred(const Expr &e, const Theorem &pred)CVC3::Theory [inline, virtual]
assignValue(const Expr &t, const Expr &val)CVC3::Theory [virtual]
assignValue(const Theorem &thm)CVC3::Theory [virtual]
backList(const Expr &ex)CVC3::TheoryQuant [inline, private]
boolType()CVC3::Theory [inline]
cacheHeadCVC3::TheoryQuant [private]
canMatch(const Expr &t1, const Expr &t2, ExprMap< Expr > &env)CVC3::TheoryQuant [private]
checkAssertEqInvariant(const Theorem &e)CVC3::Theory [inline, virtual]
checkSat(bool fullEffort)CVC3::TheoryQuant [virtual]
checkType(const Expr &e)CVC3::Theory [inline, virtual]
collectChangedTerms(CDList< Expr > &changed_terms)CVC3::TheoryQuant [private]
combineOldNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)CVC3::TheoryQuant [private]
computeBaseType(const Type &tp)CVC3::Theory [inline, virtual]
computeModel(const Expr &e, std::vector< Expr > &vars)CVC3::Theory [inline, virtual]
computeModelBasic(const std::vector< Expr > &v)CVC3::Theory [inline, virtual]
computeModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory [virtual]
computeTCC(const Expr &e)CVC3::TheoryQuant [virtual]
computeType(const Expr &e)CVC3::TheoryQuant [virtual]
computeTypePred(const Type &t, const Expr &e)CVC3::Theory [inline, virtual]
createProofRules()CVC3::TheoryQuant
d_abInstCountCVC3::TheoryQuant [private]
d_all_multTrigsInfoCVC3::TheoryQuant [private]
d_allInstCountCVC3::TheoryQuant [private]
d_allInstCount2CVC3::TheoryQuant [private]
d_allInstsCVC3::TheoryQuant [private]
d_allmap_trigsCVC3::TheoryQuant [private]
d_alloutCVC3::TheoryQuant [private]
d_alltrig_listCVC3::TheoryQuant [private]
d_arrayIndicCVC3::TheoryQuant [private]
d_arrayTrigsCVC3::TheoryQuant [private]
d_bindGlobalHistoryCVC3::TheoryQuant [private]
d_bindGlobalThmHistoryCVC3::TheoryQuant [private]
d_bindHistoryCVC3::TheoryQuant [private]
d_cacheTheoremCVC3::TheoryQuant [private]
d_cacheThmPosCVC3::TheoryQuant [private]
d_callThisRoundCVC3::TheoryQuant [private]
d_contextCacheCVC3::TheoryQuant [private]
d_contextMapCVC3::TheoryQuant [private]
d_contextTermsCVC3::TheoryQuant [private]
d_curMaxExprScoreCVC3::TheoryQuant [private]
d_eq_listCVC3::TheoryQuant [private]
d_eq_posCVC3::TheoryQuant [private]
d_eqsCVC3::TheoryQuant [private]
d_eqs_posCVC3::TheoryQuant [private]
d_eqsUpdateCVC3::TheoryQuant [private]
d_exprLastUpdatedPosCVC3::TheoryQuant [private]
d_fullTrigsCVC3::TheoryQuant [private]
d_gBindQueueCVC3::TheoryQuant [private]
d_gfactLimitCVC3::TheoryQuant [private]
d_gUnivQueueCVC3::TheoryQuant [private]
d_hasMoreBVsCVC3::TheoryQuant [private]
d_hasTriggersCVC3::TheoryQuant [private]
d_indexExprCVC3::TheoryQuant [private]
d_indexScoreCVC3::TheoryQuant [private]
d_inEndCVC3::TheoryQuant [private]
d_initMaxScoreCVC3::TheoryQuant [private]
d_instCountCVC3::TheoryQuant [private]
d_instHistoryCVC3::TheoryQuant [private]
d_instHistoryGlobalCVC3::TheoryQuant [private]
d_instsCVC3::TheoryQuant [private]
d_instThisRoundCVC3::TheoryQuant [private]
d_lastArrayPosCVC3::TheoryQuant [private]
d_lastEqsUpdatePosCVC3::TheoryQuant [private]
d_lastPartLevelCVC3::TheoryQuant [private]
d_lastPartPredsPosCVC3::TheoryQuant [private]
d_lastPartTermsPosCVC3::TheoryQuant [private]
d_lastPredsPosCVC3::TheoryQuant [private]
d_lastTermsPosCVC3::TheoryQuant [private]
d_lastUsefulGtermsPosCVC3::TheoryQuant [private]
d_maxILCVC3::TheoryQuant [private]
d_maxILReachedCVC3::TheoryQuant [private]
d_maxInstCVC3::TheoryQuant [private]
d_maxNaiveCallCVC3::TheoryQuant [private]
d_maxQuantInstCVC3::TheoryQuant [private]
d_mtrigs_bvorderCVC3::TheoryQuant [private]
d_mtrigs_instCVC3::TheoryQuant [private]
d_multitrigs_mapsCVC3::TheoryQuant [private]
d_multTriggersCVC3::TheoryQuant [private]
d_multTrigsCVC3::TheoryQuant [private]
d_mybvsCVC3::TheoryQuant [private]
d_offset_multi_trigCVC3::TheoryQuant [private]
d_parent_listCVC3::TheoryQuant [private]
d_partCalledCVC3::TheoryQuant [private]
d_partTriggersCVC3::TheoryQuant [private]
d_partTrigsCVC3::TheoryQuant [private]
d_rawUnivsCVC3::TheoryQuant [private]
d_rawUnivsSavedPosCVC3::TheoryQuant [private]
d_rulesCVC3::TheoryQuant [private]
d_same_head_exprCVC3::TheoryQuant [private]
d_savedCacheCVC3::TheoryQuant [private]
d_savedMapCVC3::TheoryQuant [private]
d_savedTermsCVC3::TheoryQuant [private]
d_savedTermsPosCVC3::TheoryQuant [private]
d_simplifiedThmQueueCVC3::TheoryQuant [private]
d_subTermsMapCVC3::TheoryQuant [private]
d_tempBindsCVC3::TheoryQuant [private]
d_theoryUsedCVC3::Theory [protected]
d_thmCountCVC3::TheoryQuant [private]
d_totalInstCountCVC3::TheoryQuant [private]
d_totalThmCountCVC3::TheoryQuant [private]
d_trans2_foundCVC3::TheoryQuant [private]
d_trans2_numCVC3::TheoryQuant [private]
d_trans_backCVC3::TheoryQuant [private]
d_trans_forwCVC3::TheoryQuant [private]
d_trans_foundCVC3::TheoryQuant [private]
d_trans_numCVC3::TheoryQuant [private]
d_translateCVC3::TheoryQuant [private]
d_transThmCVC3::TheoryQuant [private]
d_trueInstCountCVC3::TheoryQuant [private]
d_typeExprMapCVC3::TheoryQuant [private]
d_univsCVC3::TheoryQuant [private]
d_univsContextPosCVC3::TheoryQuant [private]
d_univsPartSavedPosCVC3::TheoryQuant [private]
d_univsPosFullCVC3::TheoryQuant [private]
d_univsQueueCVC3::TheoryQuant [private]
d_univsSavedPosCVC3::TheoryQuant [private]
d_useCompleteInstCVC3::TheoryQuant [private]
d_useEquCVC3::TheoryQuant [private]
d_useExprScoreCVC3::TheoryQuant [private]
d_usefulGtermsCVC3::TheoryQuant [private]
d_useFullTrigCVC3::TheoryQuant [private]
d_useGFactCVC3::TheoryQuant [private]
d_useInstAllCVC3::TheoryQuant [private]
d_useInstGCacheCVC3::TheoryQuant [private]
d_useInstLCacheCVC3::TheoryQuant [private]
d_useInstThmCacheCVC3::TheoryQuant [private]
d_useInstTrueCVC3::TheoryQuant [private]
d_useLazyInstCVC3::TheoryQuant [private]
d_useManTrigCVC3::TheoryQuant [private]
d_useMultCVC3::TheoryQuant [private]
d_useMultTrigCVC3::TheoryQuant [private]
d_useNaiveInstCVC3::TheoryQuant [private]
d_useNewCVC3::TheoryQuant [private]
d_useNewEquCVC3::TheoryQuant [private]
d_usePartCVC3::TheoryQuant [private]
d_usePartTrigCVC3::TheoryQuant [private]
d_usePolarityCVC3::TheoryQuant [private]
d_usePullVarCVC3::TheoryQuant [private]
d_useSemMatchCVC3::TheoryQuant [private]
d_useTransCVC3::TheoryQuant [private]
d_useTrans2CVC3::TheoryQuant [private]
d_useTrigLoopCVC3::TheoryQuant [private]
debug(int i)CVC3::TheoryQuant
defaultDivideExprCVC3::TheoryQuant [private]
defaultMinusExprCVC3::TheoryQuant [private]
defaultMultExprCVC3::TheoryQuant [private]
defaultPlusExprCVC3::TheoryQuant [private]
defaultPowExprCVC3::TheoryQuant [private]
defaultReadExprCVC3::TheoryQuant [private]
defaultWriteExprCVC3::TheoryQuant [private]
delNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)CVC3::TheoryQuant [private]
enqueueFact(const Theorem &e)CVC3::Theory [virtual]
enqueueInst(const Theorem, const Theorem)CVC3::TheoryQuant [private]
enqueueInst(const Theorem &univ, const std::vector< Expr > &bind, const Expr &gterm)CVC3::TheoryQuant [private]
enqueueInst(size_t univ_id, const std::vector< Expr > &bind, const Expr &gterm)CVC3::TheoryQuant [private]
enqueueInst(const Theorem &univ, Trigger &trig, const std::vector< Expr > &binds, const Expr &gterm)CVC3::TheoryQuant [private]
enqueueSE(const Theorem &e)CVC3::Theory [virtual]
exprMap2string(const ExprMap< Expr > &vec)CVC3::TheoryQuant [private]
exprMap2stringSig(const ExprMap< Expr > &vec)CVC3::TheoryQuant [private]
exprMap2stringSimplify(const ExprMap< Expr > &vec)CVC3::TheoryQuant [private]
falseExpr()CVC3::Theory [inline]
find(const Expr &e)CVC3::Theory
findExpr(const Expr &e)CVC3::Theory [inline]
findInstAssumptions(const Theorem &thm)CVC3::TheoryQuant [private]
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::Theory [inline, virtual]
forwList(const Expr &ex)CVC3::TheoryQuant [inline, private]
generalTrig(const Expr &trig, ExprMap< Expr > &bvs)CVC3::TheoryQuant [private]
getBaseType(const Expr &e)CVC3::Theory
getBaseType(const Type &tp)CVC3::Theory
getCommonRules()CVC3::Theory [inline]
getEM()CVC3::Theory [inline]
getExprScore(const Expr &e)CVC3::TheoryQuant [inline, private]
getHead(const Expr &e)CVC3::TheoryQuant [private]
getHeadExpr(const Expr &e)CVC3::TheoryQuant [private]
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::Theory
getName() const CVC3::Theory [inline]
getNumTheories()CVC3::Theory
getSubTerms(const Expr &e)CVC3::TheoryQuant [private]
getTCC(const Expr &e)CVC3::Theory
getTypePred(const Type &t, const Expr &e)CVC3::Theory
goodSynMatch(const Expr &e, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBindsTerm, std::vector< Expr > &instGterm, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
goodSynMatchNewTrig(const Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
goodSynMatchNewTrig(const Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const Expr &gterm)CVC3::TheoryQuant [private]
hasGoodSemInst(const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)CVC3::TheoryQuant [private]
hasGoodSynInstNewTrig(Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
hasGoodSynInstNewTrigOld(Trigger &trig, std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
hasGoodSynMultiInst(const Expr &e, std::vector< Expr > &bVars, std::vector< std::vector< Expr > > &instSet, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
hasTheory(int kind)CVC3::Theory
help(int i)CVC3::TheoryQuant
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::Theory [inline]
inconsistent()CVC3::Theory [virtual]
installID(const std::string &name, const Expr &e)CVC3::Theory
instantiate(Theorem univ, bool all, bool savedMap, size_t newIndex)CVC3::TheoryQuant [private]
insted(const Theorem &univ, const std::vector< Expr > &binds)CVC3::TheoryQuant [private]
isLeaf(const Expr &e)CVC3::Theory [inline]
isLeafIn(const Expr &e1, const Expr &e2)CVC3::Theory
isTrans2Like(const std::vector< Expr > &all_terms, const Expr &tr2)CVC3::TheoryQuant [private]
isTransLike(const std::vector< Expr > &cur_trig)CVC3::TheoryQuant [private]
iterBKList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)CVC3::TheoryQuant [inline, private]
iterFWList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)CVC3::TheoryQuant [inline, private]
leavesAreSimp(const Expr &e)CVC3::Theory
loc_gterm(const std::vector< Expr > &border, const Expr &gterm, int pos)CVC3::TheoryQuant [private]
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
mapTermsByType(const CDList< Expr > &terms)CVC3::TheoryQuant [private]
matchListNew(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs, const CDList< Expr > &list, size_t gbegin, size_t gend)CVC3::TheoryQuant [private]
matchListOld(const CDList< Expr > &list, size_t gbegin, size_t gend)CVC3::TheoryQuant [private]
MAX_TRIG_BVSCVC3::TheoryQuant [private, static]
multMatchChild(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false)CVC3::TheoryQuant [inline, private]
multMatchTop(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)CVC3::TheoryQuant [inline, private]
naiveCheckSat(bool)CVC3::TheoryQuant [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
newTopMatch(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)CVC3::TheoryQuant [private]
newTopMatchBackupOnly(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)CVC3::TheoryQuant [private]
newTopMatchNoSig(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)CVC3::TheoryQuant [private]
newTopMatchSig(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)CVC3::TheoryQuant [private]
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::TheoryQuant [virtual]
null_cdlistCVC3::TheoryQuant [private]
parseExpr(const Expr &e)CVC3::Theory [virtual]
parseExprOp(const Expr &e)CVC3::TheoryQuant [virtual]
partial_calledCVC3::TheoryQuant [private]
print(ExprStream &os, const Expr &e)CVC3::TheoryQuant [virtual]
pushBackList(const Expr &node, Expr ex)CVC3::TheoryQuant [inline, private]
pushForwList(const Expr &node, Expr ex)CVC3::TheoryQuant [inline, private]
recGeneralTrig(const Expr &trig, ExprMap< Expr > &bvs, size_t &mybvs_count)CVC3::TheoryQuant [private]
recGoodSemMatch(const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)CVC3::TheoryQuant [private]
recInstantiate(Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)CVC3::TheoryQuant [private]
recMultMatch(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)CVC3::TheoryQuant [private]
recMultMatchDebug(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)CVC3::TheoryQuant [private]
recMultMatchNewWay(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)CVC3::TheoryQuant [private]
recMultMatchOldWay(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)CVC3::TheoryQuant [private]
recSearchCover(const std::vector< Expr > &border, const std::vector< Expr > &mtrigs, int cur_depth, std::vector< std::vector< Expr > > &instSet, std::vector< Expr > &cur_inst)CVC3::TheoryQuant [private]
recSynMatch(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)CVC3::TheoryQuant [private]
recSynMatchBackupOnly(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)CVC3::TheoryQuant [private]
recursiveMap(const Expr &term)CVC3::TheoryQuant [private]
refineCounterExample()CVC3::Theory [inline, virtual]
reflexivityRule(const Expr &a)CVC3::Theory [inline]
registerAtom(const Expr &e, const Theorem &thm)CVC3::Theory [virtual]
registerAtom(const Expr &e)CVC3::Theory [inline, virtual]
registerKinds(Theory *theory, std::vector< int > &kinds)CVC3::Theory
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)CVC3::Theory
registerTrig(ExprMap< ExprMap< std::vector< dynTrig > * > * > &cur_trig_map, Trigger trig, const std::vector< Expr > thmBVs, size_t univ_id)CVC3::TheoryQuant [private]
registerTrigReal(Trigger trig, const std::vector< Expr >, size_t univ_id)CVC3::TheoryQuant [private]
renameExpr(const Expr &e)CVC3::Theory
resolveID(const std::string &name)CVC3::Theory
rewrite(const Expr &e)CVC3::TheoryQuant [private, virtual]
rewriteAnd(const Expr &e)CVC3::Theory [inline]
rewriteAtomic(const Expr &e)CVC3::Theory [inline, virtual]
rewriteCC(const Expr &e)CVC3::Theory
rewriteIte(const Expr &e)CVC3::Theory
rewriteOr(const Expr &e)CVC3::Theory [inline]
saveContext()CVC3::TheoryQuant [private]
searchCover(const Expr &thm, const std::vector< Expr > &border, std::vector< std::vector< Expr > > &instSet)CVC3::TheoryQuant [private]
semCheckSat(bool)CVC3::TheoryQuant [private]
semInst(const Theorem &univ, size_t tBegin)CVC3::TheoryQuant [private]
sendInstNew()CVC3::TheoryQuant [private]
setGround(const Expr &gterm, const Expr &trig, const Theorem &univ, const std::vector< Expr > &subTerms)CVC3::TheoryQuant [private]
setIncomplete(const std::string &reason)CVC3::Theory [virtual]
setInconsistent(const Theorem &e)CVC3::Theory [virtual]
setTrans2Found(const Expr &comb)CVC3::TheoryQuant [inline, private]
setTransFound(const Expr &comb)CVC3::TheoryQuant [inline, private]
setup(const Expr &e)CVC3::TheoryQuant [virtual]
setupCC(const Expr &e)CVC3::Theory
setupTriggers(ExprMap< ExprMap< std::vector< dynTrig > * > * > &trig_maps, const Theorem &thm, size_t univs_id)CVC3::TheoryQuant [private]
setUsed()CVC3::Theory [inline, virtual]
simplify(const Expr &e)CVC3::Theory [virtual]
simplifyExpr(const Expr &e)CVC3::Theory [inline]
simplifyExprMap(ExprMap< Expr > &orgExprMap)CVC3::TheoryQuant [private]
simplifyOp(const Expr &e)CVC3::Theory [virtual]
simplifyVectorExprMap(std::vector< ExprMap< Expr > > &orgVectorExprMap)CVC3::TheoryQuant [private]
simpRAWList(const Expr &org)CVC3::TheoryQuant [private]
solve(const Theorem &e)CVC3::Theory [inline, virtual]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::Theory [inline]
substitutivityRule(const Expr &e, const Theorem &t)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]
synCheckSat(ExprMap< ExprMap< std::vector< dynTrig > * > * > &, bool)CVC3::TheoryQuant [private]
synCheckSat(bool)CVC3::TheoryQuant [private]
synFullInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
synInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
synMatchTopPred(const Expr &gterm, const Trigger trig, ExprMap< Expr > &env)CVC3::TheoryQuant [private]
synMultInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
synNewInst(size_t univ_id, const std::vector< Expr > &binds, const Expr &gterm, const Trigger &trig)CVC3::TheoryQuant [private]
synPartInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)CVC3::TheoryQuant [private]
Theory(TheoryCore *theoryCore, const std::string &name)CVC3::Theory
theoryCore()CVC3::Theory [inline]
theoryOf(int kind)CVC3::Theory
theoryOf(const Type &e)CVC3::Theory
theoryOf(const Expr &e)CVC3::Theory
theoryPreprocess(const Expr &e)CVC3::TheoryQuant [private, virtual]
TheoryQuant(TheoryCore *core)CVC3::TheoryQuant
theoryUsed()CVC3::Theory [inline, virtual]
trans2Found(const Expr &comb)CVC3::TheoryQuant [inline, private]
transFound(const Expr &comb)CVC3::TheoryQuant [inline, private]
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::Theory [inline]
trueExpr()CVC3::Theory [inline]
typeMap typedefCVC3::TheoryQuant [private]
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::TheoryQuant [virtual]
updateCC(const Theorem &e, const Expr &d)CVC3::Theory
updateHelper(const Expr &e)CVC3::Theory
~Theory(void)CVC3::Theory [virtual]
~TheoryQuant()CVC3::TheoryQuant
Generated on Thu Sep 1 2011 19:35:14 for CVC3 by  doxygen 1.7.3