| addCNFFact(const Theorem &thm, bool fromCore=false) | CVCL::SearchImplBase | [protected] |
| addFact(const Theorem &thm) | CVCL::SearchImplBase | |
| addLiteralFact(const Theorem &thm)=0 | CVCL::SearchImplBase | [protected, pure virtual] |
| addNonLiteralFact(const Theorem &thm)=0 | CVCL::SearchImplBase | [protected, pure virtual] |
| addSplitter(const Expr &e, int priority) | CVCL::SearchImplBase | [virtual] |
| addToCNFCache(const Theorem &thm) | CVCL::SearchImplBase | [private] |
| applyCNFRules(const Theorem &e) | CVCL::SearchImplBase | [private] |
| checkValid(const Expr &e) | CVCL::SearchImplBase | [virtual] |
| checkValidInternal(const Expr &e)=0 | CVCL::SearchImplBase | [pure virtual] |
| createRules() | CVCL::SearchEngine | [protected] |
| d_applyCNFRulesCache | CVCL::SearchImplBase | [protected] |
| d_assumptions | CVCL::SearchImplBase | [protected] |
| d_bottomScope | CVCL::SearchImplBase | [protected] |
| d_cnfCache | CVCL::SearchImplBase | [protected] |
| d_cnfOption | CVCL::SearchImplBase | [protected] |
| d_cnfVars | CVCL::SearchImplBase | [protected] |
| d_commonRules | CVCL::SearchEngine | [protected] |
| d_core | CVCL::SearchEngine | [protected] |
| d_coreSatAPI_implBase | CVCL::SearchImplBase | [protected] |
| d_dpSplitters | CVCL::SearchImplBase | [protected] |
| d_enqueueCNFCache | CVCL::SearchImplBase | [protected] |
| d_ifLiftOption | CVCL::SearchImplBase | [protected] |
| d_ignoreCnfVarsOption | CVCL::SearchImplBase | [protected] |
| d_lastCounterExample | CVCL::SearchImplBase | [protected] |
| d_lastValid | CVCL::SearchImplBase | [protected] |
| d_origFormulaOption | CVCL::SearchImplBase | [protected] |
| d_replaceITECache | CVCL::SearchImplBase | [protected] |
| d_rules | CVCL::SearchEngine | [protected] |
| d_vm | CVCL::SearchImplBase | [protected] |
| DecisionEngine class | CVCL::SearchImplBase | [friend] |
| enqueueCNF(const Theorem &theta) | CVCL::SearchImplBase | [private] |
| enqueueCNFrec(const Theorem &theta) | CVCL::SearchImplBase | [private] |
| findInCNFCache(const Expr &e) | CVCL::SearchImplBase | [private] |
| getAssumptions(std::vector< Expr > &assumptions) | CVCL::SearchImplBase | [virtual] |
| getAssumptionsUsed() | CVCL::SearchImplBase | [virtual] |
| getBottomScope() | CVCL::SearchImplBase | [inline] |
| getConcreteModel(ExprMap< Expr > &m) | CVCL::SearchEngine | |
| getCounterExample(std::vector< Expr > &assertions, bool inOrder=true) | CVCL::SearchImplBase | [virtual] |
| getImpliedLiteral() | CVCL::SearchImplBase | [inline, virtual] |
| getInternalAssumptions(std::vector< Expr > &assumptions) | CVCL::SearchImplBase | [virtual] |
| getName()=0 | CVCL::SearchEngine | [pure virtual] |
| getProof() | CVCL::SearchImplBase | [virtual] |
| getUserAssumptions(std::vector< Expr > &assumptions) | CVCL::SearchImplBase | [virtual] |
| isAssumption(const Expr &e) | CVCL::SearchImplBase | [virtual] |
| isClause(const Expr &e) | CVCL::SearchImplBase | |
| isCNFVar(const Expr &e) | CVCL::SearchImplBase | [inline] |
| isGoodSplitter(const Expr &e) | CVCL::SearchImplBase | |
| isPropClause(const Expr &e) | CVCL::SearchImplBase | |
| lastThm() | CVCL::SearchImplBase | [inline, virtual] |
| newIntAssumption(const Expr &e) | CVCL::SearchImplBase | [virtual] |
| newIntAssumption(const Theorem &thm) | CVCL::SearchImplBase | |
| newLiteral(const Expr &e) | CVCL::SearchImplBase | [inline, protected] |
| newUserAssumption(const Expr &e, int scope=-1) | CVCL::SearchImplBase | [virtual] |
| processResult(const Theorem &res, const Expr &e) | CVCL::SearchImplBase | |
| registerAtom(const Expr &e) | CVCL::SearchImplBase | [inline, virtual] |
| replaceITE(const Expr &e) | CVCL::SearchImplBase | [private] |
| restart(const Expr &e) | CVCL::SearchImplBase | [virtual] |
| restartInternal(const Expr &e)=0 | CVCL::SearchImplBase | [pure virtual] |
| returnFromCheck() | CVCL::SearchImplBase | [inline, virtual] |
| scopeLevel() | CVCL::SearchImplBase | [inline, protected] |
| SearchEngine(TheoryCore *core) | CVCL::SearchEngine | |
| SearchImplBase(TheoryCore *core) | CVCL::SearchImplBase | |
| simplify(const Theorem &e) | CVCL::SearchImplBase | [inline, protected] |
| theoryCore() | CVCL::SearchEngine | [inline] |
| ~SearchEngine() | CVCL::SearchEngine | [virtual] |
| ~SearchImplBase() | CVCL::SearchImplBase | [virtual] |
