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. | |
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) |
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) | |
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) |
|
inlineprivatevirtual |
|
inlineprivatevirtual |
|
inlineprivatevirtual |
|
inline |
Definition at line 63 of file cdo.h.
Referenced by CVC3::SearchSimple::addNonLiteralFact(), CVC3::SearchSimple::checkValidInternal(), CVC3::TheoryQuant::collectChangedTerms(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryQuant::saveContext(), CVC3::SearchSimple::SearchSimple(), CVC3::VariableValue::setAssumpThm(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), and CVC3::VariableValue::setValue().
|
inline |
Definition at line 64 of file cdo.h.
Referenced by CVC3::SearchSimple::addNonLiteralFact(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::VariableValue::getAntecedent(), CVC3::VariableValue::getAntecedentIdx(), CVC3::VariableValue::getAssumpThm(), CVC3::SearchSat::getCounterExample(), CVC3::Expr::getEqNext(), CVC3::Expr::getFind(), CVC3::SearchSat::getProof(), CVC3::Expr::getRep(), CVC3::VariableValue::getScope(), CVC3::Expr::getSig(), CVC3::VariableValue::getTheorem(), CVC3::VariableValue::getValue(), CVC3::Expr::hasFind(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::TheoryQuant::naiveCheckSat(), SAT::CD_CNF_Formula::numVars(), CVC3::SearchSimple::restartInternal(), and CVC3::SearchEngineFast::restartInternal().
|
private |
Definition at line 40 of file cdo.h.
Referenced by CVC3::CDO< Rational >::get(), CVC3::CDO< Rational >::restoreData(), CVC3::CDO< Rational >::set(), and CVC3::CDO< Rational >::setNull().