CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
CVC3::DecisionEngine Class Reference

#include <decision_engine.h>

Inheritance diagram for CVC3::DecisionEngine:
CVC3::DecisionEngineCaching CVC3::DecisionEngineDFS CVC3::DecisionEngineMBTF

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

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 29 of file decision_engine.h.


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