diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
commit | 75db964b0c56f1a3b04b77c33d226c4d9cd0ca54 (patch) | |
tree | c30f7f17ae963e3f51cef111b2d549eacff1a852 /src/expr/node_manager.cpp | |
parent | e6e02c32c58f9e5edde2dd85fc7b19ef001eea03 (diff) |
Add nullary operator metakind.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index ebf78f541..2a819935d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -315,7 +315,7 @@ void NodeManager::reclaimZombies() { // remove from the pool kind::MetaKind mk = nv->getMetaKind(); - if(mk != kind::metakind::VARIABLE) { + if(mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) { poolRemove(nv); } @@ -787,14 +787,15 @@ Node NodeManager::mkBooleanTermVariable() { return n; } -Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { +Node NodeManager::mkNullaryOperator(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); + //should type check it + //n.setAttribute(TypeCheckedAttr(), true); d_unique_vars[k][type] = n; - Assert( n.getMetaKind() == kind::metakind::VARIABLE ); + Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR ); return n; }else{ return it->second; |