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::SearchImplBase [protected]
addFact(const Theorem &thm)CVC3::SearchImplBase
addLiteralFact(const Theorem &thm)CVC3::SearchSimple [inline, virtual]
addNonLiteralFact(const Theorem &thm)CVC3::SearchSimple [virtual]
addSplitter(const Expr &e, int priority)CVC3::SearchImplBase [virtual]
checkValid(const Expr &e, Theorem &result)CVC3::SearchImplBase [virtual]
checkValidInternal(const Expr &e)CVC3::SearchSimple [virtual]
checkValidMain(const Expr &e2)CVC3::SearchSimple [private]
checkValidRec(Theorem &thm)CVC3::SearchSimple [private]
createRules()CVC3::SearchEngine [protected]
d_applyCNFRulesCacheCVC3::SearchImplBase [protected]
d_assumptionsCVC3::SearchImplBase [protected]
d_bottomScopeCVC3::SearchImplBase [protected]
d_cnfCacheCVC3::SearchImplBase [protected]
d_cnfOptionCVC3::SearchImplBase [protected]
d_cnfVarsCVC3::SearchImplBase [protected]
d_commonRulesCVC3::SearchEngine [protected]
d_coreCVC3::SearchEngine [protected]
d_coreSatAPI_implBaseCVC3::SearchImplBase [protected]
d_decisionEngineCVC3::SearchSimple [private]
d_dpSplittersCVC3::SearchImplBase [protected]
d_enqueueCNFCacheCVC3::SearchImplBase [protected]
d_goalCVC3::SearchSimple [private]
d_ifLiftOptionCVC3::SearchImplBase [protected]
d_ignoreCnfVarsOptionCVC3::SearchImplBase [protected]
d_lastCounterExampleCVC3::SearchImplBase [protected]
d_lastValidCVC3::SearchImplBase [protected]
d_nameCVC3::SearchSimple [private]
d_nonLiteralsCVC3::SearchSimple [private]
d_origFormulaOptionCVC3::SearchImplBase [protected]
d_replaceITECacheCVC3::SearchImplBase [protected]
d_rulesCVC3::SearchEngine [protected]
d_simplifiedThmCVC3::SearchSimple [private]
d_vmCVC3::SearchImplBase [protected]
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, bool inOrder=true)CVC3::SearchImplBase [virtual]
getImpliedLiteral()CVC3::SearchImplBase [inline, virtual]
getInternalAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBase [virtual]
getName()CVC3::SearchSimple [inline, virtual]
getProof()CVC3::SearchImplBase [virtual]
getUserAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBase [virtual]
isAssumption(const Expr &e)CVC3::SearchImplBase [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::SearchImplBase [virtual]
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]
processResult(const Theorem &res, const Expr &e)CVC3::SearchImplBase
push()CVC3::SearchImplBase [inline, virtual]
registerAtom(const Expr &e)CVC3::SearchImplBase [inline, virtual]
restart(const Expr &e, Theorem &result)CVC3::SearchImplBase [virtual]
restartInternal(const Expr &e)CVC3::SearchSimple [virtual]
returnFromCheck()CVC3::SearchImplBase [inline, virtual]
scopeLevel()CVC3::SearchImplBase [inline, protected]
SearchEngine(TheoryCore *core)CVC3::SearchEngine
SearchImplBase(TheoryCore *core)CVC3::SearchImplBase
SearchSimple(TheoryCore *core)CVC3::SearchSimple
simplify(const Theorem &e)CVC3::SearchImplBase [inline, protected]
theoryCore()CVC3::SearchEngine [inline]
~SearchEngine()CVC3::SearchEngine [virtual]
~SearchImplBase()CVC3::SearchImplBase [virtual]
~SearchSimple()CVC3::SearchSimple

Generated on Tue Jul 3 14:37:34 2007 for CVC3 by  doxygen 1.5.1