CVC3
2.4.1
|
#include <decision_engine_caching.h>
Classes | |
class | CacheEntry |
Public Member Functions | |
DecisionEngineCaching (TheoryCore *core, SearchImplBase *se) | |
virtual | ~DecisionEngineCaching () |
virtual Expr | findSplitter (const Expr &e) |
Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur. | |
virtual void | goalSatisfied () |
Search should call this when it derives 'false'. | |
![]() | |
DecisionEngine (TheoryCore *core, SearchImplBase *se) | |
virtual | ~DecisionEngine () |
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. |
Protected Member Functions | |
virtual bool | isBetter (const Expr &e1, const Expr &e2) |
![]() | |
Expr | findSplitterRec (const Expr &e) |
Private Attributes | |
int | d_startLevel |
int | d_bottomLevel |
int | d_topLevel |
bool | d_topLevelLock |
int | d_height |
std::vector< CacheEntry > | d_cache |
ExprMap< int > | d_index |
Additional Inherited Members | |
![]() | |
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 24 of file decision_engine_caching.h.
CVC3::DecisionEngineCaching::DecisionEngineCaching | ( | TheoryCore * | core, |
SearchImplBase * | se | ||
) |
|
inlinevirtual |
Definition at line 50 of file decision_engine_caching.h.
|
protectedvirtual |
Implements CVC3::DecisionEngine.
Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur.
Implements CVC3::DecisionEngine.
|
virtual |
Search should call this when it derives 'false'.
Implements CVC3::DecisionEngine.
|
private |
Definition at line 36 of file decision_engine_caching.h.
|
private |
Definition at line 37 of file decision_engine_caching.h.
|
private |
Definition at line 38 of file decision_engine_caching.h.
|
private |
Definition at line 39 of file decision_engine_caching.h.
|
private |
Definition at line 40 of file decision_engine_caching.h.
|
private |
Definition at line 42 of file decision_engine_caching.h.
|
private |
Definition at line 43 of file decision_engine_caching.h.