CVC3
2.4.1
|
#include <cdo.h>
Public Member Functions | |
CDO (Context *context) | |
CDO (Context *context, const T &data, int scope=-1) | |
~CDO () | |
void | set (const T &data, int scope=-1) |
const T & | get () const |
operator T () | |
CDO< T > & | operator= (const T &data) |
![]() | |
ContextObj (Context *context) | |
Create a new ContextObj. More... | |
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) |
Make a copy of the current object so it can be restored to its current state. More... | |
virtual void | restoreData (ContextObj *data) |
Restore the current object from the given data. More... | |
virtual void | setNull (void) |
Set the current object to be invalid. More... | |
CDO (const CDO< T > &cdo) | |
CDO< T > & | operator= (const CDO< T > &cdo) |
Private Attributes | |
T | d_data |
Additional Inherited Members | |
![]() | |
ContextObj (const ContextObj &co) | |
Copy constructor (defined mainly for debugging purposes) More... | |
ContextObj & | operator= (const ContextObj &co) |
Assignment operator (defined mainly for debugging purposes) More... | |
const ContextObj * | getRestore () |
ContextMemoryManager * | getCMM () |
Return our name (for debugging) More... | |
|
inlineprivatevirtual |
Make a copy of the current object so it can be restored to its current state.
Implements CVC3::ContextObj.
|
inlineprivatevirtual |
Restore the current object from the given data.
Reimplemented from CVC3::ContextObj.
|
inlineprivatevirtual |
Set the current object to be invalid.
Implements CVC3::ContextObj.
|
inline |
Definition at line 63 of file cdo.h.
Referenced by CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryQuant::saveContext(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), and CVC3::VariableValue::setValue().
|
inline |
Definition at line 64 of file cdo.h.
Referenced by CVC3::VariableValue::getAntecedentIdx(), CVC3::VariableValue::getScope(), CVC3::VariableValue::getValue(), CVC3::TheoryQuant::naiveCheckSat(), and SAT::CD_CNF_Formula::numVars().
|
private |
Definition at line 40 of file cdo.h.
Referenced by CVC3::CDO< bool >::get(), CVC3::CDO< bool >::restoreData(), CVC3::CDO< bool >::set(), and CVC3::CDO< bool >::setNull().