summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/context/cdmap.h14
-rw-r--r--src/context/cdo.h38
-rw-r--r--src/context/context.cpp138
-rw-r--r--src/context/context.h168
-rw-r--r--src/context/context_mm.cpp3
-rw-r--r--src/expr/attribute.cpp1
-rw-r--r--src/expr/attribute.h5
-rw-r--r--src/expr/command.cpp8
-rw-r--r--src/expr/expr_manager_template.cpp2
-rw-r--r--src/expr/node_manager.h17
-rw-r--r--src/main/getopt.cpp14
-rw-r--r--src/main/usage.h3
-rw-r--r--src/theory/uf/ecdata.cpp42
-rw-r--r--src/theory/uf/ecdata.h75
-rw-r--r--src/theory/uf/theory_uf.cpp2
-rw-r--r--test/unit/context/context_white.h11
16 files changed, 402 insertions, 139 deletions
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index d4de88daf..75f6eb2ae 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -71,6 +71,7 @@ class CDOmap : public ContextObj {
}
d_next->d_prev = d_prev;
d_prev->d_next = d_next;
+ Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
d_map->d_trash.push_back(this);
} else {
d_data = p->d_data;
@@ -155,7 +156,7 @@ public:
CDMapData(Context* context) : ContextObj(context) {}
CDMapData(const ContextObj& co) : ContextObj(co) {}
- ~CDMapData() { destroy(); }
+ ~CDMapData() throw(AssertionException) { destroy(); }
};
/**
@@ -192,7 +193,7 @@ class CDMap : public ContextObj {
i != d_trash.end();
++i) {
Debug("gc") << "emptyTrash(): " << *i << std::endl;
- //(*i)->deleteSelf();
+ (*i)->deleteSelf();
}
d_trash.clear();
}
@@ -201,21 +202,26 @@ public:
CDMap(Context* context) :
ContextObj(context),
+ d_map(),
d_first(NULL),
d_context(context),
d_trash() {
}
~CDMap() throw(AssertionException) {
+ Debug("gc") << "cdmap " << this
+ << " disappearing, destroying..." << std::endl;
destroy();
+ Debug("gc") << "cdmap " << this
+ << " disappearing, done destroying" << std::endl;
for(typename table_type::iterator i = d_map.begin();
i != d_map.end();
++i) {
(*i).second->deleteSelf();
}
- //d_map.clear();
- Debug("gc") << "cdmap gone, emptying trash" << std::endl;
+ Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl;
emptyTrash();
+ Debug("gc") << "done emptying trash for " << this << std::endl;
}
// The usual operators of map
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.
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 05024430c..d371dc39a 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -10,9 +10,13 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
+ ** Implementation of base context operations.
**/
+#include <iostream>
+#include <vector>
+
#include "context/context.h"
#include "util/Assert.h"
@@ -54,7 +58,7 @@ Context::~Context() throw(AssertionException) {
void Context::push() {
- // FIXME: TRACE("pushpop", indentStr, "Push", " {");
+ Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl;
// Create a new memory region
d_pCMM->push();
@@ -93,7 +97,7 @@ void Context::pop() {
pCNO = pCNO->d_pCNOnext;
}
- //FIXME: TRACE("pushpop", indentStr, "}", " Pop");
+ Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl;
}
@@ -124,16 +128,47 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
}
-void ContextObj::update() {
+void ContextObj::update() throw(AssertionException) {
+ Debug("context") << "before update(" << this << "):" << std::endl
+ << *getContext() << std::endl;
+
// Call save() to save the information in the current object
ContextObj* pContextObjSaved = save(d_pScope->getCMM());
+ Debug("context") << "in update(" << this << ") with restore "
+ << pContextObjSaved << ": waypoint 1" << std::endl
+ << *getContext() << std::endl;
+
// Check that base class data was saved
- Assert(pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
- pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
- pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
- pContextObjSaved->d_pScope == d_pScope,
- "save() did not properly copy information in base class");
+ Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
+ pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
+ pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
+ pContextObjSaved->d_pScope == d_pScope ),
+ "save() did not properly copy information in base class" );
+
+ // Link the "saved" object in place of this ContextObj in the scope
+ // we're moving it FROM.
+ Debug("context") << "in update(" << this
+ << "): next() == " << next() << std::endl;
+ if(next() != NULL) {
+ Debug("context") << "in update(" << this
+ << "): next()->prev() == " << next()->prev() << std::endl;
+ next()->prev() = &pContextObjSaved->next();
+ Debug("context") << "in update(" << this
+ << "): next()->prev() is now "
+ << next()->prev() << std::endl;
+ }
+ Debug("context") << "in update(" << this
+ << "): prev() == " << prev() << std::endl;
+ Debug("context") << "in update(" << this
+ << "): *prev() == " << *prev() << std::endl;
+ *prev() = pContextObjSaved;
+ Debug("context") << "in update(" << this
+ << "): *prev() is now " << *prev() << std::endl;
+
+ Debug("context") << "in update(" << this << ") with restore "
+ << pContextObjSaved << ": waypoint 3" << std::endl
+ << *getContext() << std::endl;
// Update Scope pointer to current top Scope
d_pScope = d_pScope->getContext()->getTopScope();
@@ -144,18 +179,27 @@ void ContextObj::update() {
// Insert object into the list of objects that need to be restored when this
// Scope is popped.
d_pScope->addToChain(this);
+
+ Debug("context") << "after update(" << this << ") with restore "
+ << pContextObjSaved << ":" << std::endl
+ << *getContext() << std::endl;
}
-ContextObj* ContextObj::restoreAndContinue() {
+ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
// Variable to hold next object in list
ContextObj* pContextObjNext;
// Check the restore pointer. If NULL, this must be the bottom Scope
if(d_pContextObjRestore == NULL) {
- Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
- "Expected bottom scope");
+ // might not be bottom scope, since objects allocated in context
+ // memory don't get linked to scope 0
+ //
+ // Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
+ // "Expected bottom scope");
+
pContextObjNext = d_pContextObjNext;
+
// Nothing else to do
} else {
// Call restore to update the subclass data
@@ -169,13 +213,23 @@ ContextObj* ContextObj::restoreAndContinue() {
next() = d_pContextObjRestore->d_pContextObjNext;
prev() = d_pContextObjRestore->d_ppContextObjPrev;
d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
+
+ // Re-link this ContextObj to the list in this scope
+ if(next() != NULL) {
+ next()->prev() = &next();
+ }
+ *prev() = this;
}
+
// Return the next object in the list
return pContextObjNext;
}
void ContextObj::destroy() throw(AssertionException) {
+ Debug("context") << "before destroy " << this
+ << " (level " << getLevel() << "):" << std::endl
+ << *getContext() << std::endl;
for(;;) {
// If valgrind reports invalid writes on the next few lines,
// here's a hint: make sure all classes derived from ContextObj in
@@ -184,12 +238,18 @@ void ContextObj::destroy() throw(AssertionException) {
if(next() != NULL) {
next()->prev() = prev();
}
- *(prev()) = next();
+ *prev() = next();
if(d_pContextObjRestore == NULL) {
break;
}
+ Debug("context") << "in destroy " << this << ", restore object is "
+ << d_pContextObjRestore << " at level "
+ << d_pContextObjRestore->getLevel() << ":" << std::endl
+ << *getContext() << std::endl;
restoreAndContinue();
}
+ Debug("context") << "after destroy " << this << ":" << std::endl
+ << *getContext() << std::endl;
}
@@ -198,11 +258,27 @@ ContextObj::ContextObj(Context* pContext) :
Assert(pContext != NULL, "NULL context pointer");
+ Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
d_pScope = pContext->getBottomScope();
d_pScope->addToChain(this);
}
+ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
+ d_pContextObjRestore(NULL) {
+
+ Assert(pContext != NULL, "NULL context pointer");
+
+ Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+ if(allocatedInCMM) {
+ d_pScope = pContext->getTopScope();
+ } else {
+ d_pScope = pContext->getBottomScope();
+ }
+ d_pScope->addToChain(this);
+}
+
+
ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
if(preNotify) {
pContext->addNotifyObjPre(this);
@@ -217,8 +293,44 @@ ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
}
if(d_ppCNOprev != NULL) {
- *(d_ppCNOprev) = d_pCNOnext;
+ *d_ppCNOprev = d_pCNOnext;
+ }
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+ const Context& context) throw(AssertionException) {
+ const std::string separator(79, '-');
+
+ int level = context.d_scopeList.size() - 1;
+ typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
+ for(const_reverse_iterator i = context.d_scopeList.rbegin();
+ i != context.d_scopeList.rend();
+ ++i, --level) {
+ Scope* pScope = *i;
+ Assert(pScope->getLevel() == level);
+ Assert(pScope->getContext() == &context);
+ out << separator << std::endl
+ << *pScope << std::endl;
+ }
+ return out << separator << std::endl;
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+ const Scope& scope) throw(AssertionException) {
+ out << "Scope " << scope.d_level << ":";
+ ContextObj* pContextObj = scope.d_pContextObjList;
+ Assert(pContextObj == NULL ||
+ pContextObj->prev() == &scope.d_pContextObjList);
+ while(pContextObj != NULL) {
+ out << " <--> " << pContextObj;
+ Assert(pContextObj->d_pScope == &scope);
+ Assert(pContextObj->next() == NULL ||
+ pContextObj->next()->prev() == &pContextObj->next());
+ pContextObj = pContextObj->next();
}
+ return out << " --> NULL";
}
diff --git a/src/context/context.h b/src/context/context.h
index 0e2a9107f..ff650ce5d 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -18,13 +18,15 @@
#ifndef __CVC4__CONTEXT__CONTEXT_H
#define __CVC4__CONTEXT__CONTEXT_H
-#include "context/context_mm.h"
-#include "util/Assert.h"
-
+#include <iostream>
#include <cstdlib>
#include <cstring>
+#include <vector>
#include <new>
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
namespace CVC4 {
namespace context {
@@ -33,6 +35,14 @@ class Scope;
class ContextObj;
class ContextNotifyObj;
+/** Pretty-printing of Contexts (for debugging) */
+std::ostream&
+operator<<(std::ostream&, const Context&) throw(AssertionException);
+
+/** Pretty-printing of Scopes (for debugging) */
+std::ostream&
+operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
/**
* A Context encapsulates all of the dynamic state of the system. Its main
* methods are push() and pop(). A call to push() saves the current state,
@@ -78,6 +88,9 @@ class Context {
*/
ContextNotifyObj* d_pCNOpost;
+ friend std::ostream&
+ operator<<(std::ostream&, const Context&) throw(AssertionException);
+
public:
/**
* Constructor: create ContextMemoryManager and initial Scope
@@ -102,7 +115,7 @@ public:
/**
* Return the current Scope level.
*/
- int getLevel() const { return ((int)d_scopeList.size()) - 1; }
+ int getLevel() const { return d_scopeList.size() - 1; }
/**
* Return the ContextMemoryManager associated with the context.
@@ -176,13 +189,16 @@ class Scope {
*/
ContextObj* d_pContextObjList;
+ friend std::ostream&
+ operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
public:
/**
* Constructor: Create a new Scope; set the level and the previous Scope
* if any.
*/
- Scope(Context* pContext, ContextMemoryManager* pCMM, int level) :
+ Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() :
d_pContext(pContext),
d_pCMM(pCMM),
d_level(level),
@@ -193,38 +209,38 @@ public:
* Destructor: Restore all of the objects in ContextObjList. Defined inline
* below.
*/
- ~Scope() throw();
+ ~Scope() throw(AssertionException);
/**
* Get the Context for this Scope
*/
- Context* getContext() const { return d_pContext; }
+ Context* getContext() const throw() { return d_pContext; }
/**
* Get the ContextMemoryManager for this Scope
*/
- ContextMemoryManager* getCMM() const { return d_pCMM; }
+ ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
/**
* Get the level of the current Scope
*/
- int getLevel() const { return d_level; }
+ int getLevel() const throw() { return d_level; }
/**
* Return true iff this Scope is the current top Scope
*/
- bool isCurrent() const { return this == d_pContext->getTopScope(); }
+ bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
/**
- * When a ContextObj object is modified for the first time in this Scope, it
- * should call this method to add itself to the list of objects that will
- * need to be restored. Defined inline below.
+ * When a ContextObj object is modified for the first time in this
+ * Scope, it should call this method to add itself to the list of
+ * objects that will need to be restored. Defined inline below.
*/
- void addToChain(ContextObj* pContextObj);
+ void addToChain(ContextObj* pContextObj) throw(AssertionException);
/**
- * Overload operator new for use with ContextMemoryManager to allow creation
- * of new Scope objects in the current memory region.
+ * Overload operator new for use with ContextMemoryManager to allow
+ * creation of new Scope objects in the current memory region.
*/
static void* operator new(size_t size, ContextMemoryManager* pCMM) {
return pCMM->newData(size);
@@ -232,9 +248,10 @@ public:
/**
* Overload operator delete for Scope objects allocated using
- * ContextMemoryManager. No need to do anything because memory is freed
- * automatically when the ContextMemoryManager pop() method is called.
- * Include both placement and standard delete for completeness.
+ * ContextMemoryManager. No need to do anything because memory is
+ * freed automatically when the ContextMemoryManager pop() method is
+ * called. Include both placement and standard delete for
+ * completeness.
*/
static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
static void operator delete(void* pMem) {}
@@ -245,9 +262,9 @@ public:
};/* class Scope */
/**
- * This is an abstract base class from which all objects that are context-dependent
- * should inherit. For any data structure that you want to have be
- * automatically backtracked, do the following:
+ * This is an abstract base class from which all objects that are
+ * context-dependent should inherit. For any data structure that you
+ * want to have be automatically backtracked, do the following:
* 1. Create a class for the data structure that inherits from ContextObj
* 2. Implement save()
* The role of save() is to create a new ContexObj object that contains
@@ -310,31 +327,34 @@ class ContextObj {
* does the necessary bookkeeping to ensure that object can be restored to
* its current state when restore is called.
*/
- void update();
+ void update() throw(AssertionException);
// The rest of the private methods are for the benefit of the Scope. We make
// Scope our friend so it is the only one that can use them.
friend class Scope;
+ friend std::ostream&
+ operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
/**
* Return reference to next link in ContextObjList. Used by
* Scope::addToChain method.
*/
- ContextObj*& next() { return d_pContextObjNext; }
+ ContextObj*& next() throw() { return d_pContextObjNext; }
/**
* Return reference to prev link in ContextObjList. Used by
* Scope::addToChain method.
*/
- ContextObj**& prev() { return d_ppContextObjPrev; }
+ ContextObj**& prev() throw() { return d_ppContextObjPrev; }
/**
* This method is called by Scope during a pop: it does the necessary work to
* restore the object from its saved copy and then returns the next object in
* the list that needs to be restored.
*/
- ContextObj* restoreAndContinue();
+ ContextObj* restoreAndContinue() throw(AssertionException);
protected:
@@ -351,14 +371,10 @@ protected:
virtual void restore(ContextObj* pContextObjRestore) = 0;
/**
- * This method checks if the object has been modified in this Scope yet. If
- * not, it calls update().
+ * This method checks if the object has been modified in this Scope
+ * yet. If not, it calls update().
*/
- void makeCurrent() {
- if(!(d_pScope->isCurrent())) {
- update();
- }
- }
+ inline void makeCurrent() throw(AssertionException);
/**
* Should be called from sub-class destructor: calls restore until restored
@@ -369,9 +385,59 @@ protected:
*/
void destroy() throw(AssertionException);
+ /////
+ //
+ // These next four accessors return properties of the Scope to
+ // derived classes without giving them the Scope object directly.
+ //
+ /////
+
+ /**
+ * Get the Context with which this ContextObj was created. This is
+ * part of the protected interface, intended for derived classes to
+ * use if necessary.
+ */
+ Context* getContext() const throw() {
+ return d_pScope->getContext();
+ }
+
+ /**
+ * Get the ContextMemoryManager with which this ContextObj was
+ * created. This is part of the protected interface, intended for
+ * derived classes to use if necessary. If a ContextObj-derived
+ * class needs to allocate memory somewhere other than the save()
+ * member function (where it is explicitly given a
+ * ContextMemoryManager), it can use this accessor to get the memory
+ * manager.
+ */
+ ContextMemoryManager* getCMM() const throw() {
+ return d_pScope->getCMM();
+ }
+
+ /**
+ * Get the level associated to this ContextObj. Useful if a
+ * ContextObj-derived class needs to compare the level of its last
+ * update with another ContextObj.
+ */
+ int getLevel() const throw() {
+ return d_pScope->getLevel();
+ }
+
+ /**
+ * Returns true if the object is "current"-- that is, updated in the
+ * topmost contextual scope. Useful if a ContextObj-derived class
+ * needs to determine if it has been modified in the current scope.
+ * Note that it is always safe to call makeCurrent() without first
+ * checking if the object is current, so this function need not be
+ * used under normal circumstances.
+ */
+ bool isCurrent() const throw() {
+ return d_pScope->isCurrent();
+ }
+
/**
* operator new using ContextMemoryManager (common case used by
- * subclasses during save() ). No delete is required for memory
+ * subclasses during save()). No delete is required for memory
* allocated this way, since it is automatically released when the
* context is popped. Also note that allocations using this
* operator never have their destructor called, so any clean-up has
@@ -402,9 +468,17 @@ public:
ContextObj(Context* context);
/**
+ * Create a new ContextObj. This constructor takes an argument that
+ * specifies whether this ContextObj is itself allocated in context
+ * memory. If it is, it's invalid below the current scope level, so
+ * we don't put it in scope 0.
+ */
+ ContextObj(bool allocatedInCMM, Context* context);
+
+ /**
* Destructor does nothing: subclass must explicitly call destroy() instead.
*/
- virtual ~ContextObj() { Debug("contextgc") << "context obj dest" << std::endl; }
+ virtual ~ContextObj() {}
/**
* If you want to allocate a ContextObj object on the heap, use this
@@ -431,6 +505,7 @@ public:
* ContextMemoryManager as an argument.
*/
void deleteSelf() {
+ Debug("context") << "deleteSelf(" << this << ")" << std::endl;
this->~ContextObj();
::operator delete(this);
}
@@ -475,15 +550,16 @@ class ContextNotifyObj {
* Return reference to next link in ContextNotifyObj list. Used by
* Context::addNotifyObj methods.
*/
- ContextNotifyObj*& next() { return d_pCNOnext; }
+ ContextNotifyObj*& next() throw() { return d_pCNOnext; }
/**
* Return reference to prev link in ContextNotifyObj list. Used by
* Context::addNotifyObj methods.
*/
- ContextNotifyObj**& prev() { return d_ppCNOprev; }
+ ContextNotifyObj**& prev() throw() { return d_ppCNOprev; }
public:
+
/**
* Constructor for ContextNotifyObj. Parameters are the context to
* which this notify object will be added, and a flag which, if
@@ -504,11 +580,16 @@ public:
* implemented by the subclass.
*/
virtual void notify() = 0;
+
};/* class ContextNotifyObj */
-// Inline functions whose definitions had to be delayed:
+inline void ContextObj::makeCurrent() throw(AssertionException) {
+ if(!(d_pScope->isCurrent())) {
+ update();
+ }
+}
-inline Scope::~Scope() throw() {
+inline Scope::~Scope() throw(AssertionException) {
// Call restore() method on each ContextObj object in the list.
// Note that it is the responsibility of restore() to return the
// next item in the list.
@@ -517,9 +598,12 @@ inline Scope::~Scope() throw() {
}
}
-inline void Scope::addToChain(ContextObj* pContextObj) {
- if(d_pContextObjList != NULL)
- d_pContextObjList->prev() = &(pContextObj->next());
+inline void
+Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) {
+ if(d_pContextObjList != NULL) {
+ d_pContextObjList->prev() = &pContextObj->next();
+ }
+
pContextObj->next() = d_pContextObjList;
pContextObj->prev() = &d_pContextObjList;
d_pContextObjList = pContextObj;
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index ab81c7486..b0b015681 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -85,6 +85,9 @@ void* ContextMemoryManager::newData(size_t size) {
AlwaysAssert(d_nextFree <= d_endChunk,
"Request is bigger than memory chunk size");
}
+ Debug("context") << "ContextMemoryManager::newData(" << size
+ << ") returning " << res << " at level "
+ << d_chunkList.size() << std::endl;
return res;
}
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 5e8918133..1eeec68af 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -34,7 +34,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
// FIXME CD-bools in optimized table
for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) {
- Debug("gc") << "looking for " << id << " x " << nv << ":" << *nv << std::endl;
d_cdbools.obliterate(std::make_pair(id, nv));
}
for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) {
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index c79f4da80..27cddf299 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -112,11 +112,6 @@ public:
typename AttrKind::value_type getAttribute(NodeValue* nv,
const AttrKind&) const;
- // Note that there are two, distinct hasAttribute() declarations for
- // a reason (rather than using a default argument): they permit more
- // optimized code. The first (without parameter "ret") need never
- // check whether its parameter is NULL.
-
/**
* Determine if a particular attribute exists for a particular node.
*
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 934c405ad..5fc9dee20 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -42,7 +42,7 @@ void CommandSequence::invoke(SmtEngine* smtEngine) {
}
}
-void CheckSatCommand::toStream(ostream& out) const {
+void CheckSatCommand::toStream(std::ostream& out) const {
if(d_expr.isNull()) {
out << "CheckSat()";
} else {
@@ -50,7 +50,7 @@ void CheckSatCommand::toStream(ostream& out) const {
}
}
-void CommandSequence::toStream(ostream& out) const {
+void CommandSequence::toStream(std::ostream& out) const {
out << "CommandSequence[" << endl;
for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
out << *d_commandSequence[i] << endl;
@@ -75,7 +75,7 @@ void PushCommand::invoke(SmtEngine* smtEngine) {
smtEngine->push();
}
-void PushCommand::toStream(ostream& out) const {
+void PushCommand::toStream(std::ostream& out) const {
out << "Push()";
}
@@ -83,7 +83,7 @@ void PopCommand::invoke(SmtEngine* smtEngine) {
smtEngine->pop();
}
-void PopCommand::toStream(ostream& out) const {
+void PopCommand::toStream(std::ostream& out) const {
out << "Pop()";
}
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bb665ef81..a8d957c91 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -132,7 +132,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
child5.getNode())));
}
-Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
+Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
const unsigned n = children.size();
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3f7196178..0f8938397 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -159,19 +159,16 @@ class NodeManager {
*/
inline void markForDeletion(expr::NodeValue* nv) {
Assert(nv->d_rc == 0);
+
// if d_reclaiming is set, make sure we don't call
// reclaimZombies(), because it's already running.
- if(d_reclaiming) {// FIXME multithreading
- // currently reclaiming zombies; just push onto the list
- Debug("gc") << "zombifying node value " << nv
- << " [" << nv->d_id << "]: " << *nv
- << " [CURRENTLY-RECLAIMING]\n";
- d_zombies.insert(nv);// FIXME multithreading
- } else {
- Debug("gc") << "zombifying node value " << nv
- << " [" << nv->d_id << "]: " << *nv << "\n";
- d_zombies.insert(nv);// FIXME multithreading
+ Debug("gc") << "zombifying node value " << nv
+ << " [" << nv->d_id << "]: " << *nv
+ << (d_reclaiming ? " [CURRENTLY-RECLAIMING]" : "")
+ << std::endl;
+ d_zombies.insert(nv);// FIXME multithreading
+ if(!d_reclaiming) {// FIXME multithreading
// for now, collect eagerly. can add heuristic here later..
reclaimZombies();
}
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index cd952eef9..a272aaafd 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -81,6 +81,12 @@ enum OptionValue {
* getopt_long() returns the 4th entry
* 4. the return value for getopt_long() when this long option (or the
* value to set the 3rd entry to; see #3)
+ *
+ * If you add something here, you should add it in src/main/usage.h
+ * also, to document it.
+ *
+ * If you add something that has a short option equivalent, you should
+ * add it to the getopt_long() call in parseOptions().
*/
static struct option cmdlineOptions[] = {
// name, has_arg, *flag, val
@@ -91,6 +97,7 @@ static struct option cmdlineOptions[] = {
{ "quiet" , no_argument , NULL, 'q' },
{ "lang" , required_argument, NULL, 'L' },
{ "debug" , required_argument, NULL, 'd' },
+ { "trace" , required_argument, NULL, 't' },
{ "smtcomp" , no_argument , NULL, SMTCOMP },
{ "stats" , no_argument , NULL, STATS },
{ "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
@@ -131,7 +138,7 @@ throw(OptionException) {
// cmdlineOptions specifies all the long-options and the return
// value for getopt_long() should they be encountered.
while((c = getopt_long(argc, argv,
- "+:hVvqL:d:",
+ "+:hVvqL:d:t:",
cmdlineOptions, NULL)) != -1) {
switch(c) {
@@ -171,8 +178,13 @@ throw(OptionException) {
fputs(lang_help, stdout);
exit(1);
+ case 't':
+ Trace.on(optarg);
+ break;
+
case 'd':
Debug.on(optarg);
+ Trace.on(optarg);
/* fall-through */
case STATS:
diff --git a/src/main/usage.h b/src/main/usage.h
index 3a609d2ec..c8ca6a179 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -32,7 +32,8 @@ CVC4 options:\n\
--help | -h this command line reference\n\
--verbose | -v increase verbosity (repeatable)\n\
--quiet | -q decrease verbosity (repeatable)\n\
- --debug | -d debugging for something (e.g. --debug arith)\n\
+ --trace | -t tracing for something (e.g. --trace pushpop)\n\
+ --debug | -d debugging for something (e.g. --debug arith), implies -t\n\
--smtcomp competition mode (very quiet)\n\
--stats give statistics on exit\n\
--segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\
diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp
index a60aaf1cd..244605476 100644
--- a/src/theory/uf/ecdata.cpp
+++ b/src/theory/uf/ecdata.cpp
@@ -10,7 +10,8 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- **
+ ** Implementation of equivalence class data for UF theory. This is a
+ ** context-dependent object.
**/
#include "theory/uf/ecdata.h"
@@ -20,29 +21,27 @@ using namespace context;
using namespace theory;
using namespace uf;
-
ECData::ECData(Context * context, TNode n) :
ContextObj(context),
d_find(this),
d_rep(n),
d_watchListSize(0),
d_first(NULL),
- d_last(NULL)
-{}
-
+ d_last(NULL) {
+}
-bool ECData::isClassRep(){
+bool ECData::isClassRep() {
return this == this->d_find;
}
-void ECData::addPredecessor(TNode n, Context* context){
+void ECData::addPredecessor(TNode n) {
Assert(isClassRep());
makeCurrent();
- Link * newPred = new (context->getCMM()) Link(context, n, d_first);
+ Link * newPred = new(getCMM()) Link(getContext(), n, d_first);
d_first = newPred;
- if(d_last == NULL){
+ if(d_last == NULL) {
d_last = newPred;
}
@@ -62,43 +61,40 @@ void ECData::restore(ContextObj* pContextObj) {
d_watchListSize = data->d_watchListSize;
}
-Node ECData::getRep(){
+Node ECData::getRep() {
return d_rep;
}
-unsigned ECData::getWatchListSize(){
+unsigned ECData::getWatchListSize() {
return d_watchListSize;
}
-
-void ECData::setFind(ECData * ec){
+void ECData::setFind(ECData * ec) {
makeCurrent();
d_find = ec;
}
-ECData * ECData::getFind(){
+ECData* ECData::getFind() {
return d_find;
}
-
-Link* ECData::getFirst(){
+Link* ECData::getFirst() {
return d_first;
}
-
-void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){
+void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) {
Assert(nslave != nmaster);
- Assert(nslave->getFind() == nmaster );
+ Assert(nslave->getFind() == nmaster);
nmaster->makeCurrent();
- nmaster->d_watchListSize += nslave->d_watchListSize;
+ nmaster->d_watchListSize += nslave->d_watchListSize;
- if(nmaster->d_first == NULL){
+ if(nmaster->d_first == NULL) {
nmaster->d_first = nslave->d_first;
nmaster->d_last = nslave->d_last;
- }else if(nslave->d_first != NULL){
- Link * currLast = nmaster->d_last;
+ } else if(nslave->d_first != NULL) {
+ Link* currLast = nmaster->d_last;
currLast->d_next = nslave->d_first;
nmaster->d_last = nslave->d_last;
}
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index 462e713de..bfc7eab8e 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -42,12 +42,14 @@ struct Link {
* Pointer to the next element in linked list.
* This is context dependent.
*/
- context::CDO< Link* > d_next;
+ context::CDO<Link*> d_next;
- /* Link is supposed to be allocated in a region of a ContextMemoryManager.
- * In order to avoid having to decrement the ref count at deletion time,
- * it is preferrable for the user of Link to maintain the invariant that
- * data will survival for the entire scope of the TNode.
+ /**
+ * Link is supposed to be allocated in a region of a
+ * ContextMemoryManager. In order to avoid having to decrement the
+ * ref count at deletion time, it is preferrable for the user of
+ * Link to maintain the invariant that data will survival for the
+ * entire scope of the TNode.
*/
TNode d_data;
@@ -55,9 +57,12 @@ struct Link {
* Creates a new Link w.r.t. a context for the node n.
* An optional parameter is to specify the next element in the link.
*/
- Link(context::Context* context, TNode n, Link * l = NULL):
- d_next(context, l), d_data(n)
- {}
+ Link(context::Context* context, TNode n, Link* l = NULL) :
+ d_next(true, context, l),
+ d_data(n) {
+ Debug("context") << "Link: " << this
+ << " so cdo is " << &d_next << std::endl;
+ }
/**
* Allocates a new Link in the region for the provided ContextMemoryManager.
@@ -67,7 +72,25 @@ struct Link {
return pCMM->newData(size);
}
-};
+private:
+
+ /**
+ * The destructor isn't actually defined. This declaration keeps
+ * the compiler from creating (wastefully) a default definition, and
+ * ensures that we get a link error if someone uses Link in a way
+ * that requires destruction. Objects of class Link should always
+ * be allocated in a ContextMemoryManager, which doesn't call
+ * destructors.
+ */
+ ~Link() throw();
+
+ /**
+ * Just like the destructor, this is not defined. This ensures no
+ * one tries to create a Link on the heap.
+ */
+ static void* operator new(size_t size);
+
+};/* struct Link */
/**
@@ -124,13 +147,16 @@ private:
*/
TNode d_rep;
- /* Watch list datastructures. */
- /** Maintains watch list size for more efficient merging */
+ // Watch list data structures follow
+
+ /**
+ * Maintains watch list size for more efficient merging.
+ */
unsigned d_watchListSize;
/**
- *Pointer to the beginning of the watchlist.
- *This value is NULL iff the watch list is empty.
+ * Pointer to the beginning of the watchlist.
+ * This value is NULL iff the watch list is empty.
*/
Link* d_first;
@@ -143,11 +169,11 @@ private:
*/
Link* d_last;
-
- /** Context dependent operations */
+ /** Context-dependent operation: save this ECData */
context::ContextObj* save(context::ContextMemoryManager* pCMM);
- void restore(context::ContextObj* pContextObj);
+ /** Context-dependent operation: restore this ECData */
+ void restore(context::ContextObj* pContextObj);
public:
/**
@@ -157,15 +183,14 @@ public:
bool isClassRep();
/**
- * Adds a node to the watch list of the equivalence class.
- * Requires a Context in-order to do context dependent memory allocation.
+ * Adds a node to the watch list of the equivalence class. Does
+ * context-dependent memory allocation in the Context with which
+ * this ECData was created.
*
* @param n the node to be added.
* @pre isClassRep() == true
*/
- void addPredecessor(TNode n, context::Context* context);
-
-
+ void addPredecessor(TNode n);
/**
* Creates a EQ with the representative n
@@ -175,6 +200,7 @@ public:
*/
ECData(context::Context* context, TNode n);
+ /** Destructor for ECDatas */
~ECData() {
Debug("ufgc") << "Calling ECData destructor" << std::endl;
destroy();
@@ -189,7 +215,6 @@ public:
*/
static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
-
/**
* Returns the representative of this ECData.
*/
@@ -212,7 +237,6 @@ public:
*/
ECData* getFind();
-
/**
* Sets the find pointer of the equivalence class to be another ECData object.
*
@@ -223,13 +247,10 @@ public:
*/
void setFind(ECData * ec);
-
-}; /* class ECData */
-
+};/* class ECData */
}/* CVC4::theory::uf namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
#endif /* __CVC4__THEORY__UF__ECDATA_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f0d8b47e0..2d7d4e91f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -125,7 +125,7 @@ void TheoryUF::registerTerm(TNode n) {
}
}
- ecChild->addPredecessor(n, getContext());
+ ecChild->addPredecessor(n);
}
}
Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 3e0928baf..0963e4100 100644
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -164,14 +164,14 @@ public:
TS_ASSERT(b.d_pScope == t);
TS_ASSERT(b.d_pContextObjRestore != NULL);
TS_ASSERT(b.d_pContextObjNext == &a);
- //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS
+ TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);
d_context->pop();
TS_ASSERT(s->d_pContext == d_context);
TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
TS_ASSERT(s->d_level == 0);
- //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS
+ TS_ASSERT(s->d_pContextObjList == &c);
TS_ASSERT(a.d_pScope == s);
TS_ASSERT(a.d_pContextObjRestore == NULL);
@@ -181,6 +181,11 @@ public:
TS_ASSERT(b.d_pScope == s);
TS_ASSERT(b.d_pContextObjRestore == NULL);
TS_ASSERT(b.d_pContextObjNext == &a);
- TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
+ TS_ASSERT(b.d_ppContextObjPrev == &c.d_pContextObjNext);
+
+ TS_ASSERT(c.d_pScope == s);
+ TS_ASSERT(c.d_pContextObjRestore == NULL);
+ TS_ASSERT(c.d_pContextObjNext == &b);
+ TS_ASSERT(c.d_ppContextObjPrev == &s->d_pContextObjList);
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback