CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes
CVC3::SearchEngine Class Reference

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

List of all members.

Public Member Functions

 SearchEngine (TheoryCore *core)
 Constructor.
virtual ~SearchEngine ()
 Destructor.
virtual const std::string & getName ()=0
 Name of this search engine.
CommonProofRulesgetCommonRules ()
 Accessor for common rules.
TheoryCoretheoryCore ()
 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

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

Protected Attributes

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

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: