|
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) |
Public Member Functions inherited from CVC3::ContextObj | |
| 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 | |
Protected Member Functions inherited from CVC3::ContextObj | |
| 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::CDO< bool >::CDO(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::CDO< bool >::operator=(), 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().
1.8.7