fix bug 542

4 files changed, 102 insertions, 79 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index e1578efa7..f7e5498dd 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -116,87 +116,109 @@ namespace expr {
 
 static Node exportConstant(TNode n, NodeManager* to);
 
-Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags) {
-  if(n.isNull()) return Node::null();
-  if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
-    throw ExportUnsupportedException
-       ("export of node belonging to theory of DATATYPES kinds unsupported");
-  }
+class ExportPrivate {
+private:
+  typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
+  ExprManager* from;
+  ExprManager* to;
+  ExprManagerMapCollection& vmap;
+  uint32_t flags;
+  ExportCache exportCache;
+public:
+  ExportPrivate(ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags) : from(from), to(to), vmap(vmap), flags(flags) {}
+  Node exportInternal(TNode n) {
 
-  if(n.getMetaKind() == metakind::CONSTANT) {
-    return exportConstant(n, NodeManager::fromExprManager(to));
-  } else if(n.isVar()) {
-    Expr from_e(from, new Node(n));
-    Expr& to_e = vmap.d_typeMap[from_e];
-    if(! to_e.isNull()) {
-      Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
-      return to_e.getNode();
-    } else {
-      // construct new variable in other manager:
-      // to_e is a ref, so this inserts from_e -> to_e
-      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
-        } 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)
-          TypeNode typeNode = TypeNode::fromType(type);
-          NodeManager* to_nm = NodeManager::fromExprManager(to);
-          Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety
-          to_e = n.toExpr();
+    if(n.isNull()) return Node::null();
+    if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+      throw ExportUnsupportedException
+        ("export of node belonging to theory of DATATYPES kinds unsupported");
+    }
+
+    if(n.getMetaKind() == metakind::CONSTANT) {
+      return exportConstant(n, NodeManager::fromExprManager(to));
+    } else if(n.isVar()) {
+      Expr from_e(from, new Node(n));
+      Expr& to_e = vmap.d_typeMap[from_e];
+      if(! to_e.isNull()) {
+        Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
+        return to_e.getNode();
+      } else {
+        // construct new variable in other manager:
+        // to_e is a ref, so this inserts from_e -> to_e
+        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
+          } 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)
+            TypeNode typeNode = TypeNode::fromType(type);
+            NodeManager* to_nm = NodeManager::fromExprManager(to);
+            Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety
+            to_e = n.toExpr();
+          } else {
+            Unhandled();
+          }
+
+          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 {
-          Unhandled();
+          // 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
+          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);
+        uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
+        vmap.d_from[to_int] = from_int;
+        vmap.d_to[from_int] = to_int;
+        vmap.d_typeMap[to_e] = from_e;// insert other direction too
+        return Node::fromExpr(to_e);
+      }
+    } else {
+      if(exportCache.find(n) != exportCache.end()) {
+        return exportCache[n];
+      }
 
-        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;
+      std::vector<Node> children;
+      Debug("export") << "n: " << n << std::endl;
+      if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
+        children.reserve(n.getNumChildren() + 1);
+        children.push_back(exportInternal(n.getOperator()));
       } 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
-        Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
+        children.reserve(n.getNumChildren());
       }
-      uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
-      uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
-      vmap.d_from[to_int] = from_int;
-      vmap.d_to[from_int] = to_int;
-      vmap.d_typeMap[to_e] = from_e;// insert other direction too
-      return Node::fromExpr(to_e);
-    }
-  } else {
-    std::vector<Node> children;
-    Debug("export") << "n: " << n << std::endl;
-    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
-      children.reserve(n.getNumChildren() + 1);
-      children.push_back(exportInternal(n.getOperator(), from, to, vmap, flags));
-    } else {
-      children.reserve(n.getNumChildren());
-    }
-    for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
-      Debug("export") << "+ child: " << *i << std::endl;
-      children.push_back(exportInternal(*i, from, to, vmap, flags));
-    }
-    if(Debug.isOn("export")) {
-      ExprManagerScope ems(*to);
-      Debug("export") << "children for export from " << n << std::endl;
-      for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
-        Debug("export") << "  child: " << *i << std::endl;
+      for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+        Debug("export") << "+ child: " << *i << std::endl;
+        children.push_back(exportInternal(*i));
       }
+      if(Debug.isOn("export")) {
+        ExprManagerScope ems(*to);
+        Debug("export") << "children for export from " << n << std::endl;
+        for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
+          Debug("export") << "  child: " << *i << std::endl;
+        }
+      }
+
+      // FIXME thread safety
+      Node ret = NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);
+
+      exportCache[n] = ret;
+      return ret;
     }
-    return NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);// FIXME thread safety
-  }
-}/* exportInternal() */
+  }/* exportInternal() */
+
+};
 
 }/* CVC4::expr namespace */
 
@@ -205,7 +227,7 @@ Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variable
   Assert(d_exprManager != exprManager,
          "No sense in cloning an Expr in the same ExprManager");
   ExprManagerScope ems(*this);
-  return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap, flags)));
+  return Expr(exprManager, new Node(expr::ExportPrivate(d_exprManager, exprManager, variableMap, flags).exportInternal(*d_node)));
 }
 
 Expr& Expr::operator=(const Expr& e) {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index ace14a10b..756145bda 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -81,7 +81,7 @@ namespace expr {
   class CVC4_PUBLIC ExprDag;
   class CVC4_PUBLIC ExprSetLanguage;
 
-  NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
+  class ExportPrivate;
 }/* CVC4::expr namespace */
 
 /**
@@ -591,8 +591,7 @@ private:
   friend class TypeCheckingException;
   friend class expr::pickle::Pickler;
   friend class prop::TheoryProxy;
-  friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
-
+  friend class expr::ExportPrivate;
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
   template <bool ref_count> friend class NodeTemplate;
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 1c13c4674..a6914aedb 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -182,7 +182,7 @@ class NodeTemplate {
   friend class expr::NodeValue;
 
   friend class expr::pickle::PicklerPrivate;
-  friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
+  friend class expr::ExportPrivate;
 
   /** A convenient null-valued encapsulated pointer */
   static NodeTemplate s_null;
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index d516e3d69..2e722b297 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -46,9 +46,11 @@ TESTS =	\
 	miplib3.cvc \
 	miplib4.cvc \
 	miplibtrick.smt
-#	prp-13-24.smt2
 #	problem__003.smt2
 
+# Takes more than 10 seconds on debug build, move it to regress1:
+#	prp-13-24.smt2  (takes move than 30 seconds)
+
 EXTRA_DIST = $(TESTS) \
 	miplib-opt1217--27.smt \
 	miplib-opt1217--27.smt2 \