diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /src/context | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
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
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/cdmap.h | 4 | ||||
-rw-r--r-- | src/context/context.h | 20 |
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 |