CVC3::SearchEngineFast::ConflictClauseManager Class Reference
[Fast Search Engine]

Inheritance diagram for CVC3::SearchEngineFast::ConflictClauseManager:

[legend]Collaboration diagram for CVC3::SearchEngineFast::ConflictClauseManager:

[legend]List of all members.

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::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, d_restorePoints, d_se, CVC3::SearchImplBase::scopeLevel(), and CVC3::TRACE.

Referenced by CVC3::SearchEngineFast::checkValidInternal().

void SearchEngineFast::ConflictClauseManager::notify

(

)

[virtual]

Reimplemented from CVC3::ContextNotifyObj.

Definition at line 53 of file search_fast.cpp.

References CVC3::SearchEngineFast::d_conflictClauses, CVC3::SearchEngineFast::d_conflictClauseStack, d_restorePoints, d_se, CVC3::SearchImplBase::scopeLevel(), and CVC3::TRACE.

---

Member Data Documentation

SearchEngineFast* CVC3::SearchEngineFast::ConflictClauseManager::d_se [private]

Definition at line 151 of file search_fast.h.

Referenced by notify(), and setRestorePoint().

std::vector<int> CVC3::SearchEngineFast::ConflictClauseManager::d_restorePoints [private]

Definition at line 152 of file search_fast.h.

Referenced by notify(), and setRestorePoint().

---

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

• search_fast.h
• search_fast.cpp

---