diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 870408939..1ae9f1e8e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -102,8 +102,15 @@ class NodeManager { Options* d_options; StatisticsRegistry* d_statisticsRegistry; + ResourceManager* d_resourceManager; + /** + * A list of registrations on d_options to that call into d_resourceManager. + * These must be garbage collected before d_options and d_resourceManager. + */ + ListenerRegistrationList* d_registrations; + NodeValuePool d_nodeValuePool; size_t next_id; @@ -295,6 +302,8 @@ class NodeManager { // undefined private copy constructor (disallow copy) NodeManager(const NodeManager&) CVC4_UNDEFINED; + NodeManager& operator=(const NodeManager&) CVC4_UNDEFINED; + void init(); /** |