# CVCL::SearchEngine Class Reference

[Search Engine]

API to to a generic proof search engine.
More...
`#include <search.h>`

Inheritance diagram for CVCL::SearchEngine:

[legend]Collaboration diagram for CVCL::SearchEngine:
[legend]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.

- 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 Theorem checkValid (const Expr &e)=0
- Checks the validity of a formula in the current context.

- virtual Theorem restart (const Expr &e)=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, int scope=-1)=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 an invalid query.

## Protected Member Functions

## Protected Attributes

## Detailed Description

API to to a generic proof search engine.

Definition at line 56 of file search.h.

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

Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by
1.4.4