diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-12 14:44:49 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-12 14:44:49 -0400 |
| commit | 470c20cd7d12f8de3e9d4e7c38d2ebba1296b098 (patch) | |
| tree | eba01503e16a20ac5eb1f4e44e7f87aa4b16acbd /src/expr/expr_template.cpp | |
| parent | 28ec8ce392a815c47689ecd86b5b91f9a58104e5 (diff) | |
fix bug 534: portfolio define-fun duplicate model
Diffstat (limited to 'src/expr/expr_template.cpp')
| -rw-r--r-- | src/expr/expr_template.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
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) { |