diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 79c7320f7..3c3636d5f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -158,8 +158,8 @@ class NodeManager { */ Node d_operators[kind::LAST_KIND]; - /** sep nil per type */ - std::map< TypeNode, Node > d_sep_nils; + /** unique vars per (Kind,Type) */ + std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; /** * A list of subscribers for NodeManager events. @@ -489,12 +489,12 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - - /** Create nil reference for separation logic with the given type (unique per type). */ - Node mkSepNil(const TypeNode& type); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); + + /** make unique (per Type,Kind) variable. */ + Node mkUniqueVar(const TypeNode& type, Kind k); /** * Create a constant of type T. It will have the appropriate |