CVCL::SearchSimple Member List

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

addCNFFact(const Theorem &thm, bool fromCore=false)CVCL::SearchImplBase [protected]
addFact(const Theorem &thm)CVCL::SearchImplBase
addLiteralFact(const Theorem &thm)CVCL::SearchSimple [inline, virtual]
addNonLiteralFact(const Theorem &thm)CVCL::SearchSimple [virtual]
addSplitter(const Expr &e, int priority)CVCL::SearchImplBase [virtual]
checkValid(const Expr &e)CVCL::SearchImplBase [virtual]
checkValidInternal(const Expr &e)CVCL::SearchSimple [virtual]
checkValidMain(const Expr &e2)CVCL::SearchSimple [private]
checkValidRec()CVCL::SearchSimple [private]
createRules()CVCL::SearchEngine [protected]
d_applyCNFRulesCacheCVCL::SearchImplBase [protected]
d_assumptionsCVCL::SearchImplBase [protected]
d_bottomScopeCVCL::SearchImplBase [protected]
d_cnfCacheCVCL::SearchImplBase [protected]
d_cnfOptionCVCL::SearchImplBase [protected]
d_cnfVarsCVCL::SearchImplBase [protected]
d_commonRulesCVCL::SearchEngine [protected]
d_coreCVCL::SearchEngine [protected]
d_coreSatAPI_implBaseCVCL::SearchImplBase [protected]
d_decisionEngineCVCL::SearchSimple [private]
d_dpSplittersCVCL::SearchImplBase [protected]
d_enqueueCNFCacheCVCL::SearchImplBase [protected]
d_goalCVCL::SearchSimple [private]
d_ifLiftOptionCVCL::SearchImplBase [protected]
d_ignoreCnfVarsOptionCVCL::SearchImplBase [protected]
d_lastCounterExampleCVCL::SearchImplBase [protected]
d_lastValidCVCL::SearchImplBase [protected]
d_nameCVCL::SearchSimple [private]
d_nonLiteralsCVCL::SearchSimple [private]
d_origFormulaOptionCVCL::SearchImplBase [protected]
d_replaceITECacheCVCL::SearchImplBase [protected]
d_rulesCVCL::SearchEngine [protected]
d_simplifiedThmCVCL::SearchSimple [private]
d_vmCVCL::SearchImplBase [protected]
getAssumptions(std::vector< Expr > &assumptions)CVCL::SearchImplBase [virtual]
getAssumptionsUsed()CVCL::SearchImplBase [virtual]
getBottomScope()CVCL::SearchImplBase [inline]
getConcreteModel(ExprMap< Expr > &m)CVCL::SearchEngine
getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)CVCL::SearchImplBase [virtual]
getImpliedLiteral()CVCL::SearchImplBase [inline, virtual]
getInternalAssumptions(std::vector< Expr > &assumptions)CVCL::SearchImplBase [virtual]
getName()CVCL::SearchSimple [inline, virtual]
getProof()CVCL::SearchImplBase [virtual]
getUserAssumptions(std::vector< Expr > &assumptions)CVCL::SearchImplBase [virtual]
isAssumption(const Expr &e)CVCL::SearchImplBase [virtual]
isClause(const Expr &e)CVCL::SearchImplBase
isCNFVar(const Expr &e)CVCL::SearchImplBase [inline]
isGoodSplitter(const Expr &e)CVCL::SearchImplBase
isPropClause(const Expr &e)CVCL::SearchImplBase
lastThm()CVCL::SearchImplBase [inline, virtual]
newIntAssumption(const Expr &e)CVCL::SearchImplBase [virtual]
newIntAssumption(const Theorem &thm)CVCL::SearchImplBase
newLiteral(const Expr &e)CVCL::SearchImplBase [inline, protected]
newUserAssumption(const Expr &e, int scope=-1)CVCL::SearchImplBase [virtual]
processResult(const Theorem &res, const Expr &e)CVCL::SearchImplBase
registerAtom(const Expr &e)CVCL::SearchImplBase [inline, virtual]
restart(const Expr &e)CVCL::SearchImplBase [virtual]
restartInternal(const Expr &e)CVCL::SearchSimple [virtual]
returnFromCheck()CVCL::SearchImplBase [inline, virtual]
scopeLevel()CVCL::SearchImplBase [inline, protected]
SearchEngine(TheoryCore *core)CVCL::SearchEngine
SearchImplBase(TheoryCore *core)CVCL::SearchImplBase
SearchSimple(TheoryCore *core)CVCL::SearchSimple
simplify(const Theorem &e)CVCL::SearchImplBase [inline, protected]
theoryCore()CVCL::SearchEngine [inline]
~SearchEngine()CVCL::SearchEngine [virtual]
~SearchImplBase()CVCL::SearchImplBase [virtual]
~SearchSimple()CVCL::SearchSimple


Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by  doxygen 1.4.4