From 470c20cd7d12f8de3e9d4e7c38d2ebba1296b098 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 12 Sep 2013 14:44:49 -0400 Subject: fix bug 534: portfolio define-fun duplicate model --- src/expr/command.cpp | 3 ++- src/expr/expr_template.cpp | 13 +++++++------ src/expr/expr_template.h | 6 +++--- src/expr/node.h | 2 +- src/main/command_executor_portfolio.cpp | 5 ++++- src/main/portfolio.cpp | 2 ++ 6 files changed, 19 insertions(+), 12 deletions(-) (limited to 'src') 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 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 exportInternal(NodeTemplate n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + NodeTemplate exportInternal(NodeTemplate 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 expr::exportInternal(NodeTemplate n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + friend NodeTemplate expr::exportInternal(NodeTemplate n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags); friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); template 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; diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 918b554f0..e58df5699 100644 --- 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(cmd) != NULL) { mode = 1; } else if(dynamic_cast(cmd) != NULL || - dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || dynamic_cast(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 263458247..cf8bba1ba 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -38,6 +38,8 @@ int global_winner; template void runThread(int thread_id, boost::function 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() ) { -- cgit v1.2.3