CVC3
2.4.1
|
#include <cdflags.h>
Public Member Functions | |
CDFlags (Context *context) | |
~CDFlags () | |
void | set (unsigned mask, int scope=-1) |
void | clear (unsigned mask, int scope=-1) |
bool | get (unsigned mask) const |
![]() | |
ContextObj (Context *context) | |
Create a new ContextObj. | |
virtual | ~ContextObj () |
int | level () const |
bool | isCurrent (int scope=-1) const |
void | makeCurrent (int scope=-1) |
void * | operator new (size_t size, MemoryManager *mm) |
void | operator delete (void *pMem, MemoryManager *mm) |
void * | operator new (size_t size, bool b) |
void | operator delete (void *pMem, bool b) |
void | operator delete (void *) |
Private Member Functions | |
virtual ContextObj * | makeCopy (ContextMemoryManager *cmm) |
virtual void | restoreData (ContextObj *data) |
virtual void | setNull (void) |
void | update (unsigned mask, int scope, bool setMask) |
CDFlags (const CDFlags &cdflags) | |
CDFlags & | operator= (const CDFlags &cdflags) |
Private Attributes | |
unsigned | d_flags |
Additional Inherited Members | |
![]() | |
ContextObj (const ContextObj &co) | |
Copy constructor (defined mainly for debugging purposes) | |
ContextObj & | operator= (const ContextObj &co) |
Assignment operator (defined mainly for debugging purposes) | |
virtual ContextObj * | makeCopy (ContextMemoryManager *cmm)=0 |
Make a copy of the current object so it can be restored to its current state. | |
virtual void | restoreData (ContextObj *data) |
Restore the current object from the given data. | |
const ContextObj * | getRestore () |
virtual void | setNull (void)=0 |
Set the current object to be invalid. | |
ContextMemoryManager * | getCMM () |
Return our name (for debugging) |
|
inlineprivate |
|
inline |
|
inlineprivatevirtual |
|
inlineprivatevirtual |
|
inlineprivatevirtual |
Definition at line 44 of file cdflags.h.
References FatalAssert.
|
private |
Definition at line 31 of file cdflags.cpp.
References CVC3::Scope::addToChain(), d_flags, CVC3::ContextObjChain::d_restore, CVC3::ContextObj::d_restore, DebugAssert, CVC3::Scope::getCMM(), IF_DEBUG, CVC3::Scope::level(), CVC3::ContextObj::level(), makeCopy(), and CVC3::Scope::prevScope().
|
inline |
Definition at line 57 of file cdflags.h.
Referenced by CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setFinite(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Expr::setNotArrayNormalized(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTerminalsConstFlag(), CVC3::Expr::setTranslated(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setUsesCC(), CVC3::Expr::setValidType(), and CVC3::Expr::setWellFounded().
|
inline |
Definition at line 58 of file cdflags.h.
Referenced by CVC3::Expr::clearRewriteNormal(), CVC3::Expr::setIsAtomicFlag(), and CVC3::Expr::setTerminalsConstFlag().
|
inline |
Definition at line 59 of file cdflags.h.
Referenced by CVC3::Expr::computeTransClosure(), CVC3::Expr::containsBoundVar(), CVC3::Expr::getIsAtomicFlag(), CVC3::Expr::getTerminalsConstFlag(), CVC3::Expr::inUserAssumption(), CVC3::Expr::isFinite(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isIntAssumption(), CVC3::Expr::isJustified(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isRewriteNormal(), CVC3::Expr::isSelected(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isTranslated(), CVC3::Expr::isUserAssumption(), CVC3::Expr::isUserRegisteredAtom(), CVC3::Expr::isValidType(), CVC3::Expr::isWellFounded(), CVC3::Expr::notArrayNormalized(), CVC3::Expr::usesCC(), CVC3::Expr::validIsAtomicFlag(), and CVC3::Expr::validTerminalsConstFlag().
|
private |
Definition at line 38 of file cdflags.h.
Referenced by restoreData(), and update().