CVC3
2.4.1
|
API to to a generic proof search engine. More...
#include <search.h>
Public Member Functions | |
SearchEngine (TheoryCore *core) | |
Constructor. | |
virtual | ~SearchEngine () |
Destructor. | |
virtual const std::string & | getName ()=0 |
Name of this search engine. | |
CommonProofRules * | getCommonRules () |
Accessor for common rules. | |
TheoryCore * | theoryCore () |
Accessor for TheoryCore. | |
virtual void | registerAtom (const Expr &e)=0 |
Register an atomic formula of interest. | |
virtual Theorem | getImpliedLiteral ()=0 |
Return next literal implied by last assertion. Null Expr if none. | |
virtual void | push ()=0 |
Push a checkpoint. | |
virtual void | pop ()=0 |
Restore last checkpoint. | |
virtual QueryResult | checkValid (const Expr &e, Theorem &result)=0 |
Checks the validity of a formula in the current context. | |
virtual QueryResult | restart (const Expr &e, Theorem &result)=0 |
Reruns last check with e as an additional assumption. | |
virtual void | returnFromCheck ()=0 |
Returns to context immediately before last call to checkValid. | |
virtual Theorem | lastThm ()=0 |
Returns the result of the most recent valid theorem. | |
virtual Theorem | newUserAssumption (const Expr &e)=0 |
Generate and add an assumption to the set of assumptions in the current context. | |
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 void | getAssumptions (std::vector< Expr > &assumptions)=0 |
Get all assumptions made in this and all previous contexts. | |
virtual bool | isAssumption (const Expr &e)=0 |
Check if the formula has already been assumed previously. | |
virtual void | getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)=0 |
Will return the set of assertions which make the queried formula false. | |
virtual Proof | getProof ()=0 |
Returns the proof term for the last proven query. | |
void | getConcreteModel (ExprMap< Expr > &m) |
Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. | |
bool | tryModelGeneration (Theorem &thm) |
Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. | |
virtual FormulaValue | getValue (const CVC3::Expr &e)=0 |
Protected Member Functions | |
SearchEngineRules * | createRules () |
Create the trusted component. | |
SearchEngineRules * | createRules (SearchEngine *s_eng) |
Protected Attributes | |
TheoryCore * | d_core |
Access to theory reasoning. | |
CommonProofRules * | d_commonRules |
Common proof rules. | |
SearchEngineRules * | d_rules |
Proof rules for the search engine. |