CVC3
Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::ContextObj Class Referenceabstract

#include <context.h>

Inherited by CVC3::CDList< Clause >, CVC3::CDList< ClauseOwner >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< Ineq >, CVC3::CDList< Literal >, CVC3::CDList< ProcessKinds >, CVC3::CDList< size_t >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDList< Splitter >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Theorem >, CVC3::CDList< Theory * >, CVC3::CDList< Trigger >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDO< bool >, CVC3::CDO< Clause >, CVC3::CDO< Expr >, CVC3::CDO< int >, CVC3::CDO< QueryResult >, CVC3::CDO< Rational >, CVC3::CDO< size_t >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Theorem >, CVC3::CDO< U >, CVC3::CDO< unsigned >, CVC3::CDO< Unsigned >, CVC3::CDO< unsigned int >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDO< T >, CVC3::CDOmap< Key, Data, HashFcn >, and CVC3::CDOmapOrdered< Key, Data >.

Collaboration diagram for CVC3::ContextObj:
Collaboration graph

Public Member Functions

 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 *)
 

Protected Member Functions

 ContextObj (const ContextObj &co)
 Copy constructor (defined mainly for debugging purposes)
 
ContextObjoperator= (const ContextObj &co)
 Assignment operator (defined mainly for debugging purposes)
 
virtual ContextObjmakeCopy (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 ContextObjgetRestore ()
 
virtual void setNull (void)=0
 Set the current object to be invalid.
 
ContextMemoryManagergetCMM ()
 Return our name (for debugging)
 

Private Member Functions

void update (int scope=-1)
 Update on the given scope, on the current scope if 'scope' == -1.
 

Private Attributes

Scoped_scope
 Last scope in which this object was modified.
 
ContextObjChaind_restore
 The list of values on previous scopes; our destructor should clean up those.
 

Friends

class Scope
 
class ContextObjChain
 
class CDFlags
 

Detailed Description

Description: This is a generic class from which all objects that are context-dependent should inherit. Subclasses need to implement makeCopy, restoreData, and setNull.

Definition at line 200 of file context.h.

Constructor & Destructor Documentation

CVC3::ContextObj::ContextObj ( const ContextObj co)
inlineprotected

Copy constructor (defined mainly for debugging purposes)

Definition at line 220 of file context.h.

References DebugAssert, and IF_DEBUG.

ContextObj::~ContextObj ( )
virtual

Member Function Documentation

void ContextObj::update ( int  scope = -1)
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().

ContextObj& CVC3::ContextObj::operator= ( const ContextObj co)
inlineprotected

Assignment operator (defined mainly for debugging purposes)

Definition at line 229 of file context.h.

References DebugAssert.

virtual ContextObj* CVC3::ContextObj::makeCopy ( ContextMemoryManager cmm)
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< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDList< T >, CVC3::CDList< Theory * >, CVC3::CDList< Theorem >, CVC3::CDList< Literal >, CVC3::CDList< Splitter >, CVC3::CDList< ProcessKinds >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< size_t >, CVC3::CDList< ClauseOwner >, CVC3::CDList< Clause >, CVC3::CDList< Trigger >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Ineq >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDO< T >, CVC3::CDO< int >, CVC3::CDO< Theorem >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Expr >, CVC3::CDO< QueryResult >, CVC3::CDO< size_t >, CVC3::CDO< Unsigned >, CVC3::CDO< Clause >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, CVC3::CDO< Rational >, and CVC3::CDFlags.

virtual void CVC3::ContextObj::restoreData ( ContextObj data)
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< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDList< T >, CVC3::CDList< Theory * >, CVC3::CDList< Theorem >, CVC3::CDList< Literal >, CVC3::CDList< Splitter >, CVC3::CDList< ProcessKinds >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< size_t >, CVC3::CDList< ClauseOwner >, CVC3::CDList< Clause >, CVC3::CDList< Trigger >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Ineq >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDO< T >, CVC3::CDO< int >, CVC3::CDO< Theorem >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Expr >, CVC3::CDO< QueryResult >, CVC3::CDO< size_t >, CVC3::CDO< Unsigned >, CVC3::CDO< Clause >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, CVC3::CDO< Rational >, and CVC3::CDFlags.

Definition at line 239 of file context.h.

References FatalAssert.

const ContextObj* CVC3::ContextObj::getRestore ( )
inlineprotected
virtual void CVC3::ContextObj::setNull ( void  )
protectedpure virtual

Set the current object to be invalid.

Implemented in CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDMapOrdered< Key, Data >, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDList< T >, CVC3::CDList< Theory * >, CVC3::CDList< Theorem >, CVC3::CDList< Literal >, CVC3::CDList< Splitter >, CVC3::CDList< ProcessKinds >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< size_t >, CVC3::CDList< ClauseOwner >, CVC3::CDList< Clause >, CVC3::CDList< Trigger >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Ineq >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDO< T >, CVC3::CDO< int >, CVC3::CDO< Theorem >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Expr >, CVC3::CDO< QueryResult >, CVC3::CDO< size_t >, CVC3::CDO< Unsigned >, CVC3::CDO< Clause >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, CVC3::CDO< Rational >, and CVC3::CDFlags.

ContextMemoryManager* CVC3::ContextObj::getCMM ( )
inlineprotected

Return our name (for debugging)

Get context memory manager

Definition at line 255 of file context.h.

int CVC3::ContextObj::level ( void  ) const
inline

Definition at line 269 of file context.h.

Referenced by CVC3::Expr::getFindLevel(), and CVC3::CDFlags::update().

bool CVC3::ContextObj::isCurrent ( int  scope = -1) const
inline

Definition at line 270 of file context.h.

Referenced by CVC3::CDList< SmartCDO< Theorem > >::pop_back().

void CVC3::ContextObj::makeCurrent ( int  scope = -1)
inline
void* CVC3::ContextObj::operator new ( size_t  size,
MemoryManager mm 
)
inline

Definition at line 277 of file context.h.

References CVC3::MemoryManager::newData().

void CVC3::ContextObj::operator delete ( void *  pMem,
MemoryManager mm 
)
inline

Definition at line 280 of file context.h.

References CVC3::MemoryManager::deleteData().

void* CVC3::ContextObj::operator new ( size_t  size,
bool  b 
)
inline

Definition at line 286 of file context.h.

void CVC3::ContextObj::operator delete ( void *  pMem,
bool  b 
)
inline

Definition at line 289 of file context.h.

void CVC3::ContextObj::operator delete ( void *  )
inline

Definition at line 293 of file context.h.

Friends And Related Function Documentation

friend class Scope
friend

Definition at line 201 of file context.h.

friend class ContextObjChain
friend

Definition at line 202 of file context.h.

friend class CDFlags
friend

Definition at line 203 of file context.h.

Member Data Documentation

Scope* CVC3::ContextObj::d_scope
private

Last scope in which this object was modified.

Definition at line 206 of file context.h.

Referenced by CVC3::Scope::finalize(), and update().

ContextObjChain* CVC3::ContextObj::d_restore
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().


The documentation for this class was generated from the following files: