CVC3::DecisionEngine Class Reference

#include <decision_engine.h>

Inherited by CVC3::DecisionEngineCaching, CVC3::DecisionEngineDFS, and CVC3::DecisionEngineMBTF.

Collaboration 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.
  

---

Detailed Description

Definition at line 29 of file decision_engine.h.

---

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

• decision_engine.h
• decision_engine.cpp