Classes | Functions | Variables

Decision Engine

Search Engine

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

Collaboration diagram for Decision Engine:




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.

a NULL expr if no atomic formula is found.

Definition at line 55 of file decision_engine.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), CVC3::DecisionEngine::d_bestByExpr, CVC3::DecisionEngine::d_core, CVC3::DecisionEngine::d_se, CVC3::DecisionEngine::d_visited, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Theory::findExpr(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isAtomic(), CVC3::DecisionEngine::isBetter(), CVC3::Expr::isFalse(), CVC3::SearchImplBase::isGoodSplitter(), CVC3::Expr::isITE(), CVC3::Expr::isNull(), and CVC3::Expr::isTrue().

Referenced by CVC3::DecisionEngineDFS::findSplitter().

virtual bool CVC3::DecisionEngine::isBetter ( const Expr e1,
const Expr e2 
) [protected, pure virtual, inherited]
DecisionEngine::DecisionEngine ( TheoryCore core,
SearchImplBase se 
) [inherited]

Definition at line 32 of file decision_engine.cpp.

References CVC3::DecisionEngine::d_splitters, and IF_DEBUG.

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

Definition at line 61 of file decision_engine.h.

virtual Expr CVC3::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.

Null Expr if passed in a Null Expr.

Implemented in CVC3::DecisionEngineCaching, CVC3::DecisionEngineDFS, and CVC3::DecisionEngineMBTF.

Referenced by CVC3::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

whichCaseIf 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 128 of file decision_engine.cpp.

References CVC3::TheoryCore::addFact(), CVC3::SearchImplBase::addLiteralFact(), CVC3::DecisionEngine::d_core, CVC3::DecisionEngine::d_se, CVC3::DecisionEngine::d_splitterCount, CVC3::DecisionEngine::d_splitters, CVC3::TheoryCore::getCM(), CVC3::Theorem::getExpr(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::negate(), CVC3::SearchImplBase::newIntAssumption(), CVC3::ContextManager::push(), CVC3::CDList< T >::push_back(), and TRACE.

Referenced by CVC3::SearchEngineFast::split().

void DecisionEngine::popDecision ( ) [inherited]
void DecisionEngine::popTo ( int  dl) [inherited]
Expr DecisionEngine::lastSplitter ( ) [inherited]

Return the last known splitter.

Definition at line 164 of file decision_engine.cpp.

References CVC3::CDList< T >::back(), and CVC3::DecisionEngine::d_splitters.

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

Search should call this when it derives 'false'.

Implemented in CVC3::DecisionEngineCaching, CVC3::DecisionEngineDFS, and CVC3::DecisionEngineMBTF.

Referenced by CVC3::SearchEngineFast::checkSAT().

Variable Documentation

TheoryCore* CVC3::DecisionEngine::d_core [protected, inherited]
SearchImplBase* CVC3::DecisionEngine::d_se [protected, inherited]

Pointer to search engine.

Definition at line 42 of file decision_engine.h.

Referenced by CVC3::DecisionEngine::findSplitterRec(), and CVC3::DecisionEngine::pushDecision().

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

List of currently active splitters.

Definition at line 45 of file decision_engine.h.

Referenced by CVC3::DecisionEngine::DecisionEngine(), CVC3::DecisionEngine::lastSplitter(), and CVC3::DecisionEngine::pushDecision().

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

Total number of splitters.

Definition at line 48 of file decision_engine.h.

Referenced by CVC3::DecisionEngine::pushDecision().

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

Definition at line 50 of file decision_engine.h.

Referenced by CVC3::DecisionEngine::findSplitterRec().

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

Visited cache for findSplitterRec traversal.

Must be emptied in every findSplitter() call.

Definition at line 54 of file decision_engine.h.

Referenced by CVC3::DecisionEngineDFS::findSplitter(), and CVC3::DecisionEngine::findSplitterRec().