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 | |
addGlobalLemma(const Theorem &thm, int priority=0) | CVC3::Theory | |
addNotifyEq(Theory *t, const Expr &e) | CVC3::TheoryCore | inline |
addSharedTerm(const Expr &e) | CVC3::TheoryCore | inlinevirtual |
addSplitter(const Expr &e, int priority=0) | CVC3::Theory | |
addToVarDB(const Expr &e) | CVC3::TheoryCore | |
assertEqualities(const Theorem &e) | CVC3::TheoryCore | privatevirtual |
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 | inlinevirtual |
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 | |
buildModel(Theorem &thm) | CVC3::TheoryCore | |
callTheoryPreprocess(const Expr &e) | CVC3::TheoryCore | |
checkAssertEqInvariant(const Theorem &e) | CVC3::Theory | inlinevirtual |
checkEquation(const Theorem &thm) | CVC3::TheoryCore | private |
checkSat(bool fullEffort) | CVC3::TheoryCore | inlinevirtual |
checkSATCore() | CVC3::TheoryCore | |
checkSolved(const Theorem &thm) | CVC3::TheoryCore | private |
checkType(const Expr &e) | CVC3::TheoryCore | virtual |
clearInPP() | CVC3::TheoryCore | inline |
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 | inlinevirtual |
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 class | CVC3::TheoryCore | friend |
createProofRules(TheoremManager *tm) | CVC3::TheoryCore | private |
d_assignment | CVC3::TheoryCore | private |
d_basicModelVars | CVC3::TheoryCore | private |
d_boundVarMap | CVC3::TheoryCore | private |
d_boundVarStack | CVC3::TheoryCore | private |
d_cm | CVC3::TheoryCore | private |
d_coreSatAPI | CVC3::TheoryCore | private |
d_currentRecursiveSimplifier | CVC3::TheoryCore | private |
d_exprTrans | CVC3::TheoryCore | private |
d_flags | CVC3::TheoryCore | private |
d_globals | CVC3::TheoryCore | private |
d_impliedLiterals | CVC3::TheoryCore | private |
d_impliedLiteralsIdx | CVC3::TheoryCore | private |
d_inAddFact | CVC3::TheoryCore | private |
d_inCheckSATCore | CVC3::TheoryCore | private |
d_incomplete | CVC3::TheoryCore | private |
d_inconsistent | CVC3::TheoryCore | private |
d_incThm | CVC3::TheoryCore | private |
d_inPP | CVC3::TheoryCore | private |
d_inRegisterAtom | CVC3::TheoryCore | private |
d_inUpdate | CVC3::TheoryCore | private |
d_notifyEq | CVC3::TheoryCore | private |
d_notifyObj | CVC3::TheoryCore | private |
d_parseCache | CVC3::TheoryCore | private |
d_parseCacheOther | CVC3::TheoryCore | private |
d_parseCacheTop | CVC3::TheoryCore | private |
d_predicates | CVC3::TheoryCore | private |
d_printer | CVC3::TheoryCore | private |
d_queue | CVC3::TheoryCore | private |
d_queueSE | CVC3::TheoryCore | private |
d_resourceLimit | CVC3::TheoryCore | private |
d_rules | CVC3::TheoryCore | private |
d_simplifiedModelVars | CVC3::TheoryCore | private |
d_simplifyInPlace | CVC3::TheoryCore | private |
d_solver | CVC3::TheoryCore | private |
d_statistics | CVC3::TheoryCore | private |
d_tccCache | CVC3::TheoryCore | private |
d_terms | CVC3::TheoryCore | private |
d_termTheorems | CVC3::TheoryCore | private |
d_theories | CVC3::TheoryCore | private |
d_theoryMap | CVC3::TheoryCore | private |
d_theoryUsed | CVC3::Theory | protected |
d_timeBase | CVC3::TheoryCore | private |
d_timeLimit | CVC3::TheoryCore | private |
d_tm | CVC3::TheoryCore | private |
d_translator | CVC3::TheoryCore | private |
d_typeComputer | CVC3::TheoryCore | private |
d_update_data | CVC3::TheoryCore | private |
d_update_thms | CVC3::TheoryCore | private |
d_varAssignments | CVC3::TheoryCore | private |
d_varModelMap | CVC3::TheoryCore | private |
d_vars | CVC3::TheoryCore | private |
EffortLevel enum name | CVC3::TheoryCore | private |
enqueueFact(const Theorem &e) | CVC3::TheoryCore | virtual |
enqueueSE(const Theorem &thm) | CVC3::TheoryCore | virtual |
falseExpr() | CVC3::Theory | inline |
find(const Expr &e) | CVC3::Theory | |
findExpr(const Expr &e) | CVC3::Theory | inline |
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::TheoryCore | virtual |
FULL enum value | CVC3::TheoryCore | private |
getAssignment() | CVC3::TheoryCore | |
getBaseType(const Expr &e) | CVC3::Theory | |
getBaseType(const Type &tp) | CVC3::Theory | |
getCM() const | CVC3::TheoryCore | inline |
getCommonRules() | CVC3::Theory | inline |
getCoreRules() const | CVC3::TheoryCore | inline |
getCurQuantLevel() | CVC3::TheoryCore | |
getEM() | CVC3::Theory | inline |
getExprTrans() const | CVC3::TheoryCore | inline |
getFlags() const | CVC3::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() const | CVC3::Theory | inline |
getNumTheories() | CVC3::Theory | |
getPredicates() | CVC3::TheoryCore | inline |
getQuantLevelForTerm(const Expr &e) | CVC3::TheoryCore | |
getResource() | CVC3::TheoryCore | inline |
getResourceLimit() | CVC3::TheoryCore | inline |
getStatistics() const | CVC3::TheoryCore | inline |
getTCC(const Expr &e) | CVC3::Theory | |
getTerms() | CVC3::TheoryCore | inline |
getTheoremForTerm(const Expr &e) | CVC3::TheoryCore | |
getTM() const | CVC3::TheoryCore | inline |
getTranslator() const | CVC3::TheoryCore | inline |
getTypePred(const Type &t, const Expr &e) | CVC3::Theory | |
getValue(Expr e) | CVC3::TheoryCore | |
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 | inlinevirtual |
inconsistentThm() | CVC3::TheoryCore | inline |
initTimeLimit() | CVC3::TheoryCore | |
installID(const std::string &name, const Expr &e) | CVC3::Theory | |
inUpdate() | CVC3::TheoryCore | inline |
isBasicKind(int kind) | CVC3::TheoryCore | private |
isLeaf(const Expr &e) | CVC3::Theory | inline |
isLeafIn(const Expr &e1, const Expr &e2) | CVC3::Theory | |
leavesAreSimp(const Expr &e) | CVC3::Theory | |
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 | |
LOW enum value | CVC3::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 value | CVC3::TheoryCore | private |
notifyInconsistent(const Theorem &thm) | CVC3::Theory | inlinevirtual |
numImpliedLiterals() | CVC3::TheoryCore | inline |
okToEnqueue() | 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 |
printSmtLibShared(ExprStream &os, const Expr &e) | CVC3::TheoryCore | private |
processCond(const Expr &e, int i) | 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 |
refineCounterExample(Theorem &thm) | CVC3::TheoryCore | |
reflexivityRule(const Expr &a) | CVC3::Theory | inline |
registerAtom(const Expr &e, const Theorem &thm) | CVC3::TheoryCore | virtual |
CVC3::Theory::registerAtom(const Expr &e) | CVC3::Theory | inlinevirtual |
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 | |
renameExpr(const Expr &e) | 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 | inlinevirtual |
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::Theory | |
rewriteLitCore(const Expr &e) | CVC3::TheoryCore | private |
rewriteLiteral(const Expr &e) | CVC3::TheoryCore | |
rewriteOr(const Expr &e) | CVC3::Theory | inline |
setFindLiteral(const Theorem &thm) | CVC3::TheoryCore | private |
setIncomplete(const std::string &reason) | CVC3::TheoryCore | privatevirtual |
setInconsistent(const Theorem &e) | CVC3::TheoryCore | virtual |
setInPP() | CVC3::TheoryCore | inline |
setResourceLimit(unsigned limit) | CVC3::TheoryCore | inline |
setTimeLimit(unsigned limit) | CVC3::TheoryCore | |
setup(const Expr &e) | CVC3::TheoryCore | inlinevirtual |
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 | inlinevirtual |
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 &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 |
tccCache() | CVC3::TheoryCore | inline |
Theory class | CVC3::TheoryCore | friend |
CVC3::Theory::Theory(TheoryCore *theoryCore, const std::string &name) | CVC3::Theory | |
theoryCore() | CVC3::Theory | inline |
TheoryCore(ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics) | CVC3::TheoryCore | |
theoryOf(int kind) | CVC3::Theory | |
theoryOf(const Type &e) | CVC3::Theory | |
theoryOf(const Expr &e) | CVC3::Theory | |
theoryPreprocess(const Expr &e) | CVC3::Theory | inlinevirtual |
theoryUsed() | CVC3::Theory | inlinevirtual |
timeLimitReached() | CVC3::TheoryCore | private |
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 |
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::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 | |