CVC3  2.4.1
Classes | Functions | Variables
Decision Engine

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

Classes

class  CVC3::DecisionEngineDFS
 Decision Engine for use with the Search EngineAuthor: Clark Barrett. More...
 

Functions

Expr CVC3::DecisionEngine::findSplitterRec (const Expr &e)
 
virtual bool CVC3::DecisionEngine::isBetter (const Expr &e1, const Expr &e2)=0
 
 CVC3::DecisionEngine::DecisionEngine (TheoryCore *core, SearchImplBase *se)
 
virtual CVC3::DecisionEngine::~DecisionEngine ()
 
virtual Expr CVC3::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. More...
 
void CVC3::DecisionEngine::pushDecision (Expr splitter, bool whichCase=true)
 Push context and record the splitter. More...
 
void CVC3::DecisionEngine::popDecision ()
 Pop last decision (and context) More...
 
void CVC3::DecisionEngine::popTo (int dl)
 Pop to given scope. More...
 
Expr CVC3::DecisionEngine::lastSplitter ()
 Return the last known splitter. More...
 
virtual void CVC3::DecisionEngine::goalSatisfied ()=0
 Search should call this when it derives 'false'. More...
 

Variables

TheoryCore * CVC3::DecisionEngine::d_core
 Pointer to core theory. More...
 
SearchImplBase * CVC3::DecisionEngine::d_se
 Pointer to search engine. More...
 
CDList< Expr > CVC3::DecisionEngine::d_splitters
 List of currently active splitters. More...
 
StatCounter CVC3::DecisionEngine::d_splitterCount
 Total number of splitters. More...
 
ExprMap< Expr > CVC3::DecisionEngine::d_bestByExpr
 
ExprMap< Expr > CVC3::DecisionEngine::d_visited
 Visited cache for findSplitterRec traversal. More...
 

Detailed Description

Decision Engine, used by Search Engine.

Function Documentation

Expr DecisionEngine::findSplitterRec ( const Expr e)
protected

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 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 
)
protectedpure virtual
DecisionEngine::DecisionEngine ( TheoryCore core,
SearchImplBase se 
)

Definition at line 32 of file decision_engine.cpp.

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

virtual CVC3::DecisionEngine::~DecisionEngine ( )
inlinevirtual

Definition at line 61 of file decision_engine.h.

virtual Expr CVC3::DecisionEngine::findSplitter ( const Expr e)
pure virtual

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 CVC3::DecisionEngineDFS, CVC3::DecisionEngineCaching, and CVC3::DecisionEngineMBTF.

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

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

Push context and record the splitter.

Function: DecisionEngine::pushDecision

Author: Clark Barrett

Created: Sun Jul 13 22:55:16 2003

Parameters
splitter
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 ( )
void DecisionEngine::popTo ( int  dl)
Expr DecisionEngine::lastSplitter ( )

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

Search should call this when it derives 'false'.

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

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

Variable Documentation

TheoryCore* CVC3::DecisionEngine::d_core
protected
SearchImplBase* CVC3::DecisionEngine::d_se
protected

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

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

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

Definition at line 50 of file decision_engine.h.

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

ExprMap<Expr> CVC3::DecisionEngine::d_visited
protected

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().