CVC3
2.4.1
|
#include <theorem_manager.h>
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 |
CommonProofRules * | getRules () const |
unsigned | getFlag () const |
void | clearAllFlags () |
bool | withProof () |
bool | withAssumptions () |
void | setFlag (long ptr) |
bool | isFlagged (long ptr) |
void | setCachedValue (long ptr, int value) |
int | getCachedValue (long ptr) |
void | setExpandFlag (long ptr, bool value) |
bool | getExpandFlag (long ptr) |
void | setLitFlag (long ptr, bool value) |
bool | getLitFlag (long ptr) |
Private Member Functions | |
CommonProofRules * | createProofRules () |
Private Attributes | |
ContextManager * | d_cm |
ExprManager * | d_em |
const CLFlags & | d_flags |
MemoryManager * | d_mm |
MemoryManager * | d_rwmm |
bool | d_withProof |
bool | d_withAssump |
unsigned | d_flag |
bool | d_active |
Whether TheoremManager is active. See also clear() | |
CommonProofRules * | d_rules |
std::hash_map< long, bool > | d_reflFlags |
std::hash_map< long, int > | d_cachedValues |
std::hash_map< long, bool > | d_expandFlags |
std::hash_map< long, bool > | d_litFlags |
Definition at line 39 of file theorem_manager.h.
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(), PF_APPLY, and PF_HOLE.
TheoremManager::~TheoremManager | ( | ) |
|
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.
|
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().
|
inline |
Definition at line 75 of file theorem_manager.h.
References d_cm.
Referenced by CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().
|
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().
|
inline |
Definition at line 77 of file theorem_manager.h.
References d_flags.
Referenced by CVC3::TheoremProducer::newLabel(), CVC3::SearchEngineTheoremProducer::satProof(), and CVC3::SearchEngine::SearchEngine().
|
inline |
Definition at line 78 of file theorem_manager.h.
References d_mm.
Referenced by CVC3::RegTheoremValue::getMM(), and CVC3::Theorem::Theorem().
|
inline |
Definition at line 79 of file theorem_manager.h.
References d_rwmm.
Referenced by CVC3::RWTheoremValue::getMM(), and CVC3::Theorem::Theorem().
|
inline |
Definition at line 80 of file theorem_manager.h.
References d_rules.
Referenced by CVC3::TheoryCore::TheoryCore().
|
inline |
Definition at line 82 of file theorem_manager.h.
References d_flag.
Referenced by CVC3::TheoremValue::isFlagged(), and CVC3::TheoremValue::setFlag().
|
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().
|
inline |
Definition at line 91 of file theorem_manager.h.
References d_withProof.
Referenced by CVC3::SearchImplBase::getProof(), CVC3::SearchSat::getProof(), CVC3::SearchSat::SearchSat(), CVC3::TheoremProducer::withProof(), and CVC3::Theorem::withProof().
|
inline |
Definition at line 94 of file theorem_manager.h.
References d_withAssump.
Referenced by CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchImplBase::getCounterExample(), CVC3::Theorem::withAssumptions(), and CVC3::TheoremProducer::withAssumptions().
|
inline |
Definition at line 99 of file theorem_manager.h.
References d_reflFlags.
Referenced by CVC3::Theorem::setFlag().
|
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().
|
inline |
Definition at line 101 of file theorem_manager.h.
References d_cachedValues.
Referenced by CVC3::Theorem::setCachedValue().
|
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().
|
inline |
Definition at line 107 of file theorem_manager.h.
References d_expandFlags.
Referenced by CVC3::Theorem::setExpandFlag().
|
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().
|
inline |
Definition at line 113 of file theorem_manager.h.
References d_litFlags.
Referenced by CVC3::Theorem::setLitFlag().
|
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().
|
private |
Definition at line 41 of file theorem_manager.h.
Referenced by getCM().
|
private |
Definition at line 42 of file theorem_manager.h.
Referenced by getEM(), and TheoremManager().
|
private |
Definition at line 43 of file theorem_manager.h.
Referenced by getFlags().
|
private |
Definition at line 44 of file theorem_manager.h.
Referenced by getMM(), TheoremManager(), and ~TheoremManager().
|
private |
Definition at line 45 of file theorem_manager.h.
Referenced by getRWMM(), TheoremManager(), and ~TheoremManager().
|
private |
Definition at line 46 of file theorem_manager.h.
Referenced by TheoremManager(), and withProof().
|
private |
Definition at line 47 of file theorem_manager.h.
Referenced by TheoremManager(), and withAssumptions().
|
private |
Definition at line 48 of file theorem_manager.h.
Referenced by clearAllFlags(), and getFlag().
|
private |
Whether TheoremManager is active. See also clear()
Definition at line 49 of file theorem_manager.h.
Referenced by clear(), and isActive().
|
private |
Definition at line 50 of file theorem_manager.h.
Referenced by clear(), getRules(), and TheoremManager().
|
private |
Definition at line 52 of file theorem_manager.h.
Referenced by clearAllFlags(), isFlagged(), and setFlag().
|
private |
Definition at line 53 of file theorem_manager.h.
Referenced by getCachedValue(), and setCachedValue().
|
private |
Definition at line 54 of file theorem_manager.h.
Referenced by getExpandFlag(), and setExpandFlag().
|
private |
Definition at line 55 of file theorem_manager.h.
Referenced by getLitFlag(), and setLitFlag().