#include <decision_engine.h>
Inheritance diagram for CVC3::DecisionEngine:
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... | |
Detailed Description
Definition at line 29 of file decision_engine.h.
The documentation for this class was generated from the following files:
