CVC3
2.4.1
|
Decision Engine for use with the Search EngineAuthor: Clark Barrett. More...
#include <decision_engine_dfs.h>
Public Member Functions | |
DecisionEngineDFS (TheoryCore *core, SearchImplBase *se) | |
Constructor. More... | |
virtual | ~DecisionEngineDFS () |
virtual Expr | findSplitter (const Expr &e) |
Find the next splitter. More... | |
virtual void | goalSatisfied () |
Search should call this when it derives 'false'. More... | |
![]() | |
DecisionEngine (TheoryCore *core, SearchImplBase *se) | |
virtual | ~DecisionEngine () |
void | pushDecision (Expr splitter, bool whichCase=true) |
Push context and record the splitter. More... | |
void | popDecision () |
Pop last decision (and context) More... | |
void | popTo (int dl) |
Pop to given scope. More... | |
Expr | lastSplitter () |
Return the last known splitter. More... | |
Protected Member Functions | |
virtual bool | isBetter (const Expr &e1, const Expr &e2) |
![]() | |
Expr | findSplitterRec (const Expr &e) |
Additional Inherited Members | |
![]() | |
TheoryCore * | d_core |
Pointer to core theory. More... | |
SearchImplBase * | d_se |
Pointer to search engine. More... | |
CDList< Expr > | d_splitters |
List of currently active splitters. More... | |
StatCounter | d_splitterCount |
Total number of splitters. More... | |
ExprMap< Expr > | d_bestByExpr |
ExprMap< Expr > | d_visited |
Visited cache for findSplitterRec traversal. More... | |
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.
|
inlinevirtual |
Definition at line 49 of file decision_engine_dfs.h.
Implements CVC3::DecisionEngine.
Definition at line 32 of file decision_engine_dfs.cpp.
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.
|
virtual |
Search should call this when it derives 'false'.
Implements CVC3::DecisionEngine.
Definition at line 88 of file decision_engine_dfs.cpp.