Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

18 files changed, 816 insertions, 43 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index 9e349a06b..ca5772d7c 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -18,4 +18,8 @@ libcontext_la_SOURCES = \
 	cdmap_forward.h \
 	cdset.h \
 	cdset_forward.h \
-	cdvector.h
+	cdcirclist.h \
+	cdcirclist_forward.h \
+	cdvector.h \
+	stacking_map.h \
+	stacking_vector.h
diff --git a/src/context/cdcirclist.h b/src/context/cdcirclist.h
new file mode 100644
index 000000000..cc6b60217
--- /dev/null
+++ b/src/context/cdcirclist.h
@@ -0,0 +1,418 @@
+/*********************                                                        */
+/*! \file cdcirclist.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context-dependent circular list class
+ **
+ ** Context-dependent circular list class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDCIRCLIST_H
+#define __CVC4__CONTEXT__CDCIRCLIST_H
+
+#include <iterator>
+#include <memory>
+#include <string>
+#include <sstream>
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdcirclist_forward.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+// CDO for pointers in particular, adds * and -> operators
+template <class T>
+class CDPtr : public CDO<T*> {
+  typedef CDO<T*> super;
+
+  // private copy ctor
+  CDPtr(const CDPtr<T>& cdptr) :
+    super(cdptr) {
+  }
+
+public:
+
+  CDPtr(Context* context, T* data = NULL) :
+    super(context, data) {
+  }
+
+  CDPtr(bool allocatedInCMM, Context* context, T* data = NULL) :
+    super(allocatedInCMM, context, data) {
+  }
+
+  // undesirable to put this here, since CDO<> does it already (?)
+  virtual ~CDPtr() throw(AssertionException) { this->destroy(); }
+
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    Debug("context") << "save cdptr " << this << " (value " << super::get() << ")";
+    ContextObj* p = new(pCMM) CDPtr<T>(*this);
+    Debug("context") << " to " << p << std::endl;
+    return p;
+  }
+
+  virtual void restore(ContextObj* pContextObj) {
+    Debug("context") << "restore cdptr " << this << " (using " << pContextObj << ") from " << super::get();
+    this->super::restore(pContextObj);
+    Debug("context") << " to " << super::get() << std::endl;
+  }
+
+  CDPtr<T>& operator=(T* data) {
+    Debug("context") << "set " << this << " from " << super::get();
+    super::set(data);
+    Debug("context") << " to " << super::get() << std::endl;
+    return *this;
+  }
+  // assignment is just like using the underlying ptr
+  CDPtr<T>& operator=(const CDPtr<T>& cdptr) {
+    return *this = cdptr.get();
+  }
+
+  T& operator*() { return *super::get(); }
+  T* operator->() { return super::get(); }
+  const T& operator*() const { return *super::get(); }
+  const T* operator->() const { return super::get(); }
+};/* class CDPtr<T> */
+
+
+/**
+ * Class representing a single link in a CDCircList<>.
+ *
+ * The underlying T object is immutable, only the structure of the
+ * list is mutable, so only that's backtracked.
+ */
+template <class T, class AllocatorT>
+class CDCircElement {
+  typedef CDCircElement<T, AllocatorT> elt_t;
+  const T d_t;
+  CDPtr<elt_t> d_prev;
+  CDPtr<elt_t> d_next;
+  friend class CDCircList<T, AllocatorT>;
+public:
+  CDCircElement(Context* context, const T& t,
+                elt_t* prev = NULL, elt_t* next = NULL) :
+    d_t(t),
+    d_prev(true, context, prev),
+    d_next(true, context, next) {
+  }
+
+  CDPtr<elt_t>& next() { return d_next; }
+  CDPtr<elt_t>& prev() { return d_prev; }
+  elt_t* next() const { return d_next; }
+  elt_t* prev() const { return d_prev; }
+  T element() const { return d_t; }
+};/* class CDCircElement<> */
+
+
+/**
+ * Generic context-dependent circular list.  Items themselves are not
+ * context dependent, only the forward and backward links.  This
+ * allows two lists to be spliced together in constant time (see
+ * concat()).  The list *structure* is mutable (things can be spliced
+ * in, removed, added, the list can be cleared, etc.) in a
+ * context-dependent manner, but the list items are immutable.  To
+ * replace an item A in the list with B, A must be removed and
+ * B added in the same location.
+ */
+template <class T, class AllocatorT>
+class CDCircList : public ContextObj {
+public:
+
+  /** List carrier element type */
+  typedef CDCircElement<T, AllocatorT> elt_t;
+  /** The value type with which this CDCircList<> was instantiated. */
+  typedef T value_type;
+  /** The allocator type with which this CDCircList<> was instantiated. */
+  typedef AllocatorT Allocator;
+
+private:
+
+  /** Head element of the circular list */
+  CDPtr<elt_t> d_head;
+  /** The context with which we're associated */
+  Context* d_context;
+  /** Our allocator */
+  typename Allocator::template rebind< CDCircElement<T, AllocatorT> >::other d_allocator;
+
+public:
+
+  CDCircList(Context* context, const Allocator& alloc = Allocator()) :
+    ContextObj(context),
+    d_head(context, NULL),
+    d_context(context),
+    d_allocator(alloc) {
+  }
+
+  CDCircList(bool allocatedInCMM, Context* context, const Allocator& alloc = Allocator()) :
+    ContextObj(allocatedInCMM, context),
+    d_head(allocatedInCMM, context, NULL),
+    d_context(context),
+    d_allocator(alloc) {
+    Debug("cdcirclist") << "head " << &d_head << " in cmm ? " << allocatedInCMM << std::endl;
+  }
+
+  ~CDCircList() throw(AssertionException) {
+    // by context contract, call destroy() here
+    destroy();
+  }
+
+  void clear() {
+    d_head = NULL;
+  }
+
+  bool empty() const {
+    return d_head == NULL;
+  }
+
+  CDPtr<elt_t>& head() {
+    return d_head;
+  }
+
+  CDPtr<elt_t>& tail() {
+    return empty() ? d_head : d_head->d_prev;
+  }
+
+  const elt_t* head() const {
+    return d_head;
+  }
+
+  const elt_t* tail() const {
+    return empty() ? d_head : d_head->d_prev;
+  }
+
+  T front() const {
+    Assert(! empty());
+    return head()->element();
+  }
+
+  T back() const {
+    Assert(! empty());
+    return tail()->element();
+  }
+
+  void push_back(const T& t) {
+    if(Debug.isOn("cdcirclist:paranoid")) {
+      debugCheck();
+    }
+    // FIXME LEAK! (should alloc in CMM, no?)
+    elt_t* x = d_allocator.allocate(1);
+    if(empty()) {
+      // zero-element case
+      new(x) elt_t(d_context, t, x, x);
+      d_head = x;
+    } else {
+      // N-element case
+      new(x) elt_t(d_context, t, d_head->d_prev, d_head);
+      d_head->d_prev->d_next = x;
+      d_head->d_prev = x;
+    }
+  }
+
+  /**
+   * Concatenate two lists.  This modifies both: afterward, the two
+   * lists might have different heads, but they will have the same
+   * elements in the same (circular) order.
+   */
+  void concat(CDCircList<T, AllocatorT>& l) {
+    Assert(this != &l, "cannot concat a list with itself");
+
+    if(d_head == NULL) {
+      d_head = l.d_head;
+      return;
+    } else if(l.d_head == NULL) {
+      l.d_head = d_head;
+      return;
+    }
+
+    // splice together the two circular lists
+    CDPtr<elt_t> &l1head = head(), &l2head = l.head();
+    CDPtr<elt_t> &l1tail = tail(), &l2tail = l.tail();
+    // l2tail will change underneath us in what's below (because it's
+    // the same as l2head->prev()), so we have to keep a regular
+    // pointer to it
+    elt_t* oldl2tail = l2tail;
+
+    Debug("cdcirclist") << "concat1 " << this << " " << &l << std::endl;
+    l1tail->next() = l2head;
+    Debug("cdcirclist") << "concat2" << std::endl;
+    l2head->prev() = l1tail;
+
+    Debug("cdcirclist") << "concat3" << std::endl;
+    oldl2tail->next() = l1head;
+    Debug("cdcirclist") << "concat4" << std::endl;
+    l1head->prev() = oldl2tail;
+    Debug("cdcirclist") << "concat5" << std::endl;
+  }
+
+  class iterator {
+    const CDCircList<T, AllocatorT>* d_list;
+    const elt_t* d_current;
+    friend class CDCircList<T, AllocatorT>;
+  public:
+    iterator(const CDCircList<T, AllocatorT>* list, const elt_t* first) :
+      d_list(list),
+      d_current(first) {
+    }
+    iterator(const iterator& other) :
+      d_list(other.d_list),
+      d_current(other.d_current) {
+    }
+
+    bool operator==(const iterator& other) const {
+      return d_list == other.d_list && d_current == other.d_current;
+    }
+    bool operator!=(const iterator& other) const {
+      return !(*this == other);
+    }
+    iterator& operator++() {
+      Assert(d_current != NULL, "iterator already off the end");
+      if(d_current == d_list->tail()) {
+        d_current = NULL;
+      } else {
+        d_current = d_current->next();
+      }
+      return *this;
+    }
+    iterator operator++(int) {
+      const elt_t* old = d_current;
+      ++*this;
+      return iterator(d_list, old);
+    }
+    iterator& operator--() {
+      // undefined to go off the beginning, but don't have a check for that
+      if(d_current == NULL) {
+        d_current = d_list->tail();
+      } else {
+        d_current = d_current->prev();
+      }
+      return *this;
+    }
+    iterator operator--(int) {
+      const elt_t* old = d_current;
+      --*this;
+      return iterator(d_list, old);
+    }
+    T operator*() {
+      Assert(d_current != NULL, "iterator already off the end");
+      return d_current->element();
+    }
+  };/* class CDCircList<>::iterator */
+
+  // list elements are immutable
+  typedef iterator const_iterator;
+
+  iterator begin() {
+    if(Debug.isOn("cdcirclist:paranoid")) {
+      debugCheck();
+    }
+    return iterator(this, head());
+  }
+
+  iterator end() {
+    if(Debug.isOn("cdcirclist:paranoid")) {
+      debugCheck();
+    }
+    return iterator(this, NULL);
+  }
+
+  const_iterator begin() const {
+    return const_iterator(this, head());
+  }
+
+  const_iterator end() const {
+    return const_iterator(this, NULL);
+  }
+
+  iterator erase(iterator pos) {
+    Assert(pos.d_current != NULL);
+    if(pos.d_current->prev() == pos.d_current) {
+      // one-elt list
+      d_head = NULL;
+      return iterator(this, NULL);
+    } else {
+      // N-elt list
+      if(pos.d_current == d_head) {
+        // removing list head
+        elt_t *pHead = head(), *pTail = tail();
+        pTail->next() = pHead->next();
+        pHead->next()->prev() = pTail;
+        d_head = pHead->next();
+        return iterator(this, d_head);
+        // can't free old head, because of backtracking
+      } else {
+        // not removing list head
+        const elt_t *elt = pos.d_current;
+        elt_t *prev = pos.d_current->prev();
+        prev->next() = elt->next();
+        elt->next()->prev() = prev;
+        return iterator(this, elt->next());
+        // can't free elt, because of backtracking
+      }
+    }
+  }
+
+private:
+
+  // do not permit copy/assignment
+  CDCircList(const CDCircList<T, AllocatorT>&) CVC4_UNUSED;
+  CDCircList<T, AllocatorT>& operator=(const CDCircList<T, AllocatorT>&) CVC4_UNUSED;
+
+public:
+  /** Check internal structure and invariants of the list */
+  void debugCheck() const {
+    elt_t* p = d_head;
+    Debug("cdcirclist") << "this is " << this << std::endl;
+    if(p == NULL) {
+      Debug("cdcirclist") << "head[" << &d_head << "] is NULL : " << d_context->getLevel() << std::endl;
+      // empty list
+      return;
+    }
+    Debug("cdcirclist") << "head[" << &d_head << "] is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << d_context->getLevel() << std::endl;//p->d_t << std::endl;
+    do {
+      elt_t* p_last = p;
+      p = p->d_next;
+      if(p == NULL) {
+        Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, next == NULL ******" << std::endl;
+        break;
+      }
+      Debug("cdcirclist") << "   p is " << p << " next " << p->d_next << " prev " << p->d_prev << " : " << std::endl;//p->d_t << std::endl;
+      if(p->d_prev != p_last) {
+        Debug("cdcirclist") << "****** ERROR ON LINE ABOVE, prev != last ******" << std::endl;
+      }
+      //Assert(p->d_prev == p_last);
+      Assert(p != NULL);
+    } while(p != d_head);
+  }
+
+private:
+
+  // Nothing to save; the elements take care of themselves
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    Unreachable();
+  }
+
+  // Similarly, nothing to restore
+  virtual void restore(ContextObj* data) {
+    Unreachable();
+  }
+
+};/* class CDCircList<> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDCIRCLIST_H */
diff --git a/src/context/cdcirclist_forward.h b/src/context/cdcirclist_forward.h
new file mode 100644
index 000000000..56a39e96f
--- /dev/null
+++ b/src/context/cdcirclist_forward.h
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file cdcirclist_forward.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the
+ ** CDCircList<> template
+ **
+ ** This is a forward declaration header to declare the CDCircList<>
+ ** template.  It's useful if you want to forward-declare CDCircList<>
+ ** without including the full cdcirclist.h header, for example, in a
+ ** public header context, or to keep compile times low when only a
+ ** forward declaration is needed.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H
+#define __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H
+
+#include <memory>
+
+namespace __gnu_cxx {
+  template <class Key> struct hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+  namespace context {
+    template <class T>
+    class ContextMemoryAllocator;
+
+    template <class T, class Allocator = ContextMemoryAllocator<T> >
+    class CDCircList;
+  }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDCIRCLIST_FORWARD_H */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index c999ecadb..dea9f8be7 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -3,17 +3,18 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): barrett, taking
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Context-dependent list class.
+ ** \brief Context-dependent list class (only supports append)
  **
