From: Kshitij Bansal Date: Sat, 7 Dec 2013 00:05:35 +0000 (-0500) Subject: fix bug 542 X-Git-Tag: cvc5-1.0.0~7179^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=220649ac07b8819e3dfbd10127cad633699b8f26;p=cvc5.git fix bug 542 --- 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, 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 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 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::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::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 exportInternal(NodeTemplate 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 expr::exportInternal(NodeTemplate 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 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 \