CVC3

CVC3::SearchEngine Member List

This is the complete list of members for CVC3::SearchEngine, including all inherited members.
checkValid(const Expr &e, Theorem &result)=0CVC3::SearchEngine [pure virtual]
createRules()CVC3::SearchEngine [protected]
createRules(SearchEngine *s_eng)CVC3::SearchEngine [protected]
d_commonRulesCVC3::SearchEngine [protected]
d_coreCVC3::SearchEngine [protected]
d_rulesCVC3::SearchEngine [protected]
getAssumptions(std::vector< Expr > &assumptions)=0CVC3::SearchEngine [pure virtual]
getCommonRules()CVC3::SearchEngine [inline]
getConcreteModel(ExprMap< Expr > &m)CVC3::SearchEngine
getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)=0CVC3::SearchEngine [pure virtual]
getImpliedLiteral()=0CVC3::SearchEngine [pure virtual]
getInternalAssumptions(std::vector< Expr > &assumptions)=0CVC3::SearchEngine [pure virtual]
getName()=0CVC3::SearchEngine [pure virtual]
getProof()=0CVC3::SearchEngine [pure virtual]
getUserAssumptions(std::vector< Expr > &assumptions)=0CVC3::SearchEngine [pure virtual]
getValue(const CVC3::Expr &e)=0CVC3::SearchEngine [pure virtual]
isAssumption(const Expr &e)=0CVC3::SearchEngine [pure virtual]
lastThm()=0CVC3::SearchEngine [pure virtual]
newUserAssumption(const Expr &e)=0CVC3::SearchEngine [pure virtual]
pop()=0CVC3::SearchEngine [pure virtual]
push()=0CVC3::SearchEngine [pure virtual]
registerAtom(const Expr &e)=0CVC3::SearchEngine [pure virtual]
restart(const Expr &e, Theorem &result)=0CVC3::SearchEngine [pure virtual]
returnFromCheck()=0CVC3::SearchEngine [pure virtual]
SearchEngine(TheoryCore *core)CVC3::SearchEngine
theoryCore()CVC3::SearchEngine [inline]
tryModelGeneration(Theorem &thm)CVC3::SearchEngine
~SearchEngine()CVC3::SearchEngine [virtual]