From 08d6ec676189826f99756f9245186ee9de7dbc36 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 14 Apr 2017 17:03:44 -0500 Subject: [PATCH] Fix bug related to portfolio with nullary operators. --- src/expr/expr_template.cpp | 7 ++++++- src/expr/node_manager.cpp | 6 +++--- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 4fbb0cd33..806650e57 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -137,7 +137,12 @@ public: return to->mkConst(::CVC4::EmptySet(type)); } return exportConstant(n, NodeManager::fromExprManager(to), vmap); - } else if(n.isVar()) { + } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){ + Expr from_e(from, new Node(n)); + Type type = from->exportType(from_e.getType(), to, vmap); + NodeManagerScope nullScope(NULL); + return to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety + } else if(n.getMetaKind() == metakind::VARIABLE) { Expr from_e(from, new Node(n)); Expr& to_e = vmap.d_typeMap[from_e]; if(! to_e.isNull()) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7cf228403..e9e92a5b1 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -459,7 +459,7 @@ TypeNode NodeManager::getType(TNode n, bool check) /* The check should have happened, if we asked for it. */ Assert( !check || getAttribute(n, TypeCheckedAttr()) ); - Debug("getType") << "type of " << n << " is " << typeNode << endl; + Debug("getType") << "type of " << &n << " " << n << " is " << typeNode << endl; return typeNode; } @@ -799,10 +799,10 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { //setAttribute(n, TypeCheckedAttr(), true); d_unique_vars[k][type] = n; Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR ); - Trace("ajr-temp") << this << "...made nullary operator " << n << std::endl; + Trace("ajr-temp") << this << "...made nullary operator " << n << " " << &n << " " << type << std::endl; return n; }else{ - Trace("ajr-temp") << this << "...reuse nullary operator " << it->second << std::endl; + Trace("ajr-temp") << this << "...reuse nullary operator " << it->second << " " << &( it->second ) << std::endl; return it->second; } } -- 2.30.2