diff options
| -rw-r--r-- | src/expr/expr_template.cpp | 33 |
1 files changed, 21 insertions, 12 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 3c867e442..c7ef4754f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -180,7 +180,6 @@ public: } 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)); @@ -194,16 +193,17 @@ public: std::string name; Type type = from->exportType(from_e.getType(), to, vmap); if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { - // temporarily set the node manager to NULL; this gets around - // a check that mkVar isn't called internally - - if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) { - NodeManagerScope nullScope(NULL); - to_e = to->mkBoundVar(name, type);// FIXME thread safety + if (n.getKind() == kind::BOUND_VARIABLE) + { + // bound vars are only available at the Node level (not the Expr + // level) + TypeNode typeNode = TypeNode::fromType(type); + NodeManager* to_nm = NodeManager::fromExprManager(to); + Node n = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety + to_e = n.toExpr(); } else if(n.getKind() == kind::VARIABLE) { bool isGlobal; Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal); - NodeManagerScope nullScope(NULL); to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : flags);// FIXME thread safety } else if(n.getKind() == kind::SKOLEM) { // skolems are only available at the Node level (not the Expr level) @@ -217,10 +217,19 @@ public: Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; } else { - // temporarily set the node manager to NULL; this gets around - // a check that mkVar isn't called internally - NodeManagerScope nullScope(NULL); - to_e = to->mkVar(type);// FIXME thread safety + if (n.getKind() == kind::BOUND_VARIABLE) + { + // bound vars are only available at the Node level (not the Expr + // level) + TypeNode typeNode = TypeNode::fromType(type); + NodeManager* to_nm = NodeManager::fromExprManager(to); + Node n = to_nm->mkBoundVar(typeNode); // FIXME thread safety + to_e = n.toExpr(); + } + else + { + to_e = to->mkVar(type); // FIXME thread safety + } Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; } uint64_t to_int = (uint64_t)(to_e.getNode().d_nv); |