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