No more Theorems can be created after this call, only deleted. The purpose of this call is to dis-entangle the mutual dependency of ExprManager and TheoremManager during destruction time.

Definition at line 76 of file theorem_manager.cpp.

References d_active, and d_rules.

bool CVC3::TheoremManager::isActive ( ) [inline]

Test whether the TheoremManager is still active.

Definition at line 73 of file theorem_manager.h.

References d_active.

Referenced by CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().

ContextManager* CVC3::TheoremManager::getCM ( ) const [inline]

Definition at line 75 of file theorem_manager.h.

References d_cm.

Referenced by CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().

ExprManager* CVC3::TheoremManager::getEM ( ) const [inline]

Definition at line 76 of file theorem_manager.h.

References d_em.

Referenced by CVC3::TheoremProducer::newLabel(), CVC3::TheoremProducer::newPf(), and CVC3::CommonTheoremProducer::substitutivityRule().

const CLFlags& CVC3::TheoremManager::getFlags ( ) const [inline]

Definition at line 77 of file theorem_manager.h.

References d_flags.

Referenced by CVC3::TheoremProducer::newLabel(), CVC3::SearchEngineTheoremProducer::satProof(), and CVC3::SearchEngine::SearchEngine().

MemoryManager* CVC3::TheoremManager::getMM ( ) const [inline]

Definition at line 78 of file theorem_manager.h.

References d_mm.

Referenced by CVC3::RegTheoremValue::getMM().

MemoryManager* CVC3::TheoremManager::getRWMM ( ) const [inline]

Definition at line 79 of file theorem_manager.h.

References d_rwmm.

Referenced by CVC3::RWTheoremValue::getMM(), and CVC3::Theorem::Theorem().

CommonProofRules* CVC3::TheoremManager::getRules ( ) const [inline]

Definition at line 80 of file theorem_manager.h.

References d_rules.

Referenced by CVC3::TheoryCore::TheoryCore().

unsigned CVC3::TheoremManager::getFlag ( ) const [inline]

Definition at line 82 of file theorem_manager.h.

References d_flag.

Referenced by CVC3::TheoremValue::isFlagged(), and CVC3::TheoremValue::setFlag().

void CVC3::TheoremManager::clearAllFlags ( ) [inline]

Definition at line 86 of file theorem_manager.h.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::clear(), d_flag, d_reflFlags, and FatalAssert.

Referenced by CVC3::TheoremValue::clearAllFlags().

bool CVC3::TheoremManager::withProof ( ) [inline]

Definition at line 91 of file theorem_manager.h.

References d_withProof.

Referenced by CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), CVC3::SearchSat::SearchSat(), and CVC3::TheoremProducer::withProof().

bool CVC3::TheoremManager::withAssumptions ( ) [inline]

Definition at line 94 of file theorem_manager.h.

References d_withAssump.

Referenced by CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchImplBase::getCounterExample(), and CVC3::TheoremProducer::withAssumptions().

void CVC3::TheoremManager::setFlag ( long ptr ) [inline]

Definition at line 99 of file theorem_manager.h.

References d_reflFlags.

bool CVC3::TheoremManager::isFlagged ( long ptr ) [inline]

Definition at line 100 of file theorem_manager.h.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), and d_reflFlags.

void CVC3::TheoremManager::setCachedValue	(	long	ptr,
		int	value
	)		`[inline]`

Definition at line 101 of file theorem_manager.h.

References d_cachedValues.

int CVC3::TheoremManager::getCachedValue ( long ptr ) [inline]

Definition at line 102 of file theorem_manager.h.

References d_cachedValues, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find().

void CVC3::TheoremManager::setExpandFlag	(	long	ptr,
		bool	value
	)		`[inline]`

Definition at line 107 of file theorem_manager.h.

References d_expandFlags.

bool CVC3::TheoremManager::getExpandFlag ( long ptr ) [inline]

Definition at line 108 of file theorem_manager.h.

References d_expandFlags, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find().

void CVC3::TheoremManager::setLitFlag	(	long	ptr,
		bool	value
	)		`[inline]`

Definition at line 113 of file theorem_manager.h.

References d_litFlags.

bool CVC3::TheoremManager::getLitFlag ( long ptr ) [inline]

Definition at line 114 of file theorem_manager.h.

References d_litFlags, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find().

Member Data Documentation

ContextManager* CVC3::TheoremManager::d_cm [private]

Definition at line 41 of file theorem_manager.h.

Referenced by getCM().

ExprManager* CVC3::TheoremManager::d_em [private]

Definition at line 42 of file theorem_manager.h.

Referenced by getEM(), and TheoremManager().

const CLFlags& CVC3::TheoremManager::d_flags [private]

Definition at line 43 of file theorem_manager.h.

Referenced by getFlags().

MemoryManager* CVC3::TheoremManager::d_mm [private]

Definition at line 44 of file theorem_manager.h.

Referenced by getMM(), TheoremManager(), and ~TheoremManager().

MemoryManager* CVC3::TheoremManager::d_rwmm [private]

Definition at line 45 of file theorem_manager.h.

Referenced by getRWMM(), TheoremManager(), and ~TheoremManager().

bool CVC3::TheoremManager::d_withProof [private]

Definition at line 46 of file theorem_manager.h.

Referenced by TheoremManager(), and withProof().

bool CVC3::TheoremManager::d_withAssump [private]

Definition at line 47 of file theorem_manager.h.

Referenced by TheoremManager(), and withAssumptions().

unsigned CVC3::TheoremManager::d_flag [private]

Definition at line 48 of file theorem_manager.h.

Referenced by clearAllFlags(), and getFlag().

bool CVC3::TheoremManager::d_active [private]

Whether TheoremManager is active. See also clear()

Definition at line 49 of file theorem_manager.h.

Referenced by clear(), and isActive().

CommonProofRules* CVC3::TheoremManager::d_rules [private]

Definition at line 50 of file theorem_manager.h.

Referenced by clear(), getRules(), and TheoremManager().

std::hash_map<long, bool> CVC3::TheoremManager::d_reflFlags [private]

Definition at line 52 of file theorem_manager.h.

Referenced by clearAllFlags(), isFlagged(), and setFlag().

std::hash_map<long, int> CVC3::TheoremManager::d_cachedValues [private]

Definition at line 53 of file theorem_manager.h.

Referenced by getCachedValue(), and setCachedValue().

std::hash_map<long, bool> CVC3::TheoremManager::d_expandFlags [private]

Definition at line 54 of file theorem_manager.h.

Referenced by getExpandFlag(), and setExpandFlag().

std::hash_map<long, bool> CVC3::TheoremManager::d_litFlags [private]

Definition at line 55 of file theorem_manager.h.

Referenced by getLitFlag(), and setLitFlag().

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

CVC3::TheoremManager Class Reference

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation