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
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_all_multTrigsInfoCVC3::TheoryQuant [private]
d_allInstCountCVC3::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_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_exprLastUpdatedPosCVC3::TheoryQuant [private]
d_fullTrigsCVC3::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_lastPartLevelCVC3::TheoryQuant [private]
d_lastPartPredsPosCVC3::TheoryQuant [private]
d_lastPartTermsPosCVC3::TheoryQuant [private]
d_lastPredsPosCVC3::TheoryQuant [private]
d_lastTermsPosCVC3::TheoryQuant [private]
d_lastUsefulGtermsPosCVC3::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_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_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_useAtomSemCVC3::TheoryQuant [private]
d_useEquCVC3::TheoryQuant [private]
d_useExprScoreCVC3::TheoryQuant [private]
d_usefulGtermsCVC3::TheoryQuant [private]
d_useFullTrigCVC3::TheoryQuant [private]
d_useInstAllCVC3::TheoryQuant [private]
d_useInstEndCVC3::TheoryQuant [private]
d_useInstGCacheCVC3::TheoryQuant [private]
d_useInstLCacheCVC3::TheoryQuant [private]
d_useInstTrueCVC3::TheoryQuant [private]
d_useLazyInstCVC3::TheoryQuant [private]
d_useMultCVC3::TheoryQuant [private]
d_useMultTrigCVC3::TheoryQuant [private]
d_useNewCVC3::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]
d_useTrigNewCVC3::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]
falseExpr()CVC3::Theory [inline]
find(const Expr &e)CVC3::Theory
findExpr(const Expr &e)CVC3::Theory [inline]
findInstAssumptions(const Theorem &thm)CVC3::TheoryQuant [private]
findReduced(const Expr &e)CVC3::Theory
findRef(const Expr &e)CVC3::Theory
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 [private]
getModelTerm(const Expr &e, std::vector< Expr > &v)CVC3::Theory
getModelValue(const Expr &e)CVC3::Theory
getName() constCVC3::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
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]
leavesAreSimp(const Expr &e)CVC3::Theory
loc_gterm(const std::vector< Expr > &border, const Expr &gterm, int pos)CVC3::TheoryQuant [private]
lookupVar(const std::string &name, Type *type)CVC3::Theory
mapTermsByType(const CDList< Expr > &terms)CVC3::TheoryQuant [private]
matchChild(const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)CVC3::TheoryQuant [inline, private]
matchChild(const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &env)CVC3::TheoryQuant [inline, 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]
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]
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]
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]
recursiveMap(const Expr &term)CVC3::TheoryQuant [private]
refineCounterExample()CVC3::Theory [inline, virtual]
reflexivityRule(const Expr &a)CVC3::Theory [inline]
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]
resolveID(const std::string &name)CVC3::Theory
rewrite(const Expr &e)CVC3::Theory [inline, virtual]
rewriteAnd(const Expr &e)CVC3::Theory [inline]
rewriteAtomic(const Expr &e)CVC3::Theory [inline, virtual]
rewriteCC(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(const Theorem &thm, size_t univ_id)CVC3::TheoryQuant [private]
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]
simplifyOp(const Expr &e)CVC3::Theory [virtual]
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 &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 Expr &e)CVC3::Theory
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
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 Tue Jul 3 14:39:18 2007 for CVC3 by  doxygen 1.5.1