CVC3
2.4.1
|
#include <context.h>
Public Member Functions | |
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 *) |
Protected Member Functions | |
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... | |
virtual ContextObj * | makeCopy (ContextMemoryManager *cmm)=0 |
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... | |
const ContextObj * | getRestore () |
virtual void | setNull (void)=0 |
Set the current object to be invalid. More... | |
ContextMemoryManager * | getCMM () |
Return our name (for debugging) More... | |
Private Member Functions | |
void | update (int scope=-1) |
Update on the given scope, on the current scope if 'scope' == -1. More... | |
Private Attributes | |
Scope * | d_scope |
Last scope in which this object was modified. More... | |
ContextObjChain * | d_restore |
The list of values on previous scopes; our destructor should clean up those. More... | |
Friends | |
class | Scope |
class | ContextObjChain |
class | CDFlags |
Description: This is a generic class from which all objects that are context-dependent should inherit. Subclasses need to implement makeCopy, restoreData, and setNull.
|
inlineprotected |
Copy constructor (defined mainly for debugging purposes)
Definition at line 220 of file context.h.
References DebugAssert, and IF_DEBUG.
|
virtual |
Definition at line 179 of file context.cpp.
References CVC3::ContextObjChain::d_master, CVC3::ContextObjChain::d_restore, CVC3::ContextObjChain::d_restoreChainNext, CVC3::ContextObjChain::d_restoreChainPrev, FatalAssert, and IF_DEBUG.
|
private |
Update on the given scope, on the current scope if 'scope' == -1.
Definition at line 153 of file context.cpp.
References d_restore, d_scope, DebugAssert, IF_DEBUG, and CVC3::int2string().
|
inlineprotected |
Assignment operator (defined mainly for debugging purposes)
Definition at line 229 of file context.h.
References DebugAssert.
|
protectedpure virtual |
Make a copy of the current object so it can be restored to its current state.
Implemented in CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDMapOrdered< Key, Data >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArith3::FreeConst >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr > >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArith3::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst >, CVC3::CDMap< CVC3::Expr, CVC3::Rational, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo >, CVC3::CDMap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > *, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Literal >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned > >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational >, CVC3::CDMap< CVC3::Expr, int, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > * >, CVC3::CDMap< CVC3::Expr, std::set< std::vector< CVC3::Expr > >, HashFcn >, CVC3::CDMap< CVC3::Expr, std::set< std::vector< CVC3::Expr > > >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational, HashFcn >, CVC3::CDMap< CVC3::Expr, bool >, CVC3::CDMap< CVC3::Expr, CVC3::Literal, HashFcn >, CVC3::CDMap< CVC3::Expr, bool, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Rational >, CVC3::CDMap< CVC3::Expr, CVC3::Expr >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< CVC3::Expr, int >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArith3::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Rational, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > *, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< CVC3::Expr, int, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Theorem, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::set< std::vector< CVC3::Expr > >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Literal, HashFcn >, CVC3::CDOmap< CVC3::Expr, bool, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDList< T >, CVC3::CDList< CVC3::TheoryArithOld::Ineq >, CVC3::CDList< std::vector< CVC3::Expr > >, CVC3::CDList< CVC3::SmartCDO< CVC3::Theorem > >, CVC3::CDList< CVC3::Theory * >, CVC3::CDList< SAT::Clause >, CVC3::CDList< CVC3::SearchImplBase::Splitter >, CVC3::CDList< CVC3::ClauseOwner >, CVC3::CDList< ProcessKinds >, CVC3::CDList< Expr >, CVC3::CDList< CVC3::Expr >, CVC3::CDList< CVC3::Theorem >, CVC3::CDList< size_t >, CVC3::CDList< CVC3::Trigger >, CVC3::CDList< CVC3::dynTrig >, CVC3::CDList< CVC3::Literal >, CVC3::CDList< CVC3::TheoryArithNew::Ineq >, CVC3::CDList< CVC3::TheoryArith3::Ineq >, CVC3::CDO< T >, CVC3::CDO< CVC3::Clause >, CVC3::CDO< int >, CVC3::CDO< CVC3::Rational >, CVC3::CDO< unsigned int >, CVC3::CDO< CVC3::Unsigned >, CVC3::CDO< U >, CVC3::CDO< CVC3::Expr >, CVC3::CDO< CVC3::Theorem >, CVC3::CDO< QueryResult >, CVC3::CDO< std::set< CVC3::SearchSat::LitPriorityPair >::const_iterator >, CVC3::CDO< size_t >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDFlags.
|
inlineprotectedvirtual |
Restore the current object from the given data.
Reimplemented in CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDMapOrdered< Key, Data >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArith3::FreeConst >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr > >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArith3::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst >, CVC3::CDMap< CVC3::Expr, CVC3::Rational, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo >, CVC3::CDMap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > *, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Literal >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned > >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational >, CVC3::CDMap< CVC3::Expr, int, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > * >, CVC3::CDMap< CVC3::Expr, std::set< std::vector< CVC3::Expr > >, HashFcn >, CVC3::CDMap< CVC3::Expr, std::set< std::vector< CVC3::Expr > > >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational, HashFcn >, CVC3::CDMap< CVC3::Expr, bool >, CVC3::CDMap< CVC3::Expr, CVC3::Literal, HashFcn >, CVC3::CDMap< CVC3::Expr, bool, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Rational >, CVC3::CDMap< CVC3::Expr, CVC3::Expr >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< CVC3::Expr, int >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArith3::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Rational, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > *, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< CVC3::Expr, int, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Theorem, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::set< std::vector< CVC3::Expr > >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Literal, HashFcn >, CVC3::CDOmap< CVC3::Expr, bool, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDList< T >, CVC3::CDList< CVC3::TheoryArithOld::Ineq >, CVC3::CDList< std::vector< CVC3::Expr > >, CVC3::CDList< CVC3::SmartCDO< CVC3::Theorem > >, CVC3::CDList< CVC3::Theory * >, CVC3::CDList< SAT::Clause >, CVC3::CDList< CVC3::SearchImplBase::Splitter >, CVC3::CDList< CVC3::ClauseOwner >, CVC3::CDList< ProcessKinds >, CVC3::CDList< Expr >, CVC3::CDList< CVC3::Expr >, CVC3::CDList< CVC3::Theorem >, CVC3::CDList< size_t >, CVC3::CDList< CVC3::Trigger >, CVC3::CDList< CVC3::dynTrig >, CVC3::CDList< CVC3::Literal >, CVC3::CDList< CVC3::TheoryArithNew::Ineq >, CVC3::CDList< CVC3::TheoryArith3::Ineq >, CVC3::CDO< T >, CVC3::CDO< CVC3::Clause >, CVC3::CDO< int >, CVC3::CDO< CVC3::Rational >, CVC3::CDO< unsigned int >, CVC3::CDO< CVC3::Unsigned >, CVC3::CDO< U >, CVC3::CDO< CVC3::Expr >, CVC3::CDO< CVC3::Theorem >, CVC3::CDO< QueryResult >, CVC3::CDO< std::set< CVC3::SearchSat::LitPriorityPair >::const_iterator >, CVC3::CDO< size_t >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDFlags.
Definition at line 239 of file context.h.
References FatalAssert.
|
inlineprotected |
Definition at line 244 of file context.h.
References CVC3::ContextObjChain::d_data.
Referenced by CVC3::CDList< CVC3::TheoryArith3::Ineq >::pop_back().
|
protectedpure virtual |
Set the current object to be invalid.
Implemented in CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArith3::FreeConst >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr > >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArith3::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst >, CVC3::CDMap< CVC3::Expr, CVC3::Rational, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo >, CVC3::CDMap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > *, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Literal >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned > >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational >, CVC3::CDMap< CVC3::Expr, int, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > * >, CVC3::CDMap< CVC3::Expr, std::set< std::vector< CVC3::Expr > >, HashFcn >, CVC3::CDMap< CVC3::Expr, std::set< std::vector< CVC3::Expr > > >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational, HashFcn >, CVC3::CDMap< CVC3::Expr, bool >, CVC3::CDMap< CVC3::Expr, CVC3::Literal, HashFcn >, CVC3::CDMap< CVC3::Expr, bool, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::Rational >, CVC3::CDMap< CVC3::Expr, CVC3::Expr >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< CVC3::Expr, int >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDMapOrdered< Key, Data >, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArith3::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Rational, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::CDList< CVC3::dynTrig > *, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::SmartCDO< CVC3::Unsigned >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< CVC3::Expr, int, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Theorem, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithOld::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::set< std::vector< CVC3::Expr > >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Literal, HashFcn >, CVC3::CDOmap< CVC3::Expr, bool, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDList< T >, CVC3::CDList< CVC3::TheoryArithOld::Ineq >, CVC3::CDList< std::vector< CVC3::Expr > >, CVC3::CDList< CVC3::SmartCDO< CVC3::Theorem > >, CVC3::CDList< CVC3::Theory * >, CVC3::CDList< SAT::Clause >, CVC3::CDList< CVC3::SearchImplBase::Splitter >, CVC3::CDList< CVC3::ClauseOwner >, CVC3::CDList< ProcessKinds >, CVC3::CDList< Expr >, CVC3::CDList< CVC3::Expr >, CVC3::CDList< CVC3::Theorem >, CVC3::CDList< size_t >, CVC3::CDList< CVC3::Trigger >, CVC3::CDList< CVC3::dynTrig >, CVC3::CDList< CVC3::Literal >, CVC3::CDList< CVC3::TheoryArithNew::Ineq >, CVC3::CDList< CVC3::TheoryArith3::Ineq >, CVC3::CDO< T >, CVC3::CDO< CVC3::Clause >, CVC3::CDO< int >, CVC3::CDO< CVC3::Rational >, CVC3::CDO< unsigned int >, CVC3::CDO< CVC3::Unsigned >, CVC3::CDO< U >, CVC3::CDO< CVC3::Expr >, CVC3::CDO< CVC3::Theorem >, CVC3::CDO< QueryResult >, CVC3::CDO< std::set< CVC3::SearchSat::LitPriorityPair >::const_iterator >, CVC3::CDO< size_t >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDFlags.
|
inlineprotected |
Return our name (for debugging)
Get context memory manager
Definition at line 255 of file context.h.
References CVC3::Scope::getCMM().
|
inline |
Definition at line 269 of file context.h.
References CVC3::Scope::level().
Referenced by CVC3::CDFlags::update().
|
inline |
Definition at line 270 of file context.h.
References CVC3::Scope::isCurrent(), and CVC3::Scope::level().
Referenced by CVC3::CDList< CVC3::TheoryArith3::Ineq >::pop_back().
|
inline |
Definition at line 274 of file context.h.
Referenced by CVC3::CDList< CVC3::TheoryArith3::Ineq >::push_back(), CVC3::CDO< bool >::set(), CVC3::CDOmapOrdered< Key, Data >::set(), and CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >::set().
|
inline |
Definition at line 277 of file context.h.
References CVC3::MemoryManager::newData().
|
inline |
Definition at line 280 of file context.h.
References CVC3::MemoryManager::deleteData().
|
inline |
|
inline |
|
friend |
|
private |
Last scope in which this object was modified.
Definition at line 206 of file context.h.
Referenced by CVC3::Scope::finalize(), and update().
|
private |
The list of values on previous scopes; our destructor should clean up those.
Definition at line 210 of file context.h.
Referenced by CVC3::Scope::finalize(), CVC3::CDFlags::update(), and update().