CVC3::TheoremManager Class Reference

#include <theorem_manager.h>

Collaboration diagram for CVC3::TheoremManager:

[legend]

List of all members.

Public Member Functions

• TheoremManager (ContextManager *cm, ExprManager *em, const CLFlags &flags)

  Constructor.
  

• ~TheoremManager ()

  Destructor.
  

• void clear ()

  Deactivate TheoremManager.
  

• bool isActive ()

  Test whether the TheoremManager is still active.
  

• ContextManager * getCM () const
• ExprManager * getEM () const
• const CLFlags & getFlags () const
• MemoryManager * getMM () const
• MemoryManager * getRWMM () const
• CommonProofRules * getRules () const
• unsigned getFlag () const
• void clearAllFlags ()
• bool withProof ()
• bool withAssumptions ()
• void setFlag (long ptr)
• bool isFlagged (long ptr)
• void setCachedValue (long ptr, int value)
• int getCachedValue (long ptr)
• void setExpandFlag (long ptr, bool value)
• bool getExpandFlag (long ptr)
• void setLitFlag (long ptr, bool value)
• bool getLitFlag (long ptr)

Private Member Functions

• CommonProofRules * createProofRules ()

Private Attributes

• ContextManager * d_cm
• ExprManager * d_em
• const CLFlags & d_flags
• MemoryManager * d_mm
• MemoryManager * d_rwmm
• bool d_withProof
• bool d_withAssump
• unsigned d_flag
• bool d_active

  Whether TheoremManager is active. See also clear().
  

• CommonProofRules * d_rules
• std::hash_map< long, bool > d_reflFlags
• std::hash_map< long, int > d_cachedValues
• std::hash_map< long, bool > d_expandFlags
• std::hash_map< long, bool > d_litFlags

---

Detailed Description

Definition at line 39 of file theorem_manager.h.

---

Constructor & Destructor Documentation

TheoremManager::TheoremManager	(	ContextManager *	cm,
		ExprManager *	em,
		const CLFlags &	flags
	)

Constructor.

Definition at line 46 of file theorem_manager.cpp.

References createProofRules(), d_em, d_mm, d_rules, d_rwmm, d_withAssump, d_withProof, DebugAssert, CVC3::ExprManager::newKind(), CVC3::PF_APPLY, and CVC3::PF_HOLE.

TheoremManager::~TheoremManager

(

)

Destructor.

Definition at line 69 of file theorem_manager.cpp.

References d_mm, and d_rwmm.

---

Member Function Documentation

CommonProofRules * TheoremManager::createProofRules

(

)

[private]

Definition at line 35 of file common_theorem_producer.cpp.

Referenced by TheoremManager().

void TheoremManager::clear

(

)

Deactivate TheoremManager.

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.

Referenced by CVC3::VCL::destroy().

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.

MemoryManager* CVC3::TheoremManager::getMM

(

)

const [inline]

Definition at line 78 of file theorem_manager.h.

References d_mm.

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

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(), and CVC3::Theorem::clearAllFlags().

bool CVC3::TheoremManager::withProof

(

)

[inline]

Definition at line 91 of file theorem_manager.h.

References d_withProof.

Referenced by CVC3::SearchSat::check(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), CVC3::SearchSat::SearchSat(), CVC3::TheoremProducer::withProof(), and CVC3::Theorem::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(), CVC3::TheoremProducer::withAssumptions(), and CVC3::Theorem::withAssumptions().

void CVC3::TheoremManager::setFlag

(

long

ptr

)

[inline]

Definition at line 99 of file theorem_manager.h.

References d_reflFlags.

Referenced by CVC3::Theorem::setFlag().

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.

Referenced by CVC3::Theorem::isFlagged().

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

Definition at line 101 of file theorem_manager.h.

References d_cachedValues.

Referenced by CVC3::Theorem::setCachedValue().

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().

Referenced by CVC3::Theorem::getCachedValue().

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

Definition at line 107 of file theorem_manager.h.

References d_expandFlags.

Referenced by CVC3::Theorem::setExpandFlag().

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().

Referenced by CVC3::Theorem::getExpandFlag().

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

Definition at line 113 of file theorem_manager.h.

References d_litFlags.

Referenced by CVC3::Theorem::setLitFlag().

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().

Referenced by CVC3::Theorem::getLitFlag().

---

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:

• theorem_manager.h
• common_theorem_producer.cpp
• theorem_manager.cpp