CVC3::SearchImplBase Member List

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

addCNFFact(const Theorem &thm, bool fromCore=false)CVC3::SearchImplBase [protected]
addFact(const Theorem &thm)CVC3::SearchImplBase
addLiteralFact(const Theorem &thm)=0CVC3::SearchImplBase [protected, pure virtual]
addNonLiteralFact(const Theorem &thm)=0CVC3::SearchImplBase [protected, pure virtual]
addSplitter(const Expr &e, int priority)CVC3::SearchImplBase [virtual]
addToCNFCache(const Theorem &thm)CVC3::SearchImplBase [private]
applyCNFRules(const Theorem &e)CVC3::SearchImplBase [private]
checkValid(const Expr &e, Theorem &result)CVC3::SearchImplBase [virtual]
checkValidInternal(const Expr &e)=0CVC3::SearchImplBase [pure virtual]
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_dpSplittersCVC3::SearchImplBase [protected]
d_enqueueCNFCacheCVC3::SearchImplBase [protected]
d_ifLiftOptionCVC3::SearchImplBase [protected]
d_ignoreCnfVarsOptionCVC3::SearchImplBase [protected]
d_lastCounterExampleCVC3::SearchImplBase [protected]
d_lastValidCVC3::SearchImplBase [protected]
d_origFormulaOptionCVC3::SearchImplBase [protected]
d_replaceITECacheCVC3::SearchImplBase [protected]
d_rulesCVC3::SearchEngine [protected]
d_vmCVC3::SearchImplBase [protected]
DecisionEngine classCVC3::SearchImplBase [friend]
enqueueCNF(const Theorem &theta)CVC3::SearchImplBase [private]
enqueueCNFrec(const Theorem &theta)CVC3::SearchImplBase [private]
findInCNFCache(const Expr &e)CVC3::SearchImplBase [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, bool inOrder=true)CVC3::SearchImplBase [virtual]
getImpliedLiteral()CVC3::SearchImplBase [inline, virtual]
getInternalAssumptions(std::vector< Expr > &assumptions)CVC3::SearchImplBase [virtual]
getName()=0CVC3::SearchEngine [pure 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]
replaceITE(const Expr &e)CVC3::SearchImplBase [private]
restart(const Expr &e, Theorem &result)CVC3::SearchImplBase [virtual]
restartInternal(const Expr &e)=0CVC3::SearchImplBase [pure virtual]
returnFromCheck()CVC3::SearchImplBase [inline, virtual]
scopeLevel()CVC3::SearchImplBase [inline, protected]
SearchEngine(TheoryCore *core)CVC3::SearchEngine
SearchImplBase(TheoryCore *core)CVC3::SearchImplBase
simplify(const Theorem &e)CVC3::SearchImplBase [inline, protected]
theoryCore()CVC3::SearchEngine [inline]
~SearchEngine()CVC3::SearchEngine [virtual]
~SearchImplBase()CVC3::SearchImplBase [virtual]

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