CVC3::ContextObj Class Reference
[Context Management]

#include <context.h>

Inheritance diagram for CVC3::ContextObj:

[legend]Collaboration diagram for CVC3::ContextObj:

[legend]List of all members.

Public Member Functions

• ContextObj (Context *context, bool atBottomScope=true)

  Create a new ContextObj.
  

• virtual ~ContextObj ()
• int level () const
• bool isCurrent (int scope=-1) const
• void makeCurrent (int scope=-1)
• void setName (const std::string &name)
• 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).
  

• 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.
  

• virtual std::string name () const

  Return our name (for debugging).
  

• ContextMemoryManager * getCMM ()

  Get context memory manager.
  

Private Member Functions

• void update (int scope=-1)

  Update on the given scope, on the current scope if 'scope' == -1.
  

Private Attributes

• Scope * d_scope

  Last scope in which this object was modified.
  

• ContextObjChain * d_restore

  The list of values on previous scopes; our destructor should clean up those.
  

• std::string d_name
• bool d_active

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 195 of file context.h.

---

Constructor & Destructor Documentation

CVC3::ContextObj::ContextObj

(

const ContextObj &

co

)

[inline, protected]

Copy constructor (defined mainly for debugging purposes).

Definition at line 215 of file context.h.

References d_active, d_name, DebugAssert, IF_DEBUG, and name().

ContextObj::~ContextObj

(

)

[virtual]

Definition at line 155 of file context.cpp.

References d_active, d_restore, FatalAssert, IF_DEBUG, and name().

---

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 129 of file context.cpp.

References CVC3::Scope::addToChain(), ContextObjChain, d_restore, d_scope, DebugAssert, getCMM(), IF_DEBUG, CVC3::Scope::level(), level(), makeCopy(), name(), CVC3::Scope::prevScope(), setName(), and CVC3::Scope::topScope().

ContextObj& CVC3::ContextObj::operator=

(

const ContextObj &

co

)

[inline, protected]

Assignment operator (defined mainly for debugging purposes).

Definition at line 224 of file context.h.

References DebugAssert.

virtual ContextObj* CVC3::ContextObj::makeCopy

(

ContextMemoryManager *

cmm

)

[protected, pure virtual]

Make a copy of the current object so it can be restored to its current state.

Implemented in CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDO< T >, CVC3::CDList< CVC3::SmartCDO< CVC3::Theorem > >, CVC3::CDList< CVC3::Theory * >, CVC3::CDList< SAT::Clause >, CVC3::CDList< CVC3::TheoryDatatypeLazy::ProcessKinds >, CVC3::CDList< CVC3::SearchImplBase::Splitter >, CVC3::CDList< CVC3::ClauseOwner >, 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::CDOmap< CVC3::Expr, CVC3::SmartCDO< unsigned >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::vector< CVC3::Expr >, 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< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr > >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< unsigned >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational >, 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::VCL::UserAssertion >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo >, CVC3::CDMap< CVC3::Expr, CVC3::Literal >, 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, 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::Expr >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem >, CVC3::CDMap< CVC3::Expr, int >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< unsigned > >, CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDO< CVC3::Clause >, CVC3::CDO< int >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< CVC3::Expr >, CVC3::CDO< CVC3::Theorem >, CVC3::CDO< std::set< CVC3::SearchSat::LitPriorityPair >::const_iterator >, CVC3::CDO< size_t >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDO< CVC3::QueryResult >.

Referenced by update().

virtual void CVC3::ContextObj::restoreData

(

ContextObj *

data

)

[inline, protected, virtual]

Restore the current object from the given data.

Reimplemented in CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDO< T >, CVC3::CDList< CVC3::SmartCDO< CVC3::Theorem > >, CVC3::CDList< CVC3::Theory * >, CVC3::CDList< SAT::Clause >, CVC3::CDList< CVC3::TheoryDatatypeLazy::ProcessKinds >, CVC3::CDList< CVC3::SearchImplBase::Splitter >, CVC3::CDList< CVC3::ClauseOwner >, 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::CDOmap< CVC3::Expr, CVC3::SmartCDO< unsigned >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::vector< CVC3::Expr >, 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< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr > >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< unsigned >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational >, 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::VCL::UserAssertion >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo >, CVC3::CDMap< CVC3::Expr, CVC3::Literal >, 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, 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::Expr >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem >, CVC3::CDMap< CVC3::Expr, int >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< unsigned > >, CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDO< CVC3::Clause >, CVC3::CDO< int >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< CVC3::Expr >, CVC3::CDO< CVC3::Theorem >, CVC3::CDO< std::set< CVC3::SearchSat::LitPriorityPair >::const_iterator >, CVC3::CDO< size_t >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDO< CVC3::QueryResult >.

Definition at line 234 of file context.h.

References FatalAssert.

const ContextObj* CVC3::ContextObj::getRestore

(

)

[inline, protected]

Definition at line 239 of file context.h.

References CVC3::ContextObjChain::d_data, and CVC3::ContextObjChain::d_restore.

Referenced by CVC3::CDList< CVC3::Literal >::pop_back().

virtual void CVC3::ContextObj::setNull

(

void

)

[protected, pure virtual]

Set the current object to be invalid.

Implemented in CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDO< T >, CVC3::CDList< CVC3::SmartCDO< CVC3::Theorem > >, CVC3::CDList< CVC3::Theory * >, CVC3::CDList< SAT::Clause >, CVC3::CDList< CVC3::TheoryDatatypeLazy::ProcessKinds >, CVC3::CDList< CVC3::SearchImplBase::Splitter >, CVC3::CDList< CVC3::ClauseOwner >, 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::CDOmap< CVC3::Expr, CVC3::SmartCDO< unsigned >, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDOmap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< CVC3::Expr, std::vector< CVC3::Expr >, 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< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr > >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< unsigned >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::VCL::UserAssertion, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::EpsRational >, 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::VCL::UserAssertion >, CVC3::CDMap< CVC3::Expr, std::vector< CVC3::Expr >, HashFcn >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::BoundInfo >, CVC3::CDMap< CVC3::Expr, CVC3::Literal >, 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, 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::Expr >, CVC3::CDMap< CVC3::Expr, CVC3::Theorem >, CVC3::CDMap< CVC3::Expr, int >, CVC3::CDMap< CVC3::Expr, CVC3::TheoryArithNew::FreeConst >, CVC3::CDMap< CVC3::Expr, CVC3::SmartCDO< unsigned > >, CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >, CVC3::CDO< CVC3::Clause >, CVC3::CDO< int >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< CVC3::Expr >, CVC3::CDO< CVC3::Theorem >, CVC3::CDO< std::set< CVC3::SearchSat::LitPriorityPair >::const_iterator >, CVC3::CDO< size_t >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDO< CVC3::QueryResult >.

virtual std::string CVC3::ContextObj::name

(

)

const [inline, protected, virtual]

Return our name (for debugging).

Definition at line 247 of file context.h.

Referenced by ContextObj(), CVC3::ContextObjChain::name(), update(), and ~ContextObj().

ContextMemoryManager* CVC3::ContextObj::getCMM

(

)

[inline, protected]

Get context memory manager.

Definition at line 250 of file context.h.

Referenced by update().

int CVC3::ContextObj::level

(

void

)

const [inline]

Definition at line 264 of file context.h.

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

bool CVC3::ContextObj::isCurrent

(

int

scope = -1

)

const [inline]

Definition at line 265 of file context.h.

Referenced by CVC3::CDList< CVC3::Literal >::pop_back().

void CVC3::ContextObj::makeCurrent

(

int

scope = -1

)

[inline]

Definition at line 269 of file context.h.

Referenced by CVC3::CDList< CVC3::Literal >::push_back(), CVC3::CDO< CVC3::QueryResult >::set(), CVC3::CDOmapOrdered< Key, Data >::set(), CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >::set(), and CVC3::CDFlags::update().

void CVC3::ContextObj::setName

(

const std::string &

name

)

[inline]

Definition at line 270 of file context.h.

Referenced by CVC3::CDFlags::CDFlags(), CVC3::CDList< CVC3::Literal >::CDList(), CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >::CDMap(), CVC3::CDMapOrdered< Key, Data >::CDMapOrdered(), CVC3::CDO< CVC3::QueryResult >::CDO(), CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >::CDOmap(), CVC3::CDOmapOrdered< Key, Data >::CDOmapOrdered(), CVC3::ClauseValue::ClauseValue(), CVC3::VariableValue::setAssumpThm(), CVC3::Expr::setFind(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), CVC3::VariableValue::setValue(), CVC3::TheoryArithNew::TheoryArithNew(), CVC3::TheoryArithOld::TheoryArithOld(), and update().

void* CVC3::ContextObj::operator new	(	size_t	size,
		MemoryManager *	mm
	)			[inline]

Definition at line 272 of file context.h.

References CVC3::MemoryManager::newData().

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

Definition at line 275 of file context.h.

References CVC3::MemoryManager::deleteData().

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

Definition at line 281 of file context.h.

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

Definition at line 284 of file context.h.

void CVC3::ContextObj::operator delete

(

void *

)

[inline]

Definition at line 288 of file context.h.

---

Friends And Related Function Documentation

friend class Scope [friend]

Definition at line 196 of file context.h.

friend class ContextObjChain [friend]

Definition at line 197 of file context.h.

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

friend class CDFlags [friend]

Definition at line 198 of file context.h.

---

Member Data Documentation

Scope* CVC3::ContextObj::d_scope [private]

Last scope in which this object was modified.

Definition at line 201 of file context.h.

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

ContextObjChain* CVC3::ContextObj::d_restore [private]

The list of values on previous scopes; our destructor should clean up those.

Definition at line 205 of file context.h.

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

std::string CVC3::ContextObj::d_name [private]

Definition at line 207 of file context.h.

Referenced by ContextObj().

bool CVC3::ContextObj::d_active [private]

Definition at line 208 of file context.h.

Referenced by ContextObj(), and ~ContextObj().

---

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

• context.h
• context.cpp

---