diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 5 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 13 | ||||
-rw-r--r-- | src/expr/node_manager.h | 10 |
4 files changed, 16 insertions, 16 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index aa5634e7a..6d8497a60 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -941,11 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) { return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); } -Expr ExprManager::mkSepNil(Type type) { +Expr ExprManager::mkUniqueVar(Type type, Kind k){ NodeManagerScope nms(d_nodeManager); - Node n = d_nodeManager->mkSepNil(*type.d_typeNode); + Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); return n.toExpr(); - //return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); } Expr ExprManager::mkAssociative(Kind kind, diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f30b720de..95b9c60bf 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -547,9 +547,9 @@ public: Expr mkBoundVar(Type type); /** - * Create a (nameless) new nil reference for separation logic of type + * Create unique variable of type */ - Expr mkSepNil(Type type); + Expr mkUniqueVar( Type type, Kind k); /** Get a reference to the statistics registry for this ExprManager */ Statistics getStatistics() const throw(); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 94b136c46..f7e76c06b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -170,7 +170,7 @@ NodeManager::~NodeManager() { d_operators[i] = Node::null(); } - d_sep_nils.clear(); + d_unique_vars.clear(); //d_tupleAndRecordTypes.clear(); d_tt_cache.d_children.clear(); @@ -683,13 +683,14 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } -Node NodeManager::mkSepNil(const TypeNode& type) { - std::map< TypeNode, Node >::iterator it = d_sep_nils.find( type ); - if( it==d_sep_nils.end() ){ - Node n = NodeBuilder<0>(this, kind::SEP_NIL); +Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { + std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); + if( it==d_unique_vars[k].end() ){ + Node n = NodeBuilder<0>(this, k); n.setAttribute(TypeAttr(), type); n.setAttribute(TypeCheckedAttr(), true); - d_sep_nils[type] = n; + d_unique_vars[k][type] = n; + Assert( n.getMetaKind() == kind::metakind::VARIABLE ); return n; }else{ return it->second; 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 |