CVCL::TheoremManager Class Reference

#include <theorem_manager.h>

Collaboration diagram for CVCL::TheoremManager:

Collaboration graph
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Definition at line 46 of file theorem_manager.h.

Constructor & Destructor Documentation

TheoremManager::TheoremManager ContextManager cm,
ExprManager em,
const CLFlags flags


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  ) 


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:
Generated on Thu Apr 13 16:57:44 2006 for CVC Lite by  doxygen 1.4.4