CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
CVC3::SearchEngine Class Referenceabstract

API to to a generic proof search engine. More...

#include <search.h>

Inheritance diagram for CVC3::SearchEngine:
CVC3::SearchImplBase CVC3::SearchSat CVC3::SearchEngineFast CVC3::SearchSimple

Public Member Functions

 SearchEngine (TheoryCore *core)
 Constructor. More...
 
virtual ~SearchEngine ()
 Destructor. More...
 
virtual const std::string & getName ()=0
 Name of this search engine. More...
 
CommonProofRulesgetCommonRules ()
 Accessor for common rules. More...
 
TheoryCoretheoryCore ()
 Accessor for TheoryCore. More...
 
virtual void registerAtom (const Expr &e)=0
 Register an atomic formula of interest. More...
 
virtual Theorem getImpliedLiteral ()=0
 Return next literal implied by last assertion. Null Expr if none. More...
 
virtual void push ()=0
 Push a checkpoint. More...
 
virtual void pop ()=0
 Restore last checkpoint. More...
 
virtual QueryResult checkValid (const Expr &e, Theorem &result)=0
 Checks the validity of a formula in the current context. More...
 
virtual QueryResult restart (const Expr &e, Theorem &result)=0
 Reruns last check with e as an additional assumption. More...
 
virtual void returnFromCheck ()=0
 Returns to context immediately before last call to checkValid. More...
 
virtual Theorem lastThm ()=0
 Returns the result of the most recent valid theorem. More...
 
virtual Theorem newUserAssumption (const Expr &e)=0
 Generate and add an assumption to the set of assumptions in the current context. More...
 
virtual void getUserAssumptions (std::vector< Expr > &assumptions)=0
 Get all user assumptions made in this and all previous contexts. More...
 
virtual void getInternalAssumptions (std::vector< Expr > &assumptions)=0
 Get assumptions made internally in this and all previous contexts. More...
 
virtual void getAssumptions (std::vector< Expr > &assumptions)=0
 Get all assumptions made in this and all previous contexts. More...
 
virtual bool isAssumption (const Expr &e)=0
 Check if the formula has already been assumed previously. More...
 
virtual void getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)=0
 Will return the set of assertions which make the queried formula false. More...
 
virtual Proof getProof ()=0
 Returns the proof term for the last proven query. More...
 
void getConcreteModel (ExprMap< Expr > &m)
 Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. More...
 
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. More...
 
virtual FormulaValue getValue (const CVC3::Expr &e)=0
 

Protected Member Functions

SearchEngineRulescreateRules ()
 Create the trusted component. More...
 
SearchEngineRulescreateRules (SearchEngine *s_eng)
 

Protected Attributes

TheoryCored_core
 Access to theory reasoning. More...
 
CommonProofRulesd_commonRules
 Common proof rules. More...
 
SearchEngineRulesd_rules
 Proof rules for the search engine. More...
 

Detailed Description

API to to a generic proof search engine.

Definition at line 50 of file search.h.


The documentation for this class was generated from the following files: