22 #ifndef _cvc3__include__search_h_
23 #define _cvc3__include__search_h_
32 class SearchEngineRules;
37 class CommonProofRules;
39 template<
class Data>
class ExprMap;
81 virtual const std::string&
getName() = 0;
101 virtual void push() = 0;
104 virtual void pop() = 0;
173 bool inOrder =
true) = 0;
virtual const std::string & getName()=0
Name of this search engine.
API to to a generic proof search engine.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
virtual void getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)=0
Will return the set of assertions which make the queried formula false.
void getConcreteModel(ExprMap< Expr > &m)
Build a concrete Model (assign values to variables), should only be called after a query which return...
virtual void getAssumptions(std::vector< Expr > &assumptions)=0
Get all assumptions made in this and all previous contexts.
virtual QueryResult restart(const Expr &e, Theorem &result)=0
Reruns last check with e as an additional assumption.
bool tryModelGeneration(Theorem &thm)
Try to build a concrete Model (assign values to variables), should only be called after a query which...
virtual Theorem getImpliedLiteral()=0
Return next literal implied by last assertion. Null Expr if none.
virtual FormulaValue getValue(const CVC3::Expr &e)=0
enumerated type for result of queries
CommonProofRules * d_commonRules
Common proof rules.
SearchEngineRules * d_rules
Proof rules for the search engine.
virtual Proof getProof()=0
Returns the proof term for the last proven query.
virtual Theorem newUserAssumption(const Expr &e)=0
Generate and add an assumption to the set of assumptions in the current context.
virtual void pop()=0
Restore last checkpoint.
virtual void push()=0
Push a checkpoint.
virtual QueryResult checkValid(const Expr &e, Theorem &result)=0
Checks the validity of a formula in the current context.
virtual ~SearchEngine()
Destructor.
CommonProofRules * getCommonRules()
Accessor for common rules.
SearchEngine(TheoryCore *core)
Constructor.
virtual void returnFromCheck()=0
Returns to context immediately before last call to checkValid.
virtual void getUserAssumptions(std::vector< Expr > &assumptions)=0
Get all user assumptions made in this and all previous contexts.
virtual void getInternalAssumptions(std::vector< Expr > &assumptions)=0
Get assumptions made internally in this and all previous contexts.
virtual bool isAssumption(const Expr &e)=0
Check if the formula has already been assumed previously.
virtual Theorem lastThm()=0
Returns the result of the most recent valid theorem.
virtual void registerAtom(const Expr &e)=0
Register an atomic formula of interest.
TheoryCore * theoryCore()
Accessor for TheoryCore.
SearchEngineRules * createRules()
Create the trusted component.
API to the proof rules for the Search Engines.
TheoryCore * d_core
Access to theory reasoning.