diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 13:43:02 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-12 13:43:02 -0500 |
commit | 442c809911bcc45ae45dc97650146c459a841ea3 (patch) | |
tree | 1a08cc6448314cc494d63414d8b47713afa5ebf0 /src/expr/node_manager.cpp | |
parent | 14fb8fac59e368a36e936a2d0497745eda72c637 (diff) |
Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d2ac7e2a1..94b136c46 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_sep_nils.clear(); //d_tupleAndRecordTypes.clear(); d_tt_cache.d_children.clear(); @@ -682,17 +684,16 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { } 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; + 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); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + d_sep_nils[type] = n; + return n; + }else{ + return it->second; + } } Node NodeManager::mkAbstractValue(const TypeNode& type) { |