CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
Class List
Class Index
Class Hierarchy
Class Members
CVC3
DecisionEngine
Public Member Functions
|
Protected Member Functions
|
Protected Attributes
CVC3::DecisionEngine Class Reference
#include <
decision_engine.h
>
Inheritance diagram for CVC3::DecisionEngine:
List of all members.
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.
The documentation for this class was generated from the following files:
decision_engine.h
decision_engine.cpp
Generated on Thu Oct 6 2011 22:29:46 for CVC3 by
1.7.5