Support for unique variable generation in node manager.

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