| 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] |
| cacheHead | CVCL::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_allInstCount | CVCL::TheoryQuant | [private] |
| d_callThisRound | CVCL::TheoryQuant | [private] |
| d_contextCache | CVCL::TheoryQuant | [private] |
| d_contextMap | CVCL::TheoryQuant | [private] |
| d_contextTerms | CVCL::TheoryQuant | [private] |
| d_instCount | CVCL::TheoryQuant | [private] |
| d_instRound | CVCL::TheoryQuant | [private] |
| d_insts | CVCL::TheoryQuant | [private] |
| d_instThisRound | CVCL::TheoryQuant | [private] |
| d_maxQuantInst | CVCL::TheoryQuant | [private] |
| d_rules | CVCL::TheoryQuant | [private] |
| d_savedCache | CVCL::TheoryQuant | [private] |
| d_savedMap | CVCL::TheoryQuant | [private] |
| d_savedTerms | CVCL::TheoryQuant | [private] |
| d_savedTermsPos | CVCL::TheoryQuant | [private] |
| d_theoryUsed | CVCL::Theory | [protected] |
| d_typeExprMap | CVCL::TheoryQuant | [private] |
| d_univs | CVCL::TheoryQuant | [private] |
| d_univsContextPos | CVCL::TheoryQuant | [private] |
| d_univsPosFull | CVCL::TheoryQuant | [private] |
| d_univsSavedPos | CVCL::TheoryQuant | [private] |
| d_univsTriggers | CVCL::TheoryQuant | [private] |
| d_useAtomSem | CVCL::TheoryQuant | [private] |
| d_useLazyInst | CVCL::TheoryQuant | [private] |
| d_useNew | CVCL::TheoryQuant | [private] |
| d_useSemMatch | CVCL::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 >erm, 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 typedef | CVCL::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 | |
