CVC3
2.4.1
|
#include <theorem_manager.h>
TheoremManager::TheoremManager | ( | ContextManager * | cm, |
ExprManager * | em, | ||
const CLFlags & | flags | ||
) |
Constructor.
Definition at line 46 of file theorem_manager.cpp.
References d_em, CVC3::ExprManager::newKind(), PF_APPLY, PF_HOLE, DebugAssert, d_withProof, d_withAssump, d_mm, d_rwmm, d_rules, and createProofRules().
TheoremManager::~TheoremManager | ( | ) |
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.
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::RegTheoremValue::RegTheoremValue(), and CVC3::RWTheoremValue::init().
ContextManager* CVC3::TheoremManager::getCM | ( | ) | const [inline] |
Definition at line 75 of file theorem_manager.h.
References d_cm.
Referenced by CVC3::RegTheoremValue::RegTheoremValue(), and CVC3::RWTheoremValue::init().
ExprManager* CVC3::TheoremManager::getEM | ( | ) | const [inline] |
Definition at line 76 of file theorem_manager.h.
References d_em.
Referenced by CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::TheoremProducer::newLabel(), and CVC3::TheoremProducer::newPf().
const CLFlags& CVC3::TheoremManager::getFlags | ( | ) | const [inline] |
Definition at line 77 of file theorem_manager.h.
References d_flags.
Referenced by CVC3::SearchEngine::SearchEngine(), CVC3::SearchEngineTheoremProducer::satProof(), and CVC3::TheoremProducer::newLabel().
MemoryManager* CVC3::TheoremManager::getMM | ( | ) | const [inline] |
Definition at line 78 of file theorem_manager.h.
References d_mm.
Referenced by CVC3::Theorem::Theorem(), and CVC3::RegTheoremValue::getMM().
MemoryManager* CVC3::TheoremManager::getRWMM | ( | ) | const [inline] |
Definition at line 79 of file theorem_manager.h.
References d_rwmm.
Referenced by CVC3::Theorem::Theorem(), and CVC3::RWTheoremValue::getMM().
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 d_reflFlags, Hash::hash_map::clear(), FatalAssert, and d_flag.
Referenced by CVC3::Theorem::clearAllFlags(), and CVC3::TheoremValue::clearAllFlags().
bool CVC3::TheoremManager::withProof | ( | ) | [inline] |
Definition at line 91 of file theorem_manager.h.
References d_withProof.
Referenced by CVC3::SearchImplBase::getProof(), CVC3::SearchSat::SearchSat(), CVC3::SearchSat::getProof(), CVC3::Theorem::withProof(), and CVC3::TheoremProducer::withProof().
bool CVC3::TheoremManager::withAssumptions | ( | ) | [inline] |
Definition at line 94 of file theorem_manager.h.
References d_withAssump.
Referenced by CVC3::SearchImplBase::getCounterExample(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::Theorem::withAssumptions(), and CVC3::TheoremProducer::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 d_reflFlags, and Hash::hash_map::count().
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::find(), and Hash::hash_map::end().
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::find(), and Hash::hash_map::end().
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::find(), and Hash::hash_map::end().
Referenced by CVC3::Theorem::getLitFlag().
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 TheoremManager(), and getEM().
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 TheoremManager(), ~TheoremManager(), and getMM().
MemoryManager* CVC3::TheoremManager::d_rwmm [private] |
Definition at line 45 of file theorem_manager.h.
Referenced by TheoremManager(), ~TheoremManager(), and getRWMM().
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 getFlag(), and clearAllFlags().
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 TheoremManager(), clear(), and getRules().
std::hash_map<long, bool> CVC3::TheoremManager::d_reflFlags [private] |
Definition at line 52 of file theorem_manager.h.
Referenced by clearAllFlags(), setFlag(), and isFlagged().
std::hash_map<long, int> CVC3::TheoremManager::d_cachedValues [private] |
Definition at line 53 of file theorem_manager.h.
Referenced by setCachedValue(), and getCachedValue().
std::hash_map<long, bool> CVC3::TheoremManager::d_expandFlags [private] |
Definition at line 54 of file theorem_manager.h.
Referenced by setExpandFlag(), and getExpandFlag().
std::hash_map<long, bool> CVC3::TheoremManager::d_litFlags [private] |
Definition at line 55 of file theorem_manager.h.
Referenced by setLitFlag(), and getLitFlag().