CVC3::DecisionEngineDFS Class Reference

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

#include <decision_engine_dfs.h>

Inherits CVC3::DecisionEngine.

Collaboration diagram for CVC3::DecisionEngineDFS:

List of all members.

Public Member Functions

• DecisionEngineDFS (TheoryCore *core, SearchImplBase *se)

  Constructor.
  

• virtual ~DecisionEngineDFS ()
• virtual Expr findSplitter (const Expr &e)

  Find the next splitter.
  

• virtual void goalSatisfied ()

  Search should call this when it derives 'false'.
  

Protected Member Functions

• virtual bool isBetter (const Expr &e1, const Expr &e2)

---

Detailed Description

Decision Engine for use with the Search Engine

Author: Clark Barrett.

Created: Fri Jul 11 16:34:22 2003

Definition at line 41 of file decision_engine_dfs.h.

---

Constructor & Destructor Documentation

DecisionEngineDFS::DecisionEngineDFS	(	TheoryCore *	core,
		SearchImplBase *	se
	)

Constructor.

Function: DecisionEngineDFS::DecisionEngineDFS

Author: Clark Barrett

Created: Sun Jul 13 22:52:51 2003

Constructor

Definition at line 49 of file decision_engine_dfs.cpp.

virtual CVC3::DecisionEngineDFS::~DecisionEngineDFS

(

)

[inline, virtual]

Definition at line 49 of file decision_engine_dfs.h.

---

Member Function Documentation

bool DecisionEngineDFS::isBetter	(	const Expr &	e1,
		const Expr &	e2
	)		[protected, virtual]

Implements CVC3::DecisionEngine.

Definition at line 32 of file decision_engine_dfs.cpp.

Expr DecisionEngineDFS::findSplitter

(

const Expr &

e

)

[virtual]

Find the next splitter.

Returns:

Null Expr if no splitter is found.

Function: DecisionEngineDFS::findSplitter

Author: Clark Barrett

Created: Sun Jul 13 22:53:18 2003

Main function to choose the next splitter.

Returns:

NULL if all known splitters are assigned.

Implements CVC3::DecisionEngine.

Definition at line 67 of file decision_engine_dfs.cpp.

References CVC3::ExprMap< Data >::clear(), CVC3::DecisionEngine::d_visited, CVC3::DecisionEngine::findSplitterRec(), IF_DEBUG, CVC3::Expr::isNull(), and TRACE.

void DecisionEngineDFS::goalSatisfied

(

)

[virtual]

Search should call this when it derives 'false'.

Implements CVC3::DecisionEngine.

Definition at line 88 of file decision_engine_dfs.cpp.

---

The documentation for this class was generated from the following files:

• decision_engine_dfs.h
• decision_engine_dfs.cpp