From d43e5fb294d89ba69f7d2607a12c8700b7ec9345 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 14 Sep 2016 16:41:27 -0500 Subject: Support for unique variable generation in node manager. --- src/expr/node_manager.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/expr/node_manager.h') 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 -- cgit v1.2.3