CVC3
Public Member Functions | Private Member Functions | Private Attributes

CVC3::TheoremManager Class Reference

#include <theorem_manager.h>

Collaboration diagram for CVC3::TheoremManager:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


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

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.

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.

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.

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.

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

Member Data Documentation

Definition at line 41 of file theorem_manager.h.

Referenced by getCM().

Definition at line 42 of file theorem_manager.h.

Referenced by getEM(), and TheoremManager().

Definition at line 43 of file theorem_manager.h.

Referenced by getFlags().

Definition at line 44 of file theorem_manager.h.

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

Definition at line 45 of file theorem_manager.h.

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

Definition at line 46 of file theorem_manager.h.

Referenced by TheoremManager(), and withProof().

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

Whether TheoremManager is active. See also clear()

Definition at line 49 of file theorem_manager.h.

Referenced by clear(), and isActive().

Definition at line 50 of file theorem_manager.h.

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

Definition at line 52 of file theorem_manager.h.

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

Definition at line 53 of file theorem_manager.h.

Referenced by getCachedValue(), and setCachedValue().

Definition at line 54 of file theorem_manager.h.

Referenced by getExpandFlag(), and setExpandFlag().

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: