CVC3::SearchSat Member List

This is the complete list of members for CVC3::SearchSat, including all inherited members.

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 [inline, private]
checkValid(const Expr &e, Theorem &result)CVC3::SearchSat [inline, virtual]
createRules()CVC3::SearchEngine [protected]
d_bottomScopeCVC3::SearchSat [private]
d_cnfCallbackCVC3::SearchSat [private]
d_cnfManagerCVC3::SearchSat [private]
d_commonRulesCVC3::SearchEngine [protected]
d_coreCVC3::SearchEngine [protected]
d_coreSatAPICVC3::SearchSat [private]
d_deciderCVC3::SearchSat [private]
d_dplltCVC3::SearchSat [private]
d_dplltReadyCVC3::SearchSat [private]
d_idxUserAssumpCVC3::SearchSat [private]
d_inCheckSatCVC3::SearchSat [private]
d_intAssumptionsCVC3::SearchSat [private]
d_lastCheckCVC3::SearchSat [private]
d_lastRegisteredVarCVC3::SearchSat [private]
d_lastValidCVC3::SearchSat [private]
d_lemmasCVC3::SearchSat [private]
d_lemmasNextCVC3::SearchSat [private]
d_nameCVC3::SearchSat [private]
d_nextImpliedLiteralCVC3::SearchSat [private]
d_pendingLemmasCVC3::SearchSat [private]
d_pendingLemmasNextCVC3::SearchSat [private]
d_pendingLemmasSizeCVC3::SearchSat [private]
d_pendingScopesCVC3::SearchSat [private]
d_prioritySetCVC3::SearchSat [private]
d_prioritySetBottomEntriesCVC3::SearchSat [private]
d_prioritySetBottomEntriesSizeCVC3::SearchSat [private]
d_prioritySetBottomEntriesSizeStackCVC3::SearchSat [private]
d_prioritySetEntriesCVC3::SearchSat [private]
d_prioritySetEntriesSizeCVC3::SearchSat [private]
d_prioritySetStartCVC3::SearchSat [private]
d_restorerCVC3::SearchSat [private]
d_rulesCVC3::SearchEngine [protected]
d_theoremsCVC3::SearchSat [private]
d_theoryAPICVC3::SearchSat [private]
d_userAssumptionsCVC3::SearchSat [private]
d_varsCVC3::SearchSat [private]
d_varsUndoListCVC3::SearchSat [private]
d_varsUndoListSizeCVC3::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 [inline, private]
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 [inline, virtual]
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 [inline, private]
getValue(SAT::Var v)CVC3::SearchSat [inline, private]
getValue(const CVC3::Expr &e)CVC3::SearchSat [inline, virtual]
isAssumption(const Expr &e)CVC3::SearchSat [virtual]
lastThm()CVC3::SearchSat [inline, virtual]
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 [inline, virtual]
push()CVC3::SearchSat [inline, virtual]
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 [inline, virtual]
restore()CVC3::SearchSat [private]
restorePre()CVC3::SearchSat [private]
Restorer classCVC3::SearchSat [friend]
returnFromCheck()CVC3::SearchSat [virtual]
SearchEngine(TheoryCore *core)CVC3::SearchEngine
SearchSat(TheoryCore *core, const std::string &name)CVC3::SearchSat
SearchSatCNFCallback classCVC3::SearchSat [friend]
SearchSatCoreSatAPI classCVC3::SearchSat [friend]
SearchSatDecider classCVC3::SearchSat [friend]
SearchSatTheoryAPI classCVC3::SearchSat [friend]
setJustified(SAT::Var v)CVC3::SearchSat [inline, private]
setValue(SAT::Var v, SAT::Var::Val val)CVC3::SearchSat [inline, private]
theoryCore()CVC3::SearchEngine [inline]
tryModelGeneration(Theorem &thm)CVC3::SearchEngine
~SearchEngine()CVC3::SearchEngine [virtual]
~SearchSat()CVC3::SearchSat [virtual]


Generated on Wed Nov 18 16:15:49 2009 for CVC3 by  doxygen 1.5.2