CVC3
2.4.1
|
Decision Engine for use with the Search EngineAuthor: Clark Barrett. More...
#include <decision_engine_dfs.h>
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.
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.
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.
Function: DecisionEngineDFS::findSplitter
Author: Clark Barrett
Created: Sun Jul 13 22:53:18 2003
Main function to choose the next splitter.
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.