#include <theorem_manager.h>
Collaboration diagram for CVCL::TheoremManager:
Definition at line 46 of file theorem_manager.h.

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. 

Destructor.
Definition at line 79 of file theorem_manager.cpp. 

Definition at line 43 of file common_theorem_producer.cpp. Referenced by TheoremManager(). 

Deactivate TheoremManager. No more Theorems can be created after this call, only deleted. The purpose of this call is to disentangle the mutual dependency of ExprManager and TheoremManager during destruction time. Definition at line 87 of file theorem_manager.cpp. 

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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