Decision Engine
[Search Engine]

Collaboration diagram for Decision Engine:

Decision Engine, used by Search Engine. More...

Classes

• class CVCL::DecisionEngineDFS

  Decision Engine for use with the Search Engine

  Author: Clark Barrett. More...
  

Functions

• Expr CVCL::DecisionEngine::findSplitterRec (const Expr &e)
• virtual bool CVCL::DecisionEngine::isBetter (const Expr &e1, const Expr &e2)=0
• CVCL::DecisionEngine::DecisionEngine (TheoryCore *core, SearchImplBase *se)
• virtual CVCL::DecisionEngine::~DecisionEngine ()
• virtual Expr CVCL::DecisionEngine::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 CVCL::DecisionEngine::pushDecision (Expr splitter, bool whichCase=true)

  Push context and record the splitter.
  

• void CVCL::DecisionEngine::popDecision ()

  Pop last decision (and context).
  

• void CVCL::DecisionEngine::popTo (int dl)

  Pop to given scope.
  

• Expr CVCL::DecisionEngine::lastSplitter ()

  Return the last known splitter.
  

• virtual void CVCL::DecisionEngine::goalSatisfied ()=0

  Search should call this when it derives 'false'.
  

Variables

• TheoryCore * CVCL::DecisionEngine::d_core

  Pointer to core theory.
  

• SearchImplBase * CVCL::DecisionEngine::d_se

  Pointer to search engine.
  

• CDList< Expr > CVCL::DecisionEngine::d_splitters

  List of currently active splitters.
  

• StatCounter CVCL::DecisionEngine::d_splitterCount

  Total number of splitters.
  

• ExprMap< Expr > CVCL::DecisionEngine::d_bestByExpr
• ExprMap< Expr > CVCL::DecisionEngine::d_visited

  Visited cache for findSplitterRec traversal.
  

---

Detailed Description

Decision Engine, used by Search Engine.

---

Function Documentation

Expr DecisionEngine::findSplitterRec (  const Expr &  e  )  [protected, inherited]

Function: DecisionEngine::findSplitterRec Author: Clark Barrett Created: Sun Jul 13 22:47:06 2003 Search the expression e (depth-first) for an atomic formula. Note that in order to support the "simplify in-place" option, each sub-expression is checked to see if it has a find pointer, and if it does, the find is followed instead of continuing to recurse on the given expression. Returns: a NULL expr if no atomic formula is found. Definition at line 63 of file decision_engine.cpp. References CVCL::Expr::arity(), CVCL::ExprMap< Data >::count(), CVCL::DecisionEngine::d_bestByExpr, CVCL::DecisionEngine::d_core, CVCL::DecisionEngine::d_se, CVCL::DecisionEngine::d_visited, CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), CVCL::Theory::findExpr(), CVCL::Expr::getHighestKid(), CVCL::Expr::isAbsAtomicFormula(), CVCL::Expr::isAtomic(), CVCL::DecisionEngine::isBetter(), CVCL::Expr::isFalse(), CVCL::SearchImplBase::isGoodSplitter(), CVCL::Expr::isITE(), CVCL::Expr::isNull(), and CVCL::Expr::isTrue(). Referenced by CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineDFS::findSplitter(), and CVCL::DecisionEngineCaching::findSplitter().

virtual bool CVCL::DecisionEngine::isBetter (  const Expr &  e1, const Expr &  e2 )  [protected, pure virtual, inherited]

Implemented in CVCL::DecisionEngineCaching, CVCL::DecisionEngineDFS, and CVCL::DecisionEngineMBTF. Referenced by CVCL::DecisionEngine::findSplitterRec().

DecisionEngine::DecisionEngine (  TheoryCore *  core, SearchImplBase *  se )  [inherited]

Definition at line 40 of file decision_engine.cpp. References CVCL::DecisionEngine::d_splitters, and IF_DEBUG().

virtual CVCL::DecisionEngine::~DecisionEngine (   )  [inline, virtual, inherited]

Definition at line 69 of file decision_engine.h.

virtual Expr CVCL::DecisionEngine::findSplitter (  const Expr &  e  )  [pure virtual, inherited]

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. Implemented in CVCL::DecisionEngineCaching, CVCL::DecisionEngineDFS, and CVCL::DecisionEngineMBTF. Referenced by CVCL::SearchSimple::checkValidRec(), and CVCL::SearchEngineFast::findSplitter().

