Decision Engine
[Search Engine]

Collaboration diagram for Decision Engine:

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

Classes

class CVC3::DecisionEngineDFS
Decision Engine for use with the Search Engine. 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.
void CVC3::DecisionEngine::pushDecision (Expr splitter, bool whichCase=true)
Push context and record the splitter.
void CVC3::DecisionEngine::popDecision ()
Pop last decision (and context).
void CVC3::DecisionEngine::popTo (int dl)
Pop to given scope.
Expr CVC3::DecisionEngine::lastSplitter ()
Return the last known splitter.
virtual void CVC3::DecisionEngine::goalSatisfied ()=0
Search should call this when it derives 'false'.

Variables

TheoryCore * CVC3::DecisionEngine::d_core
Pointer to core theory.
SearchImplBase * CVC3::DecisionEngine::d_se
Pointer to search engine.
CDList< Expr > CVC3::DecisionEngine::d_splitters
List of currently active splitters.
StatCounter CVC3::DecisionEngine::d_splitterCount
Total number of splitters.
ExprMap< Expr > CVC3::DecisionEngine::d_bestByExpr
ExprMap< Expr > CVC3::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 55 of file decision_engine.cpp.

References CVC3::DecisionEngine::d_bestByExpr, CVC3::DecisionEngine::d_core, CVC3::DecisionEngine::d_se, CVC3::DecisionEngine::d_visited, CVC3::Theory::findExpr(), CVC3::DecisionEngine::isBetter(), CVC3::SearchImplBase::isGoodSplitter(), and CVC3::Expr::isNull().

Referenced by CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), and CVC3::DecisionEngineCaching::findSplitter().

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

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

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

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.

Returns:: Null Expr if passed in a Null Expr.

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

Referenced by CVC3::SearchSimple::checkValidRec(), and 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

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 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(), and CVC3::TRACE.