CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::TheoremManager Class Reference

#include <theorem_manager.h>

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.
ContextManagergetCM () const
ExprManagergetEM () const
const CLFlagsgetFlags () const
MemoryManagergetMM () const
MemoryManagergetRWMM () const
CommonProofRulesgetRules () 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

CommonProofRulescreateProofRules ()

Private Attributes

ContextManagerd_cm
ExprManagerd_em
const CLFlagsd_flags
MemoryManagerd_mm
MemoryManagerd_rwmm
bool d_withProof
bool d_withAssump
unsigned d_flag
bool d_active
 Whether TheoremManager is active. See also clear()
CommonProofRulesd_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 
)
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.

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
const CLFlags& CVC3::TheoremManager::getFlags ( ) const
inline
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
bool CVC3::TheoremManager::withProof ( )
inline
bool CVC3::TheoremManager::withAssumptions ( )
inline
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
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
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
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

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: