From c94347913fa464b1ec6a3da2ab21e319c0c42e02 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 29 Sep 2011 05:15:30 +0000
Subject: 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
---
 src/context/context.h | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'src/context/context.h')

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
-- 
cgit v1.2.3