diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-04-06 06:39:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-04-06 06:39:01 +0000 |
commit | 4143f662e0c5ef311e98dbd554500b98cd02ecdb (patch) | |
tree | 79abe3f9393d41450ada658dbd3f0914680048c9 /src/context/cdo.h | |
parent | 6ad21b68e654b940d97caea6d34404d0a6b6e628 (diff) |
* Add some protected ContextObj accessors for ContextObj-derived classes:
+ Context* getContext() -- gets the context
+ ContextMemoryManager* getCMM() -- gets the CMM
+ int getLevel() -- the scope level of the ContextObj's most recent update
+ bool isCurrent() -- true iff the most recent update is the current top level
In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
ECData::addPredecessor() function substantially (re: code review bug #64).
* Fix serious bugs in context operations that corrupted the ContextObj
linked lists. Closes bug #85.
* Identified a bug in the way objects of the "Link" class are
allocated; see bug #96.
* Re-enable context white-box tests that ensure proper links in linked
lists. Closes bug #86.
* Re-enable CDMap<>::emptyTrash(). Closes bug #87.
* Add a tracing option (-t foo or --trace foo) to the driver to enable
Trace("foo") output stream. -d foo implies -t foo.
* Minor clean-up of some TheoryUF code; addition of some documentation
(re: code review bug #64).
* Address some things that caused Doxygen discomfort.
* Address an issue raised in NodeManager's code review (bug #65).
* Remove an inaccurate comment in Attribute code (re: code review bug #61).
Diffstat (limited to 'src/context/cdo.h')
-rw-r--r-- | src/context/cdo.h | 38 |
1 files changed, 35 insertions, 3 deletions
diff --git a/src/context/cdo.h b/src/context/cdo.h index e03156e8a..ead43b2e8 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -66,11 +66,26 @@ class CDO : public ContextObj { CDO<T>& operator=(const CDO<T>& cdo); public: + /** * Main constructor - uses default constructor for T to create the initial * value of d_data. */ - CDO(Context* context) : ContextObj(context) {} + CDO(Context* context) : + ContextObj(context) { + } + + /** + * Main constructor - uses default constructor for T to create the + * initial value of d_data. + * + * This version takes an argument that specifies whether this CDO<> + * was itself allocated in context memory. If it was, it is linked + * with the current scope rather than scope 0. + */ + CDO(bool allocatedInCMM, Context* context) : + ContextObj(allocatedInCMM, context) { + } /** * Constructor from object of type T. Creates a ContextObj and sets the data @@ -78,7 +93,24 @@ public: * current Scope. If the Scope is popped, the value will revert to whatever * is assigned by the default constructor for T */ - CDO(Context* context, const T& data) : ContextObj(context) { + CDO(Context* context, const T& data) : + ContextObj(context) { + makeCurrent(); + d_data = data; + } + + /** + * Constructor from object of type T. Creates a ContextObj and sets the data + * to the given data value. Note that this value is only valid in the + * current Scope. If the Scope is popped, the value will revert to whatever + * is assigned by the default constructor for T. + * + * This version takes an argument that specifies whether this CDO<> + * was itself allocated in context memory. If it was, it is linked + * with the current scope rather than scope 0. + */ + CDO(bool allocatedInCMM, Context* context, const T& data) : + ContextObj(allocatedInCMM, context) { makeCurrent(); d_data = data; } @@ -86,7 +118,7 @@ public: /** * Destructor - call destroy() method */ - ~CDO() throw() { destroy(); } + ~CDO() throw(AssertionException) { destroy(); } /** * Set the data in the CDO. First call makeCurrent. |