25 #ifndef _cvc3__theorem_manager_h_
26 #define _cvc3__theorem_manager_h_
37 class CommonProofRules;
std::hash_map< long, int > d_cachedValues
size_type count(const _Key &key) const
Description: Collection of debugging macros and functions.
ExprManager * getEM() const
std::hash_map< long, bool > d_reflFlags
TheoremManager(ContextManager *cm, ExprManager *em, const CLFlags &flags)
Constructor.
CommonProofRules * d_rules
MemoryManager * getMM() const
~TheoremManager()
Destructor.
iterator find(const key_type &key)
operations
int getCachedValue(long ptr)
bool d_active
Whether TheoremManager is active. See also clear()
CommonProofRules * createProofRules()
ContextManager * getCM() const
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
CommonProofRules * getRules() const
MemoryManager * getRWMM() const
std::hash_map< long, bool > d_expandFlags
void setExpandFlag(long ptr, bool value)
bool getLitFlag(long ptr)
void clear()
Deactivate TheoremManager.
void setCachedValue(long ptr, int value)
bool getExpandFlag(long ptr)
const CLFlags & getFlags() const
Manager for multiple contexts. Also holds current context.
bool isActive()
Test whether the TheoremManager is still active.
void setLitFlag(long ptr, bool value)
std::hash_map< long, bool > d_litFlags