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. | |
void | pushDecision (Expr splitter, bool whichCase=true) |
Push context and record the splitter. | |
void | popDecision () |
Pop last decision (and context) | |
void | popTo (int dl) |
Pop to given scope. | |
Expr | lastSplitter () |
Return the last known splitter. | |
virtual void | goalSatisfied ()=0 |
Search should call this when it derives 'false'. |
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. | |
SearchImplBase * | d_se |
Pointer to search engine. | |
CDList< Expr > | d_splitters |
List of currently active splitters. | |
StatCounter | d_splitterCount |
Total number of splitters. | |
ExprMap< Expr > | d_bestByExpr |
ExprMap< Expr > | d_visited |
Visited cache for findSplitterRec traversal. |
Definition at line 29 of file decision_engine.h.