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 
)

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:
Generated on Wed Nov 18 16:16:03 2009 for CVC3 by  doxygen 1.5.2