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.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 26 | ||||
-rw-r--r-- | src/expr/node_manager.h | 10 | ||||
-rw-r--r-- | src/expr/type_node.h | 4 |
6 files changed, 29 insertions, 24 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 2dc3aebe5..6d8497a60 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -941,9 +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); - return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode)); + Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); + return n.toExpr(); } 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.h b/src/expr/node.h index 998294da3..c9bfb75a4 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -308,7 +308,7 @@ public: * Destructor. If ref_count is true it will decrement the reference count * and, if zero, collect the NodeValue. */ - ~NodeTemplate() throw(AssertionException); + ~NodeTemplate(); /** * Return the null node. @@ -1089,7 +1089,7 @@ NodeTemplate<ref_count>::NodeTemplate(const Expr& e) { } template <bool ref_count> -NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) { +NodeTemplate<ref_count>::~NodeTemplate() { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); if(ref_count) { // shouldn't ever fail diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d2ac7e2a1..f7e76c06b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -169,6 +169,8 @@ NodeManager::~NodeManager() { for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { d_operators[i] = Node::null(); } + + d_unique_vars.clear(); //d_tupleAndRecordTypes.clear(); d_tt_cache.d_children.clear(); @@ -681,18 +683,18 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } -Node NodeManager::mkSepNil(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::SEP_NIL); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); - return n; -} - -Node* NodeManager::mkSepNilPtr(const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr(); - setAttribute(*n, TypeAttr(), type); - setAttribute(*n, TypeCheckedAttr(), true); - return n; +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_unique_vars[k][type] = n; + Assert( n.getMetaKind() == kind::metakind::VARIABLE ); + return n; + }else{ + return it->second; + } } Node NodeManager::mkAbstractValue(const TypeNode& type) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index dcd7005f8..3c3636d5f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -157,6 +157,9 @@ class NodeManager { * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; + + /** unique vars per (Kind,Type) */ + std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; /** * A list of subscribers for NodeManager events. @@ -486,13 +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. */ - Node mkSepNil(const TypeNode& type); - Node* mkSepNilPtr(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 diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 46fdaa143..0cada0df2 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -116,7 +116,7 @@ public: * Destructor. If ref_count is true it will decrement the reference count * and, if zero, collect the NodeValue. */ - ~TypeNode() throw(AssertionException); + ~TypeNode(); /** * Assignment operator for nodes, copies the relevant information from node @@ -785,7 +785,7 @@ inline TypeNode::TypeNode(const TypeNode& typeNode) { d_nv->inc(); } -inline TypeNode::~TypeNode() throw(AssertionException) { +inline TypeNode::~TypeNode() { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); d_nv->dec(); } |