CVC3::SearchEngine Class Reference

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

#include <search.h>

Inherited by CVC3::SearchImplBase, and CVC3::SearchSat.

Collaboration diagram for CVC3::SearchEngine:

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.
  

• 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

API to to a generic proof search engine.

Definition at line 51 of file search.h.

---

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

• search.h
• search.cpp
• search_theorem_producer.cpp