fix bug 534: portfolio define-fun duplicate model

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index d0bd02c8a845b12ed9cf5f1d002a30cc6a6e7585..8ae448657723d6c94fa74ec44fdb56f37f043434 100644 (file)
--- 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 1b1bc7535739aea72faefa4a84ee46d29107873d..ad9ec49ac5ab4b79c26cbb89d0d5add0781fed0c 100644 (file)
--- 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 7772de81eb33b8586f1b0f108a30ad8e67414fe4..e262fada8c7afaf034307b12540af1ef89e1321f 100644 (file)
--- 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 99e1e7ee708de5134f3133556cd38120e115281e..e6a163a8b701086a2b818707fb55f836d3f005ab 100644 (file)
--- 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;

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 918b554f0ff458e0b5da6805b5e50501b4fcb2cb..e58df5699ca2ce38d3a3d7f2013c9c5991ad262b 100644 (file)
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -187,7 +187,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
      dynamic_cast<QueryCommand*>(cmd) != NULL) {
     mode = 1;
   } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
-            dynamic_cast<GetModelCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
             dynamic_cast<GetModelCommand*>(cmd) != NULL ||
             dynamic_cast<GetProofCommand*>(cmd) != NULL ||
@@ -199,6 +198,10 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     mode = 2;
   }
 
+  Debug("portfolio::outputmode") << "Mode is " << mode
+                                 << "lastWinner is " << d_lastWinner 
+                                 << "d_seq is " << d_seq << std::endl;
+
   if(mode == 0) {
     d_seq->addCommand(cmd->clone());
     Command* cmdExported = 

diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 263458247e8ec4e256a3e7bccf03ef9b6e877cb7..cf8bba1ba324fe13a94fe5b04c9c9450d2f3bf42 100644 (file)
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -38,6 +38,8 @@ int global_winner;
 template<typename S>
 void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue)
 {
+  /* Uncommment line to delay first thread, useful to unearth errors/debug */
+  // if(thread_id == 0) { sleep(1); }
   returnValue = threadFn();
 
   if( mutex_done.try_lock() ) {