CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager Class Reference
[Fast Search Engine]
Public Member Functions
- ConflictClauseManager (Context *context, SearchEngineFast *se)
- void setRestorePoint ()
- void notify ()
Private Attributes
- SearchEngineFast * d_se
- std::vector< int > d_restorePoints
Detailed Description
Definition at line 150 of file search_fast.h.
Constructor & Destructor Documentation
| CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::ConflictClauseManager | ( | Context * | context, | |
| SearchEngineFast * | se | |||
| ) | [inline] |
Definition at line 154 of file search_fast.h.
Member Function Documentation
| void SearchEngineFast::ConflictClauseManager::setRestorePoint | ( | ) |
Definition at line 42 of file search_fast.cpp.
References CVC3::SearchEngineFast::d_conflictClauses, CVC3::SearchEngineFast::d_conflictClauseStack, CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::d_restorePoints, CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::d_se, CVC3::SearchImplBase::scopeLevel(), and CVC3::TRACE.
Referenced by CVC3::SearchEngineFast::checkValidInternal().
| void SearchEngineFast::ConflictClauseManager::notify | ( | void | ) | [virtual] |
Reimplemented from CVC3::ContextNotifyObj.
Definition at line 53 of file search_fast.cpp.
References CVC3::SearchEngineFast::d_conflictClauses, CVC3::SearchEngineFast::d_conflictClauseStack, CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::d_restorePoints, CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::d_se, CVC3::SearchImplBase::scopeLevel(), and CVC3::TRACE.
Member Data Documentation
SearchEngineFast* CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::d_se [private] |
Definition at line 151 of file search_fast.h.
Referenced by CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::notify(), and CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::setRestorePoint().
std::vector<int> CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::d_restorePoints [private] |
Definition at line 152 of file search_fast.h.
Referenced by CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::notify(), and CVC3::SearchEngineFast::SearchEngineFast::ConflictClauseManager::setRestorePoint().
The documentation for this class was generated from the following files:
