From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 31 Aug 2018 20:08:40 +0000 (-0500)
Subject: Fix export of bound variables (#2409)
X-Git-Tag: cvc5-1.0.0~4694
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b48be52459c358267ca19f4e134fe22b850f425;p=cvc5.git

Fix export of bound variables (#2409)
---

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);