API to to a generic proof search engine. More...
#include <search.h>
Inherited by CVC3::SearchImplBase, and CVC3::SearchSat.
Collaboration diagram for CVC3::SearchEngine:
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. | |
Detailed Description
The documentation for this class was generated from the following files:
