#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 >.
|
void | update (int scope=-1) |
| Update on the given scope, on the current scope if 'scope' == -1.
|
|
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.
CVC3::ContextObj::ContextObj |
( |
const ContextObj & |
co | ) |
|
|
inlineprotected |
ContextObj::~ContextObj |
( |
| ) |
|
|
virtual |
void ContextObj::update |
( |
int |
scope = -1 | ) |
|
|
private |
Assignment operator (defined mainly for debugging purposes)
Definition at line 229 of file context.h.
References DebugAssert.
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.
Return our name (for debugging)
Get context memory manager
Definition at line 255 of file context.h.
int CVC3::ContextObj::level |
( |
void |
| ) |
const |
|
inline |
bool CVC3::ContextObj::isCurrent |
( |
int |
scope = -1 | ) |
const |
|
inline |
void CVC3::ContextObj::makeCurrent |
( |
int |
scope = -1 | ) |
|
|
inline |
void* CVC3::ContextObj::operator new |
( |
size_t |
size, |
|
|
MemoryManager * |
mm |
|
) |
| |
|
inline |
void CVC3::ContextObj::operator delete |
( |
void * |
pMem, |
|
|
MemoryManager * |
mm |
|
) |
| |
|
inline |
void* CVC3::ContextObj::operator new |
( |
size_t |
size, |
|
|
bool |
b |
|
) |
| |
|
inline |
void CVC3::ContextObj::operator delete |
( |
void * |
pMem, |
|
|
bool |
b |
|
) |
| |
|
inline |
void CVC3::ContextObj::operator delete |
( |
void * |
| ) |
|
|
inline |
Scope* CVC3::ContextObj::d_scope |
|
private |
The documentation for this class was generated from the following files: