21 #ifndef _cvc3__include__search_simple_h_
22 #define _cvc3__include__search_simple_h_
Implementation of the simple search engine.
~SearchSimple()
Destructor.
Data structure of expressions in CVC3.
QueryResult checkValidInternal(const Expr &e)
Checks the validity of a formula in the current context.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
void addLiteralFact(const Theorem &thm)
Notify the search engine about a new literal fact.
CDO< Theorem > d_nonLiterals
Non-literals generated by DP's.
SearchSimple(TheoryCore *core)
Constructor.
QueryResult checkValidRec(Theorem &thm)
Recursive DPLL algorithm used by checkValid.
Description: Counters and flags for collecting run-time statistics.
void addNonLiteralFact(const Theorem &thm)
Notify the search engine about a new non-literal fact.
Abstract API to the proof search engine.
DecisionEngine * d_decisionEngine
Decision Engine.
const std::string & getName()
Name of this search engine.
API to to a generic proof search engine (a.k.a. SAT solver)
CDO< Theorem > d_simplifiedThm
Theorem which records simplification of the last query.
QueryResult restartInternal(const Expr &e)
Reruns last check with e as an additional assumption.
CDO< Theorem > d_goal
Formula being checked.
QueryResult checkValidMain(const Expr &e2)
Private helper function for checkValid and restart.