CVC3::SearchSimple Class Reference

Implementation of the simple search engine. More...

#include <search_simple.h>

Inherits CVC3::SearchImplBase.

Collaboration diagram for CVC3::SearchSimple:

List of all members.

Public Member Functions

• SearchSimple (TheoryCore *core)

  Constructor.
  

• ~SearchSimple ()

  Destructor.
  

• const std::string & getName ()

  Name of this search engine.
  

• QueryResult checkValidInternal (const Expr &e)

  Checks the validity of a formula in the current context.
  

• QueryResult restartInternal (const Expr &e)

  Reruns last check with e as an additional assumption.
  

• void addLiteralFact (const Theorem &thm)

  Notify the search engine about a new literal fact.
  

• void addNonLiteralFact (const Theorem &thm)

  Notify the search engine about a new non-literal fact.
  

Private Member Functions

• QueryResult checkValidRec (Theorem &thm)

  Recursive DPLL algorithm used by checkValid.
  

• QueryResult checkValidMain (const Expr &e2)

  Private helper function for checkValid and restart.
  

Private Attributes

• std::string d_name

  Name.
  

• DecisionEngine * d_decisionEngine

  Decision Engine.
  

• CDO< Theorem > d_goal

  Formula being checked.
  

• CDO< Theorem > d_nonLiterals

  Non-literals generated by DP's.
  

• CDO< Theorem > d_simplifiedThm

  Theorem which records simplification of the last query.
  

---

Detailed Description

Implementation of the simple search engine.

Definition at line 41 of file search_simple.h.

---

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

• search_simple.h
• search_simple.cpp