void DecisionEngine::pushDecision (  Expr  splitter, bool  whichCase = true )  [inherited]

Push context and record the splitter. Function: DecisionEngine::pushDecision Author: Clark Barrett Created: Sun Jul 13 22:55:16 2003 Parameters: splitter  whichCase  If true, increment the splitter count and assert the splitter. If false, do NOT increment the splitter count and assert the negation of the splitter. Defaults to true. Definition at line 136 of file decision_engine.cpp. References CVCL::TheoryCore::addFact(), CVCL::SearchImplBase::addLiteralFact(), CVCL::DecisionEngine::d_core, CVCL::DecisionEngine::d_se, CVCL::DecisionEngine::d_splitterCount, CVCL::DecisionEngine::d_splitters, CVCL::TheoryCore::getCM(), CVCL::Theorem::getExpr(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::negate(), CVCL::SearchImplBase::newIntAssumption(), CVCL::ContextManager::push(), CVCL::CDList< T >::push_back(), and CVCL::TRACE. Referenced by CVCL::SearchSimple::checkValidRec(), and CVCL::SearchEngineFast::split().

void DecisionEngine::popDecision (   )  [inherited]

Pop last decision (and context). Definition at line 158 of file decision_engine.cpp. References CVCL::DecisionEngine::d_core, CVCL::TheoryCore::getCM(), and CVCL::ContextManager::pop(). Referenced by CVCL::SearchSimple::checkValidRec().

void DecisionEngine::popTo (  int  dl  )  [inherited]

Pop to given scope. Definition at line 164 of file decision_engine.cpp. References CVCL::DecisionEngine::d_core, CVCL::TheoryCore::getCM(), and CVCL::ContextManager::popto(). Referenced by CVCL::SearchEngineFast::fixConflict(), and CVCL::SearchEngineFast::traceConflict().

Expr DecisionEngine::lastSplitter (   )  [inherited]

Return the last known splitter. Definition at line 170 of file decision_engine.cpp. References CVCL::CDList< T >::back(), and CVCL::DecisionEngine::d_splitters.

virtual void CVCL::DecisionEngine::goalSatisfied (   )  [pure virtual, inherited]

Search should call this when it derives 'false'. Implemented in CVCL::DecisionEngineCaching, CVCL::DecisionEngineDFS, and CVCL::DecisionEngineMBTF. Referenced by CVCL::SearchEngineFast::checkSAT(), and CVCL::SearchSimple::checkValidRec().

---

Variable Documentation

TheoryCore* CVCL::DecisionEngine::d_core [protected, inherited]

Pointer to core theory. Definition at line 49 of file decision_engine.h. Referenced by CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::DecisionEngine::findSplitterRec(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::DecisionEngine::popDecision(), CVCL::DecisionEngine::popTo(), and CVCL::DecisionEngine::pushDecision().

SearchImplBase* CVCL::DecisionEngine::d_se [protected, inherited]

Pointer to search engine. Definition at line 50 of file decision_engine.h. Referenced by CVCL::DecisionEngine::findSplitterRec(), and CVCL::DecisionEngine::pushDecision().

CDList<Expr> CVCL::DecisionEngine::d_splitters [protected, inherited]

List of currently active splitters. Definition at line 53 of file decision_engine.h. Referenced by CVCL::DecisionEngine::DecisionEngine(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::DecisionEngine::lastSplitter(), and CVCL::DecisionEngine::pushDecision().

StatCounter CVCL::DecisionEngine::d_splitterCount [protected, inherited]

Total number of splitters. Definition at line 56 of file decision_engine.h. Referenced by CVCL::DecisionEngine::pushDecision().

ExprMap<Expr> CVCL::DecisionEngine::d_bestByExpr [protected, inherited]

Definition at line 58 of file decision_engine.h. Referenced by CVCL::DecisionEngine::findSplitterRec(), CVCL::DecisionEngineMBTF::goalSatisfied(), and CVCL::DecisionEngineCaching::goalSatisfied().

ExprMap<Expr> CVCL::DecisionEngine::d_visited [protected, inherited]

Visited cache for findSplitterRec traversal. Must be emptied in every findSplitter() call. Definition at line 62 of file decision_engine.h. Referenced by CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineDFS::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), and CVCL::DecisionEngine::findSplitterRec().

---