CVC3::SearchEngineFast Member List

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

addCNFFact(const Theorem &thm, bool fromCore=false)CVC3::SearchImplBase [protected]
addFact(const Theorem &thm)CVC3::SearchImplBase
addLiteralFact(const Theorem &thm)CVC3::SearchEngineFast [virtual]
addNewClause(Clause &c)CVC3::SearchEngineFast [private]
addNonLiteralFact(const Theorem &thm)CVC3::SearchEngineFast [virtual]
addSplitter(const Expr &e, int priority)CVC3::SearchEngineFast [virtual]
analyzeUIPs(const Theorem &falseThm, int conflictScope)CVC3::SearchEngineFast [private]
assertAssumptions()CVC3::SearchEngineFast [private]
bcp()CVC3::SearchEngineFast [private]
checkSAT()CVC3::SearchEngineFast [private]
checkValid(const Expr &e, Theorem &result)CVC3::SearchImplBase [virtual]
checkValidInternal(const Expr &e)CVC3::SearchEngineFast [virtual]
checkValidMain(const Expr &e2)CVC3::SearchEngineFast [private]
Circuit classCVC3::SearchEngineFast [friend]
clearFacts()CVC3::SearchEngineFast [private]
clearLiterals()CVC3::SearchEngineFast [private]
commitFacts()CVC3::SearchEngineFast [private]
ConflictClauseManager classCVC3::SearchEngineFast [friend]
createRules()CVC3::SearchEngine [protected]
d_applyCNFRulesCacheCVC3::SearchImplBase [protected]
d_assumptionsCVC3::SearchImplBase [protected]
d_berkminFlagCVC3::SearchEngineFast [private]
d_bottomScopeCVC3::SearchImplBase [protected]
d_circuitPropCountCVC3::SearchEngineFast [private]
d_circuitsCVC3::SearchEngineFast [private]
d_circuitsByExprCVC3::SearchEngineFast [private]
d_clausesCVC3::SearchEngineFast [private]
d_clausesQueryEndCVC3::SearchEngineFast [private]
d_clausesQueryStartCVC3::SearchEngineFast [private]
d_cnfCacheCVC3::SearchImplBase [protected]
d_cnfOptionCVC3::SearchImplBase [protected]
d_cnfVarsCVC3::SearchImplBase [protected]
d_commonRulesCVC3::SearchEngine [protected]
d_conflictClauseCountCVC3::SearchEngineFast [private]
d_conflictClauseManagerCVC3::SearchEngineFast [private]
d_conflictClausesCVC3::SearchEngineFast [private]
d_conflictClauseStackCVC3::SearchEngineFast [private]
d_conflictCountCVC3::SearchEngineFast [private]
d_conflictTheoremCVC3::SearchEngineFast [private]
d_coreCVC3::SearchEngine [protected]
d_coreSatAPI_implBaseCVC3::SearchImplBase [protected]
d_decisionEngineCVC3::SearchEngineFast [private]
d_dpSplittersCVC3::SearchImplBase [protected]
d_enqueueCNFCacheCVC3::SearchImplBase [protected]
d_factQueueCVC3::SearchEngineFast [private]
d_ifLiftOptionCVC3::SearchImplBase [protected]
d_ignoreCnfVarsOptionCVC3::SearchImplBase [protected]
d_inCheckSATCVC3::SearchEngineFast [private]
d_lastConflictClauseCVC3::SearchEngineFast [private]
d_lastConflictScopeCVC3::SearchEngineFast [private]
d_lastCounterExampleCVC3::SearchImplBase [protected]
d_lastValidCVC3::SearchImplBase [protected]
d_literalsCVC3::SearchEngineFast [private]
d_literalSetCVC3::SearchEngineFast [private]
d_litsAliveCVC3::SearchEngineFast [private]
d_litsByScoresCVC3::SearchEngineFast [private]
d_litsMaxScorePosCVC3::SearchEngineFast [private]
d_litSortCountCVC3::SearchEngineFast [private]
d_nameCVC3::SearchEngineFast [private]
d_nonLiteralsCVC3::SearchEngineFast [private]
d_nonLiteralsSavedCVC3::SearchEngineFast [private]
d_nonlitQueryEndCVC3::SearchEngineFast [private]
d_nonlitQueryStartCVC3::SearchEngineFast [private]
d_origFormulaOptionCVC3::SearchImplBase [protected]
d_replaceITECacheCVC3::SearchImplBase [protected]
d_rulesCVC3::SearchEngine [protected]
d_simplifiedThmCVC3::SearchEngineFast [private]
d_splitterCountCVC3::SearchEngineFast [private]
d_unitConflictClausesCVC3::SearchEngineFast [private]
d_unitPropCountCVC3::SearchEngineFast [private]
d_unreportedLitsCVC3::SearchEngineFast [private]
d_unreportedLitsHandledCVC3::SearchEngineFast [private]
d_useEnqueueFactCVC3::SearchEngineFast [private]
d_vmCVC3::SearchImplBase [protected]
enqueueFact(const Theorem &thm)CVC3::SearchEngineFast [private]
findSplitter()CVC3::SearchEngineFast [private]
fixConflict()CVC3::SearchEngineFast [private]
getAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBase [virtual]
getAssumptionsUsed()CVC3::SearchImplBase [virtual]
getBottomScope()CVC3::SearchImplBase [inline]
getCommonRules()CVC3::SearchEngine [inline]
getConcreteModel(ExprMap< Expr > &m)CVC3::SearchEngine
getCounterExample(std::vector< Expr > &assertions)CVC3::SearchEngineFast [virtual]
CVC3::SearchImplBase::getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)CVC3::SearchImplBase [virtual]
getImpliedLiteral()CVC3::SearchImplBase [inline, virtual]
getInternalAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBase [virtual]
getName()CVC3::SearchEngineFast [inline, virtual]
getProof()CVC3::SearchImplBase [virtual]
getUserAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBase [virtual]
getValue(const CVC3::Expr &e)CVC3::SearchImplBase [inline, virtual]
isAssumption(const Expr &e)CVC3::SearchEngineFast [virtual]
isClause(const Expr &e)CVC3::SearchImplBase
isCNFVar(const Expr &e)CVC3::SearchImplBase [inline]
isGoodSplitter(const Expr &e)CVC3::SearchImplBase
isPropClause(const Expr &e)CVC3::SearchImplBase
lastThm()CVC3::SearchImplBase [inline, virtual]
newIntAssumption(const Expr &e)CVC3::SearchEngineFast [virtual]
CVC3::SearchImplBase::newIntAssumption(const Theorem &thm)CVC3::SearchImplBase
newLiteral(const Expr &e)CVC3::SearchImplBase [inline, protected]
newUserAssumption(const Expr &e)CVC3::SearchImplBase [virtual]
pop()CVC3::SearchImplBase [inline, virtual]
processConflict(const Literal &l)CVC3::SearchEngineFast [private]
processConflict(const Theorem &thm)CVC3::SearchEngineFast [private]
processResult(const Theorem &res, const Expr &e)CVC3::SearchImplBase
propagate(const Clause &c, int idx, bool &wpUpdated)CVC3::SearchEngineFast [private]
push()CVC3::SearchImplBase [inline, virtual]
recordFact(const Theorem &thm)CVC3::SearchEngineFast [private]
registerAtom(const Expr &e)CVC3::SearchImplBase [inline, virtual]
restart(const Expr &e, Theorem &result)CVC3::SearchImplBase [virtual]
restartInternal(const Expr &e)CVC3::SearchEngineFast [virtual]
returnFromCheck()CVC3::SearchImplBase [inline, virtual]
scopeLevel()CVC3::SearchImplBase [inline, protected]
SearchEngine(TheoryCore *core)CVC3::SearchEngine
SearchEngineFast(TheoryCore *core)CVC3::SearchEngineFast
SearchImplBase(TheoryCore *core)CVC3::SearchImplBase
setInconsistent(const Theorem &thm)CVC3::SearchEngineFast [private]
simplify(const Theorem &e)CVC3::SearchImplBase [inline, protected]
split()CVC3::SearchEngineFast [private]
theoryCore()CVC3::SearchEngine [inline]
traceConflict(const Theorem &conflictThm)CVC3::SearchEngineFast [private]
tryModelGeneration(Theorem &thm)CVC3::SearchEngine
unitPropagation(const Clause &c, unsigned idx)CVC3::SearchEngineFast [private]
updateLitCounts(const Clause &c)CVC3::SearchEngineFast [private]
updateLitScores(bool firstTime)CVC3::SearchEngineFast [private]
wp(const Literal &literal)CVC3::SearchEngineFast [private]
~SearchEngine()CVC3::SearchEngine [virtual]
~SearchEngineFast()CVC3::SearchEngineFast [virtual]
~SearchImplBase()CVC3::SearchImplBase [virtual]

Generated on Thu Oct 15 22:19:56 2009 for CVC3 by  doxygen 1.5.8