CVCL::TheoremManager Class Reference

#include <theorem_manager.h>

Collaboration diagram for CVCL::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
• MemoryManager * getReflMM () const
• CommonProofRules * getRules () const
• unsigned getFlag () const
• void clearAllFlags ()
• bool withProof ()
• bool withAssumptions ()

Private Member Functions

• CommonProofRules * createProofRules ()

Private Attributes

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

  Whether TheoremManager is active. See also clear().
  

• CommonProofRules * d_rules

---

Detailed Description

Definition at line 46 of file theorem_manager.h.

---

Constructor & Destructor Documentation

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

Constructor. Definition at line 54 of file theorem_manager.cpp. References createProofRules(), d_em, d_mm, d_reflmm, d_rules, d_rwmm, d_withAssump, d_withProof, CVCL::ExprManager::newKind(), CVCL::PF_APPLY, and CVCL::PF_HOLE.

TheoremManager::~TheoremManager (   )

Destructor. Definition at line 79 of file theorem_manager.cpp. References d_mm, d_reflmm, and d_rwmm.

---

Member Function Documentation

CommonProofRules * TheoremManager::createProofRules (   )  [private]

Definition at line 43 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 87 of file theorem_manager.cpp. References d_active, and d_rules.

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

Test whether the TheoremManager is still active. Definition at line 76 of file theorem_manager.h. References d_active. Referenced by CVCL::TheoremValue::TheoremValue().

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

Definition at line 78 of file theorem_manager.h. References d_cm. Referenced by CVCL::TheoremValue::TheoremValue().

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

Definition at line 79 of file theorem_manager.h. References d_em. Referenced by CVCL::RefinedArithTheoremProducer::addAssoc(), CVCL::RefinedArithTheoremProducer::addInvR(), CVCL::RefinedArithTheoremProducer::addLID(), CVCL::RefinedArithTheoremProducer::addSymm(), CVCL::RefinedArithTheoremProducer::distribL(), CVCL::RefinedArithTheoremProducer::divideDef(), CVCL::RefinedArithTheoremProducer::ltAddR(), CVCL::RefinedArithTheoremProducer::ltScale(), CVCL::RefinedArithTheoremProducer::ltTrans(), CVCL::RefinedArithTheoremProducer::minusDef(), CVCL::RefinedArithTheoremProducer::multAssoc(), CVCL::RefinedArithTheoremProducer::multInvR(), CVCL::RefinedArithTheoremProducer::multLID(), CVCL::RefinedArithTheoremProducer::multSymm(), CVCL::RefinedArithTheoremProducer::multZeroL(), CVCL::TheoremProducer::newLabel(), and CVCL::TheoremProducer::newPf().

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

Definition at line 80 of file theorem_manager.h. References d_flags.

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

Definition at line 81 of file theorem_manager.h. References d_mm. Referenced by CVCL::TheoremValue::getMM(), and CVCL::Theorem::Theorem().

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

Definition at line 82 of file theorem_manager.h. References d_rwmm. Referenced by CVCL::RWTheoremValue::getMM(), and CVCL::Theorem::Theorem().

MemoryManager* CVCL::TheoremManager::getReflMM (   )  const [inline]

Definition at line 83 of file theorem_manager.h. References d_reflmm. Referenced by CVCL::ReflexivityTheoremValue::getMM(), and CVCL::Theorem::Theorem().

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

Definition at line 84 of file theorem_manager.h. References d_rules. Referenced by d_coreSatAPI().

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

Definition at line 86 of file theorem_manager.h. References d_flag. Referenced by CVCL::TheoremValue::isFlagged(), and CVCL::TheoremValue::setFlag().

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

Definition at line 90 of file theorem_manager.h. References d_flag. Referenced by CVCL::TheoremValue::clearAllFlags().

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

Definition at line 94 of file theorem_manager.h. References d_withProof. Referenced by CVCL::SearchImplBase::getProof(), CVCL::TheoremProducer::withProof(), and CVCL::Theorem::withProof().

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

Definition at line 97 of file theorem_manager.h. References d_withAssump. Referenced by CVCL::SearchImplBase::getAssumptionsUsed(), CVCL::TheoremProducer::withAssumptions(), and CVCL::Theorem::withAssumptions().

---

Member Data Documentation

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

Definition at line 48 of file theorem_manager.h. Referenced by getCM().

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

Definition at line 49 of file theorem_manager.h. Referenced by getEM(), and TheoremManager().

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

Definition at line 50 of file theorem_manager.h. Referenced by getFlags().

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

Definition at line 51 of file theorem_manager.h. Referenced by getMM(), TheoremManager(), and ~TheoremManager().

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

Definition at line 52 of file theorem_manager.h. Referenced by getRWMM(), TheoremManager(), and ~TheoremManager().

MemoryManager* CVCL::TheoremManager::d_reflmm [private]

Definition at line 53 of file theorem_manager.h. Referenced by getReflMM(), TheoremManager(), and ~TheoremManager().

bool CVCL::TheoremManager::d_withProof [private]

Definition at line 54 of file theorem_manager.h. Referenced by TheoremManager(), and withProof().

bool CVCL::TheoremManager::d_withAssump [private]

Definition at line 55 of file theorem_manager.h. Referenced by TheoremManager(), and withAssumptions().

unsigned CVCL::TheoremManager::d_flag [private]

Definition at line 56 of file theorem_manager.h. Referenced by clearAllFlags(), and getFlag().

bool CVCL::TheoremManager::d_active [private]

Whether TheoremManager is active. See also clear(). Definition at line 57 of file theorem_manager.h. Referenced by clear(), and isActive().

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

Definition at line 58 of file theorem_manager.h. Referenced by clear(), getRules(), and TheoremManager().

---

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

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

---