CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
Class List
Class Index
Class Hierarchy
Class Members
CVC3
SearchSimple
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
createRules
(SearchEngine *s_eng)
CVC3::SearchEngine
protected
d_applyCNFRulesCache
CVC3::SearchImplBase
protected
d_assumptions
CVC3::SearchImplBase
protected
d_bottomScope
CVC3::SearchImplBase
protected
d_cnfCache
CVC3::SearchImplBase
protected
d_cnfOption
CVC3::SearchImplBase
protected
d_cnfVars
CVC3::SearchImplBase
protected
d_commonRules
CVC3::SearchEngine
protected
d_core
CVC3::SearchEngine
protected
d_coreSatAPI_implBase
CVC3::SearchImplBase
protected
d_decisionEngine
CVC3::SearchSimple
private
d_dpSplitters
CVC3::SearchImplBase
protected
d_enqueueCNFCache
CVC3::SearchImplBase
protected
d_goal
CVC3::SearchSimple
private
d_ifLiftOption
CVC3::SearchImplBase
protected
d_ignoreCnfVarsOption
CVC3::SearchImplBase
protected
d_lastCounterExample
CVC3::SearchImplBase
protected
d_lastValid
CVC3::SearchImplBase
protected
d_name
CVC3::SearchSimple
private
d_nonLiterals
CVC3::SearchSimple
private
d_origFormulaOption
CVC3::SearchImplBase
protected
d_replaceITECache
CVC3::SearchImplBase
protected
d_rules
CVC3::SearchEngine
protected
d_simplifiedThm
CVC3::SearchSimple
private
d_vm
CVC3::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
getValue
(const CVC3::Expr &e)
CVC3::SearchImplBase
inline
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
tryModelGeneration
(Theorem &thm)
CVC3::SearchEngine
~SearchEngine
()
CVC3::SearchEngine
virtual
~SearchImplBase
()
CVC3::SearchImplBase
virtual
~SearchSimple
()
CVC3::SearchSimple
Generated on Sun Aug 5 2012 13:19:31 for CVC3 by
1.8.1.2