Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.

I also expect this commit to fix bug #273.

No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863

2 files changed, 24 insertions, 0 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 3ac99f729..2a5365082 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -364,6 +364,10 @@ public:
     return d_map.size();
   }
 
+  bool empty() const {
+    return d_map.empty();
+  }
+
   size_t count(const Key& k) const {
     return d_map.count(k);
   }
diff --git a/src/context/context.h b/src/context/context.h
index 1e69964a0..78c06e7d5 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -95,6 +95,10 @@ class Context {
   friend std::ostream&
   operator<<(std::ostream&, const Context&) throw(AssertionException);
 
+  // disable copy, assignment
+  Context(const Context&) CVC4_UNUSED;
+  Context& operator=(const Context&) CVC4_UNUSED;
+
 public:
   /**
    * Constructor: create ContextMemoryManager and initial Scope
@@ -153,6 +157,22 @@ public:
 
 };/* class Context */
 
+
+/**
+ * A UserContext is different from a Context only because it's used for
+ * different purposes---so separating the two types gives type errors where
+ * appropriate.
+ */
+class UserContext : public Context {
+private:
+  // disable copy, assignment
+  UserContext(const UserContext&) CVC4_UNUSED;
+  UserContext& operator=(const UserContext&) CVC4_UNUSED;
+public:
+  UserContext() {}
+};/* class UserContext */
+
+
 /**
  * Conceptually, a Scope encapsulates that portion of the context that
  * changes after a call to push() and must be undone on a subsequent call to