diff options
Diffstat (limited to 'src/context/context.h')
| -rw-r--r-- | src/context/context.h | 20 |
1 files changed, 20 insertions, 0 deletions
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 |