- ** Context-dependent list class.
+ ** Context-dependent list class.  This list only supports appending
+ ** to the list; on backtrack, the list is simply shortened.
  **/
 
 #include "cvc4_private.h"
diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h
index 45a44756d..fcb51fe20 100644
--- a/src/context/cdlist_context_memory.h
+++ b/src/context/cdlist_context_memory.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index a1e50c7c8..90c439085 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index c71459835..3ac99f729 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): taking, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h
index 214d9e700..331d6a93e 100644
--- a/src/context/cdmap_forward.h
+++ b/src/context/cdmap_forward.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/cdo.h b/src/context/cdo.h
index f4c4a7e29..025e8e337 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -40,13 +40,29 @@ class CDO : public ContextObj {
    */
   T d_data;
 
+protected:
+
+  /**
+   * Copy constructor - it's private to ensure it is only used by save().
+   * Basic CDO objects, cannot be copied-they have to be unique.
+   */
+  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
+
+  /**
+   * operator= for CDO is private to ensure CDO object is not copied.
+   */
+  CDO<T>& operator=(const CDO<T>& cdo) CVC4_UNUSED;
+
   /**
    * Implementation of mandatory ContextObj method save: simply copies the
    * current data to a copy using the copy constructor.  Memory is allocated
    * using the ContextMemoryManager.
    */
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDO<T>(*this);
+    Debug("context") << "save cdo " << this << " (value " << get() << ")";
+    ContextObj* p = new(pCMM) CDO<T>(*this);
+    Debug("context") << " to " << p << std::endl;
+    return p;
   }
 
   /**
@@ -54,20 +70,11 @@ class CDO : public ContextObj {
    * saved data back from the saved copy using operator= for T.
    */
   virtual void restore(ContextObj* pContextObj) {
+    //Debug("context") << "restore cdo " << this << " from " << get();
     d_data = ((CDO<T>*) pContextObj)->d_data;
+    //Debug("context") << " to " << get() << std::endl;
   }
 
