diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-15 22:11:11 +0000 |
| commit | e45de2ba8a8c34d3212327ed6f021462c149825c (patch) | |
| tree | eb82e6d1a3bc9b133d501ff89742384156a64b3b /src/expr/expr_manager_template.h | |
| parent | 225f4e77f3afdebdfa046834ef7c006b9b8ec77c (diff) | |
partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.
Diffstat (limited to 'src/expr/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 83d306871..f51d6fa28 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -80,8 +80,12 @@ private: /** ExprManagerScope reaches in to get the NodeManager */ friend class ExprManagerScope; - // undefined, private copy constructor (disallow copy) + /** NodeManager reaches in to get the NodeManager */ + friend class NodeManager; + + // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) CVC4_UNDEFINED; + ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; public: |