CVC3: Decision Engine

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::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::DecisionEngine::isBetter(), CVC3::SearchImplBase::isGoodSplitter(), and CVC3::Expr::isNull().

Referenced by CVC3::DecisionEngineDFS::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(), CVC3::CDList< T >::push_back(), and CVC3::TRACE.