| addCNFFact(const Theorem &thm, bool fromCore=false) | CVCL::SearchImplBase | [protected] |
| addFact(const Theorem &thm) | CVCL::SearchImplBase | |
| addLiteralFact(const Theorem &thm) | CVCL::SearchEngineFast | [virtual] |
| addNewClause(Clause &c) | CVCL::SearchEngineFast | [private] |
| addNonLiteralFact(const Theorem &thm) | CVCL::SearchEngineFast | [virtual] |
| addSplitter(const Expr &e, int priority) | CVCL::SearchEngineFast | [virtual] |
| analyzeUIPs(const Theorem &falseThm, int conflictScope) | CVCL::SearchEngineFast | [private] |
| assertAssumptions() | CVCL::SearchEngineFast | [private] |
| bcp() | CVCL::SearchEngineFast | [private] |
| checkSAT() | CVCL::SearchEngineFast | [private] |
| checkValid(const Expr &e) | CVCL::SearchImplBase | [virtual] |
| checkValidInternal(const Expr &e) | CVCL::SearchEngineFast | [virtual] |
| checkValidMain(const Expr &e2) | CVCL::SearchEngineFast | [private] |
| Circuit class | CVCL::SearchEngineFast | [friend] |
| clearFacts() | CVCL::SearchEngineFast | [private] |
| clearLiterals() | CVCL::SearchEngineFast | [private] |
| commitFacts() | CVCL::SearchEngineFast | [private] |
| ConflictClauseManager class | CVCL::SearchEngineFast | [friend] |
| createRules() | CVCL::SearchEngine | [protected] |
| d_applyCNFRulesCache | CVCL::SearchImplBase | [protected] |
| d_assumptions | CVCL::SearchImplBase | [protected] |
| d_berkminFlag | CVCL::SearchEngineFast | [private] |
| d_bottomScope | CVCL::SearchImplBase | [protected] |
| d_circuitPropCount | CVCL::SearchEngineFast | [private] |
| d_circuits | CVCL::SearchEngineFast | [private] |
| d_circuitsByExpr | CVCL::SearchEngineFast | [private] |
| d_clauses | CVCL::SearchEngineFast | [private] |
| d_clausesQueryEnd | CVCL::SearchEngineFast | [private] |
| d_clausesQueryStart | CVCL::SearchEngineFast | [private] |
| d_cnfCache | CVCL::SearchImplBase | [protected] |
| d_cnfOption | CVCL::SearchImplBase | [protected] |
| d_cnfVars | CVCL::SearchImplBase | [protected] |
| d_commonRules | CVCL::SearchEngine | [protected] |
| d_conflictClauseCount | CVCL::SearchEngineFast | [private] |
| d_conflictClauseManager | CVCL::SearchEngineFast | [private] |
| d_conflictClauses | CVCL::SearchEngineFast | [private] |
| d_conflictClauseStack | CVCL::SearchEngineFast | [private] |
| d_conflictCount | CVCL::SearchEngineFast | [private] |
| d_conflictTheorem | CVCL::SearchEngineFast | [private] |
| d_core | CVCL::SearchEngine | [protected] |
| d_coreSatAPI_implBase | CVCL::SearchImplBase | [protected] |
| d_decisionEngine | CVCL::SearchEngineFast | [private] |
| d_dpSplitters | CVCL::SearchImplBase | [protected] |
| d_enqueueCNFCache | CVCL::SearchImplBase | [protected] |
| d_factQueue | CVCL::SearchEngineFast | [private] |
| d_ifLiftOption | CVCL::SearchImplBase | [protected] |
| d_ignoreCnfVarsOption | CVCL::SearchImplBase | [protected] |
| d_inCheckSAT | CVCL::SearchEngineFast | [private] |
| d_lastConflictClause | CVCL::SearchEngineFast | [private] |
| d_lastConflictScope | CVCL::SearchEngineFast | [private] |
| d_lastCounterExample | CVCL::SearchImplBase | [protected] |
| d_lastValid | CVCL::SearchImplBase | [protected] |
| d_literals | CVCL::SearchEngineFast | [private] |
| d_literalSet | CVCL::SearchEngineFast | [private] |
| d_litsAlive | CVCL::SearchEngineFast | [private] |
| d_litsByScores | CVCL::SearchEngineFast | [private] |
| d_litsMaxScorePos | CVCL::SearchEngineFast | [private] |
| d_litSortCount | CVCL::SearchEngineFast | [private] |
| d_name | CVCL::SearchEngineFast | [private] |
| d_nonLiterals | CVCL::SearchEngineFast | [private] |
| d_nonLiteralsSaved | CVCL::SearchEngineFast | [private] |
| d_nonlitQueryEnd | CVCL::SearchEngineFast | [private] |
| d_nonlitQueryStart | CVCL::SearchEngineFast | [private] |
| d_origFormulaOption | CVCL::SearchImplBase | [protected] |
| d_replaceITECache | CVCL::SearchImplBase | [protected] |
| d_rules | CVCL::SearchEngine | [protected] |
| d_simplifiedThm | CVCL::SearchEngineFast | [private] |
| d_splitterCount | CVCL::SearchEngineFast | [private] |
| d_unitConflictClauses | CVCL::SearchEngineFast | [private] |
| d_unitPropCount | CVCL::SearchEngineFast | [private] |
| d_unreportedLits | CVCL::SearchEngineFast | [private] |
| d_unreportedLitsHandled | CVCL::SearchEngineFast | [private] |
| d_useEnqueueFact | CVCL::SearchEngineFast | [private] |
| d_vm | CVCL::SearchImplBase | [protected] |
| enqueueFact(const Theorem &thm) | CVCL::SearchEngineFast | [private] |
| findSplitter() | CVCL::SearchEngineFast | [private] |
| fixConflict() | CVCL::SearchEngineFast | [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) | CVCL::SearchEngineFast | [virtual] |
| CVCL::SearchImplBase::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() | CVCL::SearchEngineFast | [inline, virtual] |
| getProof() | CVCL::SearchImplBase | [virtual] |
| getUserAssumptions(std::vector< Expr > &assumptions) | CVCL::SearchImplBase | [virtual] |
| IF_DEBUG(void fullCheck()) | CVCL::SearchEngineFast | [private] |
| isAssumption(const Expr &e) | CVCL::SearchEngineFast | [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::SearchEngineFast | [virtual] |
| CVCL::SearchImplBase::newIntAssumption(const Theorem &thm) | CVCL::SearchImplBase | |
| newLiteral(const Expr &e) | CVCL::SearchImplBase | [inline, protected] |
| newUserAssumption(const Expr &e, int scope=-1) | CVCL::SearchImplBase | [virtual] |
| processConflict(const Literal &l) | CVCL::SearchEngineFast | [private] |
| processConflict(const Theorem &thm) | CVCL::SearchEngineFast | [private] |
| processResult(const Theorem &res, const Expr &e) | CVCL::SearchImplBase | |
| propagate(const Clause &c, int idx, bool &wpUpdated) | CVCL::SearchEngineFast | [private] |
| recordFact(const Theorem &thm) | CVCL::SearchEngineFast | [private] |
| registerAtom(const Expr &e) | CVCL::SearchImplBase | [inline, virtual] |
| restart(const Expr &e) | CVCL::SearchImplBase | [virtual] |
| restartInternal(const Expr &e) | CVCL::SearchEngineFast | [virtual] |
| returnFromCheck() | CVCL::SearchImplBase | [inline, virtual] |
| scopeLevel() | CVCL::SearchImplBase | [inline, protected] |
| SearchEngine(TheoryCore *core) | CVCL::SearchEngine | |
| SearchEngineFast(TheoryCore *core) | CVCL::SearchEngineFast | |
| SearchImplBase(TheoryCore *core) | CVCL::SearchImplBase | |
| setInconsistent(const Theorem &thm) | CVCL::SearchEngineFast | [private] |
| simplify(const Theorem &e) | CVCL::SearchImplBase | [inline, protected] |
| split() | CVCL::SearchEngineFast | [private] |
| theoryCore() | CVCL::SearchEngine | [inline] |
| traceConflict(const Theorem &conflictThm) | CVCL::SearchEngineFast | [private] |
| unitPropagation(const Clause &c, unsigned idx) | CVCL::SearchEngineFast | [private] |
| updateLitCounts(const Clause &c) | CVCL::SearchEngineFast | [private] |
| updateLitScores(bool firstTime) | CVCL::SearchEngineFast | [private] |
| wp(const Literal &literal) | CVCL::SearchEngineFast | [private] |
| ~SearchEngine() | CVCL::SearchEngine | [virtual] |
| ~SearchEngineFast() | CVCL::SearchEngineFast | [virtual] |
| ~SearchImplBase() | CVCL::SearchImplBase | [virtual] |
