CVC3::DecisionEngineCaching Class Reference

#include <decision_engine_caching.h>

Inheritance diagram for CVC3::DecisionEngineCaching:

Inheritance graph
[legend]
Collaboration diagram for CVC3::DecisionEngineCaching:

Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Protected Member Functions

Private Attributes


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 (  )  [inline, virtual]

Definition at line 50 of file decision_engine_caching.h.


Member Function Documentation

virtual bool CVC3::DecisionEngineCaching::isBetter ( const Expr e1,
const Expr e2 
) [protected, virtual]

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

Definition at line 36 of file decision_engine_caching.h.

Definition at line 37 of file decision_engine_caching.h.

Definition at line 38 of file decision_engine_caching.h.

Definition at line 39 of file decision_engine_caching.h.

Definition at line 40 of file decision_engine_caching.h.

Definition at line 42 of file decision_engine_caching.h.

Definition at line 43 of file decision_engine_caching.h.


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

Generated on Thu Oct 15 22:24:29 2009 for CVC3 by  doxygen 1.5.8