-  /**
-   * Copy constructor - it's private to ensure it is only used by save().
-   * Basic CDO objects, cannot be copied-they have to be unique.
-   */
-  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
-
-  /**
-   * operator= for CDO is private to ensure CDO object is not copied.
-   */
-  CDO<T>& operator=(const CDO<T>& cdo);
-
 public:
 
   /**
@@ -75,7 +82,8 @@ public:
    * value of d_data.
    */
   CDO(Context* context) :
-    ContextObj(context) {
+    ContextObj(context),
+    d_data(T()) {
   }
 
   /**
@@ -90,7 +98,8 @@ public:
    * allocating contextual objects with non-standard allocators."
    */
   CDO(bool allocatedInCMM, Context* context) :
-    ContextObj(allocatedInCMM, context) {
+    ContextObj(allocatedInCMM, context),
+    d_data(T()) {
   }
 
   /**
@@ -100,7 +109,8 @@ public:
    * is assigned by the default constructor for T
    */
   CDO(Context* context, const T& data) :
-    ContextObj(context) {
+    ContextObj(context),
+    d_data(T()) {
     makeCurrent();
     d_data = data;
   }
@@ -119,7 +129,8 @@ public:
    * allocating contextual objects with non-standard allocators."
    */
   CDO(bool allocatedInCMM, Context* context, const T& data) :
-    ContextObj(allocatedInCMM, context) {
+    ContextObj(allocatedInCMM, context),
+    d_data(T()) {
     makeCurrent();
     d_data = data;
   }
diff --git a/src/context/cdset.h b/src/context/cdset.h
index 268c3127b..8699d9cf4 100644
--- a/src/context/cdset.h
+++ b/src/context/cdset.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/cdset_forward.h b/src/context/cdset_forward.h
index af3c6f85c..2339552a6 100644
--- a/src/context/cdset_forward.h
+++ b/src/context/cdset_forward.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index cb86d5c4d..49d1b67e9 100644
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 9b40e9780..2b220d5b4 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: barrett
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -78,8 +78,10 @@ void Context::pop() {
   // Notify the (pre-pop) ContextNotifyObj objects
   ContextNotifyObj* pCNO = d_pCNOpre;
   while(pCNO != NULL) {
+    // pre-store the "next" pointer in case pCNO deletes itself on notify()
+    ContextNotifyObj* next = pCNO->d_pCNOnext;
     pCNO->notify();
-    pCNO = pCNO->d_pCNOnext;
+    pCNO = next;
   }
 
   // Grab the top Scope
@@ -97,8 +99,10 @@ void Context::pop() {
   // Notify the (post-pop) ContextNotifyObj objects
   pCNO = d_pCNOpost;
   while(pCNO != NULL) {
+    // pre-store the "next" pointer in case pCNO deletes itself on notify()
+    ContextNotifyObj* next = pCNO->d_pCNOnext;
     pCNO->notify();
-    pCNO = pCNO->d_pCNOnext;
+    pCNO = next;
   }
 
   Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
@@ -135,6 +139,7 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
 
 void ContextObj::update() throw(AssertionException) {
   Debug("context") << "before update(" << this << "):" << std::endl
+                   << "context is " << getContext() << std::endl
                    << *getContext() << std::endl;
 
   // Call save() to save the information in the current object
@@ -203,6 +208,7 @@ ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
     // Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
     //        "Expected bottom scope");
 
+    Debug("context") << "NULL restore object! " << this << std::endl;
     pContextObjNext = d_pContextObjNext;
 
     // Nothing else to do
@@ -261,22 +267,28 @@ void ContextObj::destroy() throw(AssertionException) {
 
 
 ContextObj::ContextObj(Context* pContext) :
-  d_pContextObjRestore(NULL) {
+  d_pScope(NULL),
+  d_pContextObjRestore(NULL),
+  d_pContextObjNext(NULL),
+  d_ppContextObjPrev(NULL) {
 
   Assert(pContext != NULL, "NULL context pointer");
 
-  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+  Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
   d_pScope = pContext->getBottomScope();
   d_pScope->addToChain(this);
 }
 
 
 ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
-  d_pContextObjRestore(NULL) {
+  d_pScope(NULL),
+  d_pContextObjRestore(NULL),
+  d_pContextObjNext(NULL),
+  d_ppContextObjPrev(NULL) {
 
   Assert(pContext != NULL, "NULL context pointer");
 
-  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+  Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
   if(allocatedInCMM) {
     d_pScope = pContext->getTopScope();
   } else {
@@ -326,12 +338,15 @@ std::ostream& operator<<(std::ostream& out,
 
 std::ostream& operator<<(std::ostream& out,
                          const Scope& scope) throw(AssertionException) {
-  out << "Scope " << scope.d_level << ":";
+  out << "Scope " << scope.d_level << " [" << &scope << "]:";
   ContextObj* pContextObj = scope.d_pContextObjList;
   Assert(pContextObj == NULL ||
          pContextObj->prev() == &scope.d_pContextObjList);
   while(pContextObj != NULL) {
     out << " <--> " << pContextObj;
+    if(pContextObj->d_pScope != &scope) {
+      out << " XXX bad scope" << std::endl;
+    }
     Assert(pContextObj->d_pScope == &scope);
     Assert(pContextObj->next() == NULL ||
            pContextObj->next()->prev() == &pContextObj->next());
diff --git a/src/context/context.h b/src/context/context.h
index 34107ef29..1e69964a0 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: barrett
- ** Minor contributors (to current version): taking, dejan
+ ** Minor contributors (to current version): dejan, taking
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index fde69a149..aea2fe9c2 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 56ef7ab59..66db21424 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -161,10 +161,11 @@ public:
   };
 
   ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {}
-  ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.d_mm) {}
+  template <class U>
+  ContextMemoryAllocator(const ContextMemoryAllocator<U>& alloc) throw() : d_mm(alloc.getCMM()) {}
   ~ContextMemoryAllocator() throw() {}
 
-  ContextMemoryManager* getCMM() { return d_mm; }
+  ContextMemoryManager* getCMM() const { return d_mm; }
   T* address(T& v) const { return &v; }
   T const* address(T const& v) const { return &v; }
   size_t max_size() const throw() {
diff --git a/src/context/stacking_map.h b/src/context/stacking_map.h
new file mode 100644
index 000000000..2dec1845c
--- /dev/null
+++ b/src/context/stacking_map.h
@@ -0,0 +1,162 @@
+/*********************                                                        */
+/*! \file stacking_map.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Backtrackable map using an undo stack
+ **
+ ** Backtrackable map using an undo stack rather than storing items in
+ ** a CDMap<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__STACKING_MAP_H
+#define __CVC4__CONTEXT__STACKING_MAP_H
+
+#include <utility>
+#include <vector>
+#include <ext/hash_map>
+
+#include "expr/node.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class T>
+struct StackingMapArgType {
+  typedef T argtype;
+};/* struct StackingMapArgType<T> */
+
+template <>
+struct StackingMapArgType<Node> {
+  typedef TNode argtype;
+};/* struct StackingMapArgType<Node> */
+
+
+template <class KeyType, class ValueType, class KeyHash>
+struct StackingMapRestoreValue {
+  typedef typename StackingMapArgType<KeyType>::argtype ArgType;
+  static void restore(__gnu_cxx::hash_map<KeyType, ValueType, KeyHash>& map, const ArgType& k, const ValueType& v) {
+    map[k] = v;
+  }
+};/* struct StackingMapRestoreValue<KeyType, ValueType, KeyHash> */
+
+template <class KeyType, class KeyHash>
+struct StackingMapRestoreValue<KeyType, Node, KeyHash> {
+  typedef typename StackingMapArgType<KeyType>::argtype ArgType;
+  static void restore(__gnu_cxx::hash_map<KeyType, Node, KeyHash>& map, const ArgType& k, TNode v) {
+    if(v.isNull()) {
+      map.erase(k);
+    } else {
+      map[k] = v;
+    }
+  }
+};/* struct StackingMapRestoreValue<KeyType, Node, KeyHash> */
+
+template <class KeyType, class KeyHash>
+struct StackingMapRestoreValue<KeyType, TNode, KeyHash> {
+  typedef typename StackingMapArgType<KeyType>::argtype ArgType;
+  static void restore(__gnu_cxx::hash_map<KeyType, TNode, KeyHash>& map, const ArgType& k, TNode v) {
+    if(v.isNull()) {
+      map.erase(k);
+    } else {
+      map[k] = v;
+    }
+  }
+};/* struct StackingMapRestoreValue<KeyType, TNode, KeyHash> */
+
+
+template <class KeyType, class ValueType, class KeyHash>
+class StackingMap : context::ContextNotifyObj {
+  /** Our underlying map type. */
+  typedef __gnu_cxx::hash_map<KeyType, ValueType, KeyHash> MapType;
+
+  /**
+   * The type for arguments being passed in.  It's the same as
+   * KeyType, unless KeyType is Node, then it's TNode for efficiency.
+   */
+  typedef typename StackingMapArgType<KeyType>::argtype ArgType;
+
+  /** Our map of keys to their values. */
+  MapType d_map;
+
+  /** Our undo stack for changes made to d_map. */
+  std::vector<std::pair<ArgType, ValueType> > d_trace;
+
+  /** Our current offset in the d_trace stack (context-dependent). */
+  context::CDO<size_t> d_offset;
+
+public:
+  typedef typename MapType::const_iterator const_iterator;
+
+  StackingMap(context::Context* ctxt) :
+    context::ContextNotifyObj(ctxt),
+    d_offset(ctxt, 0) {
+  }
+
+  ~StackingMap() throw() { }
+
+  const_iterator find(ArgType n) const { return d_map.find(n); }
+  const_iterator end() const { return d_map.end(); }
+
+  /**
+   * Return a key's value in the key-value map.  If n is not a key in
+   * the map, this function returns a default-constructed value.
+   */
+  ValueType operator[](ArgType n) const {
+    const_iterator it = find(n);
+    if(it == end()) {
+      return ValueType();
+    } else {
+      return (*it).second;
+    }
+  }
+  //ValueType& operator[](ArgType n) { return d_map[n]; }// not permitted--bypasses set() logic
+
+  /**
+   * Set the value in the key-value map for Node n to newValue.
+   */
+  void set(ArgType n, const ValueType& newValue);
+
+  /**
+   * Called by the Context when a pop occurs.  Cancels everything to the
+   * current context level.  Overrides ContextNotifyObj::notify().
+   */
+  void notify();
+
+};/* class StackingMap<> */
+
+template <class KeyType, class ValueType, class KeyHash>
+void StackingMap<KeyType, ValueType, KeyHash>::set(ArgType n, const ValueType& newValue) {
+  Trace("sm") << "SM setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl;
+  ValueType& ref = d_map[n];
+  d_trace.push_back(std::make_pair(n, ValueType(ref)));
+  d_offset = d_trace.size();
+  ref = newValue;
+}
+
+template <class KeyType, class ValueType, class KeyHash>
+void StackingMap<KeyType, ValueType, KeyHash>::notify() {
+  Trace("sm") << "SM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl;
+  while(d_offset < d_trace.size()) {
+    std::pair<ArgType, ValueType> p = d_trace.back();
+    StackingMapRestoreValue<KeyType, ValueType, KeyHash>::restore(d_map, p.first, p.second);
+    d_trace.pop_back();
+  }
+  Trace("sm") << "SM cancelling finished." << std::endl;
+}
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__CONTEXT__STACKING_MAP_H */
diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h
new file mode 100644
index 000000000..9987731d4
--- /dev/null
+++ b/src/context/stacking_vector.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file stacking_vector.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Backtrackable vector using an undo stack
+ **
+ ** Backtrackable vector using an undo stack rather than storing items in
+ ** a CDVector<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__STACKING_VECTOR_H
+#define __CVC4__CONTEXT__STACKING_VECTOR_H
+
+#include <utility>
+#include <vector>
+
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class T>
+class StackingVector : context::ContextNotifyObj {
+  /** Our underlying map type. */
+  typedef std::vector<T> VectorType;
+
+  /** Our map of indices to their values. */
+  VectorType d_map;
+
+  /** Our undo stack for changes made to d_map. */
+  std::vector<std::pair<size_t, T> > d_trace;
+
+  /** Our current offset in the d_trace stack (context-dependent). */
+  context::CDO<size_t> d_offset;
+
+public:
+  typedef typename VectorType::const_iterator const_iterator;
+
+  StackingVector(context::Context* ctxt) :
+    context::ContextNotifyObj(ctxt),
+    d_offset(ctxt, 0) {
+  }
+
+  ~StackingVector() throw() { }
+
+  /**
+   * Return a value from the vector.  If n is not a key in
+   * the map, this function returns a default-constructed T.
+   */
+  T operator[](size_t n) const {
+    return n < d_map.size() ? d_map[n] : T();
+  }
+  //T& operator[](ArgType n) { return d_map[n]; }// not permitted--bypasses set() logic
+
+  /**
+   * Set the value in the key-value map for Node n to newValue.
+   */
+  void set(size_t n, const T& newValue);
+
+  /**
+   * Return the current size of the vector.  Note that once a certain
+   * size is achieved, the size never goes down again, although the
+   * elements off the old end of the vector will be replaced with
+   * default-constructed T values.
+   */
+  size_t size() const {
+    return d_map.size();
+  }
+
+  /**
+   * Called by the Context when a pop occurs.  Cancels everything to the
+   * current context level.  Overrides ContextNotifyObj::notify().
+   */
+  void notify();
+
+};/* class StackingVector<> */
+
+template <class T>
+void StackingVector<T>::set(size_t n, const T& newValue) {
+  Trace("sv") << "SV setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl;
+  if(n >= d_map.size()) {
+    d_map.resize(n + 1);
+  }
+  T& ref = d_map[n];
+  d_trace.push_back(std::make_pair(n, T(ref)));
+  d_offset = d_trace.size();
+  ref = newValue;
+}
+
+template <class T>
+void StackingVector<T>::notify() {
+  Trace("sv") << "SV cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl;
+  while(d_offset < d_trace.size()) {
+    std::pair<size_t, T> p = d_trace.back();
+    Trace("sv") << "SV cancelling: " << p.first << " back to " << p.second << std::endl;
+    d_map[p.first] = p.second;
+    d_trace.pop_back();
+  }
+  Trace("sv") << "SV cancelling finished." << std::endl;
+}
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__CONTEXT__STACKING_VECTOR_H */