#include <decision_engine.h>
Inherited by CVC3::DecisionEngineCaching, CVC3::DecisionEngineDFS, and CVC3::DecisionEngineMBTF.
Collaboration 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. | |
| 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. | |
Detailed Description
Definition at line 29 of file decision_engine.h.
The documentation for this class was generated from the following files:
