CVC3  2.4.1
CVC3::TheoryQuant Member List

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

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