CVC3  2.4.1
CVC3::SearchSimple Member List

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

addCNFFact(const Theorem &thm, bool fromCore=false)CVC3::SearchImplBaseprotected
addFact(const Theorem &thm)CVC3::SearchImplBase
addLiteralFact(const Theorem &thm)CVC3::SearchSimpleinlinevirtual
addNonLiteralFact(const Theorem &thm)CVC3::SearchSimplevirtual
addSplitter(const Expr &e, int priority)CVC3::SearchImplBasevirtual
checkValid(const Expr &e, Theorem &result)CVC3::SearchImplBasevirtual
checkValidInternal(const Expr &e)CVC3::SearchSimplevirtual
checkValidMain(const Expr &e2)CVC3::SearchSimpleprivate
checkValidRec(Theorem &thm)CVC3::SearchSimpleprivate
createRules()CVC3::SearchEngineprotected
createRules(SearchEngine *s_eng)CVC3::SearchEngineprotected
d_applyCNFRulesCacheCVC3::SearchImplBaseprotected
d_assumptionsCVC3::SearchImplBaseprotected
d_bottomScopeCVC3::SearchImplBaseprotected
d_cnfCacheCVC3::SearchImplBaseprotected
d_cnfOptionCVC3::SearchImplBaseprotected
d_cnfVarsCVC3::SearchImplBaseprotected
d_commonRulesCVC3::SearchEngineprotected
d_coreCVC3::SearchEngineprotected
d_coreSatAPI_implBaseCVC3::SearchImplBaseprotected
d_decisionEngineCVC3::SearchSimpleprivate
d_dpSplittersCVC3::SearchImplBaseprotected
d_enqueueCNFCacheCVC3::SearchImplBaseprotected
d_goalCVC3::SearchSimpleprivate
d_ifLiftOptionCVC3::SearchImplBaseprotected
d_ignoreCnfVarsOptionCVC3::SearchImplBaseprotected
d_lastCounterExampleCVC3::SearchImplBaseprotected
d_lastValidCVC3::SearchImplBaseprotected
d_nameCVC3::SearchSimpleprivate
d_nonLiteralsCVC3::SearchSimpleprivate
d_origFormulaOptionCVC3::SearchImplBaseprotected
d_replaceITECacheCVC3::SearchImplBaseprotected
d_rulesCVC3::SearchEngineprotected
d_simplifiedThmCVC3::SearchSimpleprivate
d_vmCVC3::SearchImplBaseprotected
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, bool inOrder=true)CVC3::SearchImplBasevirtual
getImpliedLiteral()CVC3::SearchImplBaseinlinevirtual
getInternalAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBasevirtual
getName()CVC3::SearchSimpleinlinevirtual
getProof()CVC3::SearchImplBasevirtual
getUserAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBasevirtual
getValue(const CVC3::Expr &e)CVC3::SearchImplBaseinlinevirtual
isAssumption(const Expr &e)CVC3::SearchImplBasevirtual
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::SearchImplBasevirtual
newIntAssumption(const Theorem &thm)CVC3::SearchImplBase
newLiteral(const Expr &e)CVC3::SearchImplBaseinlineprotected
newUserAssumption(const Expr &e)CVC3::SearchImplBasevirtual
pop()CVC3::SearchImplBaseinlinevirtual
processResult(const Theorem &res, const Expr &e)CVC3::SearchImplBase
push()CVC3::SearchImplBaseinlinevirtual
registerAtom(const Expr &e)CVC3::SearchImplBaseinlinevirtual
restart(const Expr &e, Theorem &result)CVC3::SearchImplBasevirtual
restartInternal(const Expr &e)CVC3::SearchSimplevirtual
returnFromCheck()CVC3::SearchImplBaseinlinevirtual
scopeLevel()CVC3::SearchImplBaseinlineprotected
SearchEngine(TheoryCore *core)CVC3::SearchEngine
SearchImplBase(TheoryCore *core)CVC3::SearchImplBase
SearchSimple(TheoryCore *core)CVC3::SearchSimple
simplify(const Theorem &e)CVC3::SearchImplBaseinlineprotected
theoryCore()CVC3::SearchEngineinline
tryModelGeneration(Theorem &thm)CVC3::SearchEngine
~SearchEngine()CVC3::SearchEnginevirtual
~SearchImplBase()CVC3::SearchImplBasevirtual
~SearchSimple()CVC3::SearchSimple