CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
Class List
Class Index
Class Hierarchy
Class Members
CVC3
SearchImplBase
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)=0
CVC3::SearchImplBase
protected
pure virtual
addNonLiteralFact
(const Theorem &thm)=0
CVC3::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)=0
CVC3::SearchImplBase
pure virtual
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_dpSplitters
CVC3::SearchImplBase
protected
d_enqueueCNFCache
CVC3::SearchImplBase
protected
d_ifLiftOption
CVC3::SearchImplBase
protected
d_ignoreCnfVarsOption
CVC3::SearchImplBase
protected
d_lastCounterExample
CVC3::SearchImplBase
protected
d_lastValid
CVC3::SearchImplBase
protected
d_origFormulaOption
CVC3::SearchImplBase
protected
d_replaceITECache
CVC3::SearchImplBase
protected
d_rules
CVC3::SearchEngine
protected
d_vm
CVC3::SearchImplBase
protected
DecisionEngine
class
CVC3::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
()=0
CVC3::SearchEngine
pure 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
replaceITE
(const Expr &e)
CVC3::SearchImplBase
private
restart
(const Expr &e, Theorem &result)
CVC3::SearchImplBase
virtual
restartInternal
(const Expr &e)=0
CVC3::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
tryModelGeneration
(Theorem &thm)
CVC3::SearchEngine
~SearchEngine
()
CVC3::SearchEngine
virtual
~SearchImplBase
()
CVC3::SearchImplBase
virtual
Generated on Mon Aug 6 2012 09:40:13 for CVC3 by
1.8.1.1