CVC3  2.4.1
Classes | Public Member Functions | Protected Member Functions | Private Attributes
CVC3::DecisionEngineCaching Class Reference

#include <decision_engine_caching.h>

Inheritance diagram for CVC3::DecisionEngineCaching:
CVC3::DecisionEngine

List of all members.

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'.
- Public Member Functions inherited from CVC3::DecisionEngine
 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)
- Protected Member Functions inherited from CVC3::DecisionEngine
Expr findSplitterRec (const Expr &e)

Private Attributes

int d_startLevel
int d_bottomLevel
int d_topLevel
bool d_topLevelLock
int d_height
std::vector< CacheEntryd_cache
ExprMap< int > d_index

Additional Inherited Members

- Protected Attributes inherited from CVC3::DecisionEngine
TheoryCored_core
 Pointer to core theory.
SearchImplBased_se
 Pointer to search engine.
CDList< Exprd_splitters
 List of currently active splitters.
StatCounter d_splitterCount
 Total number of splitters.
ExprMap< Exprd_bestByExpr
ExprMap< Exprd_visited
 Visited cache for findSplitterRec traversal.

Detailed Description

Definition at line 24 of file decision_engine_caching.h.


Constructor & Destructor Documentation

CVC3::DecisionEngineCaching::DecisionEngineCaching ( TheoryCore core,
SearchImplBase se 
)
virtual CVC3::DecisionEngineCaching::~DecisionEngineCaching ( )
inlinevirtual

Definition at line 50 of file decision_engine_caching.h.


Member Function Documentation

virtual bool CVC3::DecisionEngineCaching::isBetter ( const Expr e1,
const Expr e2 
)
protectedvirtual

Implements CVC3::DecisionEngine.

virtual Expr CVC3::DecisionEngineCaching::findSplitter ( const Expr e)
virtual

Finds a splitter inside a non const expression. The expression passed in must not be a boolean constant, otherwise a DebugAssert will occur.

Returns:
Null Expr if passed in a Null Expr.

Implements CVC3::DecisionEngine.

virtual void CVC3::DecisionEngineCaching::goalSatisfied ( )
virtual

Search should call this when it derives 'false'.

Implements CVC3::DecisionEngine.


Member Data Documentation

int CVC3::DecisionEngineCaching::d_startLevel
private

Definition at line 36 of file decision_engine_caching.h.

int CVC3::DecisionEngineCaching::d_bottomLevel
private

Definition at line 37 of file decision_engine_caching.h.

int CVC3::DecisionEngineCaching::d_topLevel
private

Definition at line 38 of file decision_engine_caching.h.

bool CVC3::DecisionEngineCaching::d_topLevelLock
private

Definition at line 39 of file decision_engine_caching.h.

int CVC3::DecisionEngineCaching::d_height
private

Definition at line 40 of file decision_engine_caching.h.

std::vector<CacheEntry> CVC3::DecisionEngineCaching::d_cache
private

Definition at line 42 of file decision_engine_caching.h.

ExprMap<int> CVC3::DecisionEngineCaching::d_index
private

Definition at line 43 of file decision_engine_caching.h.


The documentation for this class was generated from the following file: