21 #ifndef _cvc3__search__decision_engine_h_
22 #define _cvc3__search__decision_engine_h_
virtual void goalSatisfied()=0
Search should call this when it derives 'false'.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr findSplitterRec(const Expr &e)
ExprMap< Expr > d_visited
Visited cache for findSplitterRec traversal.
Expr lastSplitter()
Return the last known splitter.
virtual bool isBetter(const Expr &e1, const Expr &e2)=0
Description: Counters and flags for collecting run-time statistics.
virtual Expr findSplitter(const Expr &e)=0
Finds a splitter inside a non const expression. The expression passed in must not be a boolean consta...
SearchImplBase * d_se
Pointer to search engine.
void pushDecision(Expr splitter, bool whichCase=true)
Push context and record the splitter.
virtual ~DecisionEngine()
void popTo(int dl)
Pop to given scope.
TheoryCore * d_core
Pointer to core theory.
ExprMap< Expr > d_bestByExpr
CDList< Expr > d_splitters
List of currently active splitters.
void popDecision()
Pop last decision (and context)
API to to a generic proof search engine (a.k.a. SAT solver)
StatCounter d_splitterCount
Total number of splitters.
DecisionEngine(TheoryCore *core, SearchImplBase *se)