CVC3
2.4.1
|
#include <decision_engine.h>
Public Member Functions | |
DecisionEngine (TheoryCore *core, SearchImplBase *se) | |
virtual | ~DecisionEngine () |
virtual Expr | findSplitter (const Expr &e)=0 |
Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur. More... | |
void | pushDecision (Expr splitter, bool whichCase=true) |
Push context and record the splitter. More... | |
void | popDecision () |
Pop last decision (and context) More... | |
void | popTo (int dl) |
Pop to given scope. More... | |
Expr | lastSplitter () |
Return the last known splitter. More... | |
virtual void | goalSatisfied ()=0 |
Search should call this when it derives 'false'. More... | |
Protected Member Functions | |
Expr | findSplitterRec (const Expr &e) |
virtual bool | isBetter (const Expr &e1, const Expr &e2)=0 |
Protected Attributes | |
TheoryCore * | d_core |
Pointer to core theory. More... | |
SearchImplBase * | d_se |
Pointer to search engine. More... | |
CDList< Expr > | d_splitters |
List of currently active splitters. More... | |
StatCounter | d_splitterCount |
Total number of splitters. More... | |
ExprMap< Expr > | d_bestByExpr |
ExprMap< Expr > | d_visited |
Visited cache for findSplitterRec traversal. More... | |
Definition at line 29 of file decision_engine.h.