| addBoundVar(const std::string &name, const Type &type) | CVCL::Theory | |
| addBoundVar(const std::string &name, const Type &type, const Expr &def) | CVCL::Theory | |
| addFact(const Theorem &e) | CVCL::TheoryCore | |
| addSharedTerm(const Expr &e) | CVCL::TheoryCore | [inline, virtual] |
| addSplitter(const Expr &e, int priority=0) | CVCL::Theory | |
| addToVarDB(const Expr &e) | CVCL::TheoryCore | |
| assertEqualities(const Theorem &e) | CVCL::TheoryCore | [private, virtual] |
| assertFact(const Theorem &e) | CVCL::TheoryCore | [virtual] |
| assertFactCore(const Theorem &e) | CVCL::TheoryCore | [private] |
| assertFormula(const Theorem &e) | CVCL::TheoryCore | [private] |
| assertTypePred(const Expr &e, const Theorem &pred) | CVCL::Theory | [inline, virtual] |
| assignValue(const Expr &t, const Expr &val) | CVCL::TheoryCore | [virtual] |
| assignValue(const Theorem &thm) | CVCL::TheoryCore | [virtual] |
| boolType() | CVCL::Theory | [inline] |
| buildModel(ExprMap< Expr > &m) | CVCL::TheoryCore | |
| checkSat(bool fullEffort) | CVCL::TheoryCore | [virtual] |
| checkSATCore() | CVCL::TheoryCore | |
| checkType(const Expr &e) | CVCL::TheoryCore | [virtual] |
| collectBasicVars() | CVCL::TheoryCore | |
| collectModelValues(const Expr &e, ExprMap< Expr > &m) | CVCL::TheoryCore | |
| computeBaseType(const Type &t) | CVCL::TheoryCore | [virtual] |
| computeModel(const Expr &e, std::vector< Expr > &vars) | CVCL::Theory | [inline, virtual] |
| computeModelBasic(const std::vector< Expr > &v) | CVCL::TheoryCore | [virtual] |
| computeModelTerm(const Expr &e, std::vector< Expr > &v) | CVCL::Theory | [virtual] |
| computeTCC(const Expr &e) | CVCL::TheoryCore | [virtual] |
| computeType(const Expr &e) | CVCL::TheoryCore | [virtual] |
| computeTypePred(const Type &t, const Expr &e) | CVCL::TheoryCore | [virtual] |
| CoreNotifyObj class | CVCL::TheoryCore | [friend] |
| createProofRules(TheoremManager *tm) | CVCL::TheoryCore | [private] |
| d_basicModelVars | CVCL::TheoryCore | [private] |
| d_boundVarStack | CVCL::TheoryCore | [private] |
| d_cm | CVCL::TheoryCore | [private] |
| d_cnfOption | CVCL::TheoryCore | [private] |
| d_coreSatAPI | CVCL::TheoryCore | [private] |
| d_currentRecursiveSimplifier | CVCL::TheoryCore | [private] |
| d_diseq | CVCL::TheoryCore | [private] |
| d_equalityQueue | CVCL::TheoryCore | [private] |
| d_equivCheckMMidx | CVCL::TheoryCore | [private] |
| d_exprTrans | CVCL::TheoryCore | [private] |
| d_flags | CVCL::TheoryCore | [private] |
| d_globals | CVCL::TheoryCore | [private] |
| d_impliedLiterals | CVCL::TheoryCore | [private] |
| d_impliedLiteralsIdx | CVCL::TheoryCore | [private] |
| d_incomplete | CVCL::TheoryCore | [private] |
| d_inconsistent | CVCL::TheoryCore | [private] |
| d_incThm | CVCL::TheoryCore | [private] |
| d_notifyObj | CVCL::TheoryCore | [private] |
| d_printer | CVCL::TheoryCore | [private] |
| d_queue | CVCL::TheoryCore | [private] |
| d_queueSE | CVCL::TheoryCore | [private] |
| d_resourceLimit | CVCL::TheoryCore | [private] |
| d_rules | CVCL::TheoryCore | [private] |
| d_sharedTerms | CVCL::TheoryCore | [private] |
| d_simplifiedModelVars | CVCL::TheoryCore | [private] |
| d_simplifyInPlace | CVCL::TheoryCore | [private] |
| d_solver | CVCL::TheoryCore | [private] |
| d_statistics | CVCL::TheoryCore | [private] |
| d_terms | CVCL::TheoryCore | [private] |
| d_theories | CVCL::TheoryCore | [private] |
| d_theoryMap | CVCL::TheoryCore | [private] |
| d_theoryUsed | CVCL::Theory | [protected] |
| d_tm | CVCL::TheoryCore | [private] |
| d_typeComputer | CVCL::TheoryCore | [private] |
| d_typePredAsserted | CVCL::TheoryCore | [private] |
| d_update_data | CVCL::TheoryCore | [private] |
| d_update_thms | CVCL::TheoryCore | [private] |
| d_varAssignments | CVCL::TheoryCore | [private] |
| d_varModelMap | CVCL::TheoryCore | [private] |
| d_vars | CVCL::TheoryCore | [private] |
| enqueueEquality(const Theorem &e) | CVCL::TheoryCore | [private, virtual] |
| enqueueFact(const Theorem &e) | CVCL::TheoryCore | [virtual] |
| enqueueSE(const Theorem &thm) | CVCL::TheoryCore | [private] |
| falseExpr() | CVCL::Theory | [inline] |
| find(const Expr &e) | CVCL::Theory | |
| findExpr(const Expr &e) | CVCL::Theory | [inline] |
| getBaseType(const Expr &e) | CVCL::Theory | |
| getBaseType(const Type &tp) | CVCL::Theory | |
| getCM() const | CVCL::TheoryCore | [inline] |
| getCommonRules() | CVCL::Theory | [inline] |
| getCoreRules() const | CVCL::TheoryCore | [inline] |
| getE0(const Expr &e) | CVCL::TheoryCore | |
| getE1(const Expr &e) | CVCL::TheoryCore | |
| getEM() | CVCL::Theory | [inline] |
| getExprTrans() const | CVCL::TheoryCore | [inline] |
| getFlags() const | CVCL::TheoryCore | [inline] |
| getImpliedLiteral(void) | CVCL::TheoryCore | |
| getImpliedLiteralByIndex(unsigned index) | CVCL::TheoryCore | |
| getModelTerm(const Expr &e, std::vector< Expr > &v) | CVCL::Theory | |
| getModelValue(const Expr &e) | CVCL::TheoryCore | [private] |
| getName() const | CVCL::Theory | [inline] |
| getNumTheories() | CVCL::Theory | |
| getResource() | CVCL::TheoryCore | [private] |
| getStatistics() const | CVCL::TheoryCore | [inline] |
| getTCC(const Expr &e) | CVCL::Theory | |
| getTerms() | CVCL::TheoryCore | [inline] |
| getTM() const | CVCL::TheoryCore | [inline] |
| getTypePred(const Type &t, const Expr &e) | CVCL::Theory | |
| hasTheory(int kind) | CVCL::Theory | |
| IF_DEBUG(const std::string *d_dumpTrace) | CVCL::TheoryCore | [private] |
| IF_DEBUG(bool d_inCheckSATCore) | CVCL::TheoryCore | [private] |
| IF_DEBUG(bool d_inAddFact) | CVCL::TheoryCore | [private] |
| IF_DEBUG(bool d_inSimplify) | CVCL::TheoryCore | [private] |
| IF_DEBUG(bool d_inRegisterAtom) | CVCL::TheoryCore | [private] |
| IF_DEBUG(void dumpTrace(const Expr &fact, const std::string &title);) void setFindLiteral(const Theorem &thm | CVCL::TheoryCore | [private] |
| iffMP(const Theorem &e1, const Theorem &e1_iff_e2) | CVCL::Theory | [inline] |
| implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs) | CVCL::TheoryCore | |
| incomplete() | CVCL::TheoryCore | [inline] |
| incomplete(std::vector< std::string > &reasons) | CVCL::TheoryCore | |
| inconsistent() | CVCL::TheoryCore | [inline, virtual] |
| inconsistentThm() | CVCL::TheoryCore | [inline] |
| installID(const std::string &name, const Expr &e) | CVCL::Theory | |
| isEquivCheckExpr(const Expr &e) | CVCL::TheoryCore | |
| 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 | |
| newEquivCkExpr(const Expr &e0, const Expr &e1) | CVCL::TheoryCore | [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::Theory | [inline, virtual] |
| notifySAT | CVCL::TheoryCore | [private] |
| numImpliedLiterals() | CVCL::TheoryCore | [inline] |
| parseExpr(const Expr &e) | CVCL::TheoryCore | [virtual] |
| parseExprOp(const Expr &e) | CVCL::TheoryCore | [virtual] |
| parseExprTop(const Expr &e) | CVCL::TheoryCore | [inline] |
| print(ExprStream &os, const Expr &e) | CVCL::TheoryCore | [virtual] |
| processCond(const Expr &e, int i) | CVCL::TheoryCore | [private] |
| processEquality(const Theorem &thm, ExprMap< Theorem > &q) | CVCL::TheoryCore | [private] |
| processFactQueue() | CVCL::TheoryCore | [private] |
| processNotify(const Theorem &e, NotifyList *L) | CVCL::TheoryCore | [private] |
| processUpdates() | CVCL::TheoryCore | [private] |
| queryTCC(const Theorem &phi, const Theorem &D_phi) | CVCL::TheoryCore | |
| refineCounterExample() | CVCL::TheoryCore | [virtual] |
| reflexivityRule(const Expr &a) | CVCL::Theory | [inline] |
| registerAtom(const Expr &e) | CVCL::TheoryCore | |
| registerCoreSatAPI(CoreSatAPI *coreSatAPI) | CVCL::TheoryCore | [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::TheoryCore | [virtual] |
| rewriteAnd(const Expr &e) | CVCL::Theory | [inline] |
| rewriteAtomic(const Expr &e) | CVCL::Theory | [inline, virtual] |
| rewriteCC(const Expr &e) | CVCL::Theory | |
| rewriteCore(const Theorem &e) | CVCL::TheoryCore | [private] |
| rewriteCore(const Expr &e) | CVCL::TheoryCore | [private] |
| rewriteIte(const Expr &e) | CVCL::TheoryCore | [private] |
| rewriteLitCore(const Expr &e) | CVCL::TheoryCore | [private] |
| rewriteLiteral(const Expr &e) | CVCL::TheoryCore | |
| rewriteN(const Expr &e, int n) | CVCL::TheoryCore | [private] |
| rewriteOr(const Expr &e) | CVCL::Theory | [inline] |
| setIncomplete(const std::string &reason) | CVCL::TheoryCore | [private, virtual] |
| setInconsistent(const Theorem &e) | CVCL::TheoryCore | [virtual] |
| setResourceLimit(unsigned limit) | CVCL::TheoryCore | |
| setup(const Expr &e) | CVCL::TheoryCore | [virtual] |
| setupCC(const Expr &e) | CVCL::Theory | |
| setupSubFormulas(const Expr &s, const Expr &e) | CVCL::TheoryCore | [private] |
| setupTerm(const Expr &e, Theory *i) | CVCL::TheoryCore | |
| simplify(const Expr &e, bool forceRebuild=true) | CVCL::TheoryCore | [virtual] |
| simplifyExpr(const Expr &e, bool forceRebuild=true) | CVCL::Theory | [inline] |
| simplifyFullRec(const Expr &e) | CVCL::TheoryCore | [private] |
| simplifyInPlaceRec(const Expr &e) | CVCL::TheoryCore | [private] |
| simplifyOp(const Expr &e) | CVCL::TheoryCore | [virtual] |
| simplifyRec(const Expr &e) | CVCL::TheoryCore | [private, virtual] |
| solve(const Theorem &e) | CVCL::TheoryCore | [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::TheoryCore | |
| symmetryRule(const Theorem &a1_eq_a2) | CVCL::Theory | [inline] |
| Theory class | CVCL::TheoryCore | [friend] |
| CVCL::Theory::Theory(TheoryCore *theoryCore, const std::string &name) | CVCL::Theory | |
| TheoryCore(ContextManager *cm, ExprManager *em, TheoremManager *tm, const CLFlags &flags, Statistics &statistics) | CVCL::TheoryCore | |
| theoryCore() | CVCL::Theory | [inline] |
| theoryOf(int kind) | CVCL::Theory | |
| theoryOf(const Expr &e) | CVCL::Theory | |
| theoryUsed() | CVCL::Theory | [inline, virtual] |
| transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) | CVCL::Theory | [inline] |
| trueExpr() | CVCL::Theory | [inline] |
| typePred(const Expr &e) | CVCL::TheoryCore | |
| update(const Theorem &e, const Expr &d) | CVCL::TheoryCore | [virtual] |
| updateCC(const Theorem &e, const Expr &d) | CVCL::Theory | |
| updateHelper(const Expr &e) | CVCL::Theory | |
| ~Theory(void) | CVCL::Theory | [virtual] |
| ~TheoryCore() | CVCL::TheoryCore | |
