addLemma(const Theorem &thm, int priority=0, bool atBotomScope=false) | CVC3::SearchSat | private |
addSplitter(const Expr &e, int priority) | CVC3::SearchSat | private |
assertLit(SAT::Lit l) | CVC3::SearchSat | private |
check(const Expr &e, Theorem &result, bool isRestart=false) | CVC3::SearchSat | private |
checkConsistent(SAT::CNF_Formula &cnf, bool fullEffort) | CVC3::SearchSat | private |
checkJustified(SAT::Var v) | CVC3::SearchSat | inlineprivate |
checkValid(const Expr &e, Theorem &result) | CVC3::SearchSat | inlinevirtual |
createRules() | CVC3::SearchEngine | protected |
createRules(SearchEngine *s_eng) | CVC3::SearchEngine | protected |
d_bottomScope | CVC3::SearchSat | private |
d_cnfCallback | CVC3::SearchSat | private |
d_cnfManager | CVC3::SearchSat | private |
d_commonRules | CVC3::SearchEngine | protected |
d_core | CVC3::SearchEngine | protected |
d_coreSatAPI | CVC3::SearchSat | private |
d_decider | CVC3::SearchSat | private |
d_dpllt | CVC3::SearchSat | private |
d_dplltReady | CVC3::SearchSat | private |
d_idxUserAssump | CVC3::SearchSat | private |
d_inCheckSat | CVC3::SearchSat | private |
d_intAssumptions | CVC3::SearchSat | private |
d_lastCheck | CVC3::SearchSat | private |
d_lastRegisteredVar | CVC3::SearchSat | private |
d_lastValid | CVC3::SearchSat | private |
d_lemmas | CVC3::SearchSat | private |
d_lemmasNext | CVC3::SearchSat | private |
d_name | CVC3::SearchSat | private |
d_nextImpliedLiteral | CVC3::SearchSat | private |
d_pendingLemmas | CVC3::SearchSat | private |
d_pendingLemmasNext | CVC3::SearchSat | private |
d_pendingLemmasSize | CVC3::SearchSat | private |
d_pendingScopes | CVC3::SearchSat | private |
d_prioritySet | CVC3::SearchSat | private |
d_prioritySetBottomEntries | CVC3::SearchSat | private |
d_prioritySetBottomEntriesSize | CVC3::SearchSat | private |
d_prioritySetBottomEntriesSizeStack | CVC3::SearchSat | private |
d_prioritySetEntries | CVC3::SearchSat | private |
d_prioritySetEntriesSize | CVC3::SearchSat | private |
d_prioritySetStart | CVC3::SearchSat | private |
d_restorer | CVC3::SearchSat | private |
d_rules | CVC3::SearchEngine | protected |
d_theorems | CVC3::SearchSat | private |
d_theoryAPI | CVC3::SearchSat | private |
d_userAssumptions | CVC3::SearchSat | private |
d_vars | CVC3::SearchSat | private |
d_varsUndoList | CVC3::SearchSat | private |
d_varsUndoListSize | CVC3::SearchSat | private |
findSplitterRec(SAT::Lit lit, SAT::Var::Val value, SAT::Lit *litDecision) | CVC3::SearchSat | private |
getAssumptions(std::vector< Expr > &assumptions) | CVC3::SearchSat | virtual |
getBottomScope() | CVC3::SearchSat | inlineprivate |
getCommonRules() | CVC3::SearchEngine | inline |
getConcreteModel(ExprMap< Expr > &m) | CVC3::SearchEngine | |
getCounterExample(std::vector< Expr > &assertions, bool inOrder=true) | CVC3::SearchSat | virtual |
getExplanation(SAT::Lit l, SAT::CNF_Formula &cnf) | CVC3::SearchSat | private |
getImplication() | CVC3::SearchSat | private |
getImpliedLiteral() | CVC3::SearchSat | virtual |
getInternalAssumptions(std::vector< Expr > &assumptions) | CVC3::SearchSat | virtual |
getName() | CVC3::SearchSat | inlinevirtual |
getNewClauses(SAT::CNF_Formula &cnf) | CVC3::SearchSat | private |
getProof() | CVC3::SearchSat | virtual |
getUserAssumptions(std::vector< Expr > &assumptions) | CVC3::SearchSat | virtual |
getValue(SAT::Lit c) | CVC3::SearchSat | inlineprivate |
getValue(SAT::Var v) | CVC3::SearchSat | inlineprivate |
getValue(const CVC3::Expr &e) | CVC3::SearchSat | inlinevirtual |
isAssumption(const Expr &e) | CVC3::SearchSat | virtual |
lastThm() | CVC3::SearchSat | inlinevirtual |
makeDecision() | CVC3::SearchSat | private |
newUserAssumption(const Expr &e) | CVC3::SearchSat | virtual |
newUserAssumptionInt(const Expr &e, SAT::CNF_Formula_Impl &cnf, bool atBottomScope) | CVC3::SearchSat | private |
newUserAssumptionIntHelper(const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope) | CVC3::SearchSat | private |
pop() | CVC3::SearchSat | inlinevirtual |
push() | CVC3::SearchSat | inlinevirtual |
recordNewRootLit(SAT::Lit lit, int priority=0, bool atBottomScope=false) | CVC3::SearchSat | private |
registerAtom(const Expr &e) | CVC3::SearchSat | virtual |
restart(const Expr &e, Theorem &result) | CVC3::SearchSat | inlinevirtual |
restore() | CVC3::SearchSat | private |
restorePre() | CVC3::SearchSat | private |
Restorer class | CVC3::SearchSat | friend |
returnFromCheck() | CVC3::SearchSat | virtual |
SearchEngine(TheoryCore *core) | CVC3::SearchEngine | |
SearchSat(TheoryCore *core, const std::string &name) | CVC3::SearchSat | |
SearchSatCNFCallback class | CVC3::SearchSat | friend |
SearchSatCoreSatAPI class | CVC3::SearchSat | friend |
SearchSatDecider class | CVC3::SearchSat | friend |
SearchSatTheoryAPI class | CVC3::SearchSat | friend |
setJustified(SAT::Var v) | CVC3::SearchSat | inlineprivate |
setValue(SAT::Var v, SAT::Var::Val val) | CVC3::SearchSat | inlineprivate |
theoryCore() | CVC3::SearchEngine | inline |
tryModelGeneration(Theorem &thm) | CVC3::SearchEngine | |
~SearchEngine() | CVC3::SearchEngine | virtual |
~SearchSat() | CVC3::SearchSat | virtual |