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::SearchEnginepure virtual
createRules()CVC3::SearchEngineprotected
createRules(SearchEngine *s_eng)CVC3::SearchEngineprotected
d_commonRulesCVC3::SearchEngineprotected
d_coreCVC3::SearchEngineprotected
d_rulesCVC3::SearchEngineprotected
getAssumptions(std::vector< Expr > &assumptions)=0CVC3::SearchEnginepure virtual
getCommonRules()CVC3::SearchEngineinline
getConcreteModel(ExprMap< Expr > &m)CVC3::SearchEngine
getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)=0CVC3::SearchEnginepure virtual
getImpliedLiteral()=0CVC3::SearchEnginepure virtual
getInternalAssumptions(std::vector< Expr > &assumptions)=0CVC3::SearchEnginepure virtual
getName()=0CVC3::SearchEnginepure virtual
getProof()=0CVC3::SearchEnginepure virtual
getUserAssumptions(std::vector< Expr > &assumptions)=0CVC3::SearchEnginepure virtual
getValue(const CVC3::Expr &e)=0CVC3::SearchEnginepure virtual
isAssumption(const Expr &e)=0CVC3::SearchEnginepure virtual
lastThm()=0CVC3::SearchEnginepure virtual
newUserAssumption(const Expr &e)=0CVC3::SearchEnginepure virtual
pop()=0CVC3::SearchEnginepure virtual
push()=0CVC3::SearchEnginepure virtual
registerAtom(const Expr &e)=0CVC3::SearchEnginepure virtual
restart(const Expr &e, Theorem &result)=0CVC3::SearchEnginepure virtual
returnFromCheck()=0CVC3::SearchEnginepure virtual
SearchEngine(TheoryCore *core)CVC3::SearchEngine
theoryCore()CVC3::SearchEngineinline
tryModelGeneration(Theorem &thm)CVC3::SearchEngine
~SearchEngine()CVC3::SearchEnginevirtual