fix bug 534: portfolio define-fun duplicate model

4 files changed, 13 insertions, 11 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index d0bd02c8a..8ae448657 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -467,6 +467,7 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle
     Command* cmd_to_export = *i;
     Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
     seq->addCommand(cmd);
+    Debug("export") << "[export] so far coverted: " << seq << endl;
   }
   seq->d_index = d_index;
   return seq;
@@ -671,7 +672,7 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  Expr func = d_func.exportTo(exprManager, variableMap);
+  Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
   vector<Expr> formals;
   transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
             ExportTransformer(exprManager, variableMap));
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 1b1bc7535..ad9ec49ac 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -115,7 +115,7 @@ namespace expr {
 
 static Node exportConstant(TNode n, NodeManager* to);
 
-Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
+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
@@ -146,7 +146,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
           bool isGlobal;
           Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
           NodeManagerScope nullScope(NULL);
-          to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : ExprManager::VAR_FLAG_NONE);// FIXME thread safety
+          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);
@@ -178,13 +178,13 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
     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));
+      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));
+      children.push_back(exportInternal(*i, from, to, vmap, flags));
     }
     if(Debug.isOn("export")) {
       ExprManagerScope ems(*to);
@@ -199,11 +199,12 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
 
 }/* CVC4::expr namespace */
 
-Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) const {
+Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap,
+                    uint32_t flags /* = 0 */) const {
   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)));
+  return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap, flags)));
 }
 
 Expr& Expr::operator=(const Expr& e) {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 7772de81e..e262fada8 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);
+  NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
 }/* CVC4::expr namespace */
 
 /**
@@ -510,7 +510,7 @@ public:
    * variableMap for the translation and extending it with any new
    * mappings.
    */
-  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) const;
+  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
 
   /**
    * IOStream manipulator to set the maximum depth of Exprs when
@@ -591,7 +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);
+  friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
 
   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 99e1e7ee7..e6a163a8b 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);
+  friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
 
   /** A convenient null-valued encapsulated pointer */
   static NodeTemplate s_null;