From: Andrew Reynolds Date: Tue, 30 Jan 2018 17:42:31 +0000 (-0600) Subject: Further clean and document datatypes rewriter (#1548) X-Git-Tag: cvc5-1.0.0~5341 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e4eba43ffa4dd938b7e1153cc42216a42e8ce04;p=cvc5.git Further clean and document datatypes rewriter (#1548) --- diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index ff3f75998..14de0ac6d 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -23,29 +23,30 @@ namespace datatypes { RewriteResponse DatatypesRewriter::postRewrite(TNode in) { Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; - if (in.getKind() == kind::APPLY_CONSTRUCTOR) + Kind k = in.getKind(); + NodeManager* nm = NodeManager::currentNM(); + if (k == kind::APPLY_CONSTRUCTOR) { return rewriteConstructor(in); } - else if (in.getKind() == kind::APPLY_SELECTOR_TOTAL) + else if (k == kind::APPLY_SELECTOR_TOTAL) { return rewriteSelector(in); } - else if (in.getKind() == kind::APPLY_TESTER) + else if (k == kind::APPLY_TESTER) { return rewriteTester(in); } - else if (in.getKind() == kind::DT_SIZE) + else if (k == kind::DT_SIZE) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { std::vector children; - for (unsigned i = 0; i < in[0].getNumChildren(); i++) + for (unsigned i = 0, size = in [0].getNumChildren(); i < size; i++) { if (in[0][i].getType().isDatatype()) { - children.push_back( - NodeManager::currentNM()->mkNode(kind::DT_SIZE, in[0][i])); + children.push_back(nm->mkNode(kind::DT_SIZE, in[0][i])); } } TNode constructor = in[0].getOperator(); @@ -53,17 +54,16 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) const Datatype& dt = Datatype::datatypeOf(constructor.toExpr()); const DatatypeConstructor& c = dt[constructorIndex]; unsigned weight = c.getWeight(); - children.push_back(NodeManager::currentNM()->mkConst(Rational(weight))); - Node res = children.size() == 1 - ? children[0] - : NodeManager::currentNM()->mkNode(kind::PLUS, children); + children.push_back(nm->mkConst(Rational(weight))); + Node res = + children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children); Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite size " << in << " to " << res << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (in.getKind() == kind::DT_HEIGHT_BOUND) + else if (k == kind::DT_HEIGHT_BOUND) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { @@ -71,31 +71,25 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) Node res; Rational r = in[1].getConst(); Rational rmo = Rational(r - Rational(1)); - for (unsigned i = 0; i < in[0].getNumChildren(); i++) + for (unsigned i = 0, size = in [0].getNumChildren(); i < size; i++) { if (in[0][i].getType().isDatatype()) { if (r.isZero()) { - res = NodeManager::currentNM()->mkConst(false); + res = nm->mkConst(false); break; } - else - { - children.push_back(NodeManager::currentNM()->mkNode( - kind::DT_HEIGHT_BOUND, - in[0][i], - NodeManager::currentNM()->mkConst(rmo))); - } + children.push_back( + nm->mkNode(kind::DT_HEIGHT_BOUND, in[0][i], nm->mkConst(rmo))); } } if (res.isNull()) { res = children.size() == 0 - ? NodeManager::currentNM()->mkConst(true) + ? nm->mkConst(true) : (children.size() == 1 ? children[0] - : NodeManager::currentNM()->mkNode( - kind::AND, children)); + : nm->mkNode(kind::AND, children)); } Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite height " << in << " to " @@ -103,53 +97,42 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (in.getKind() == kind::DT_SIZE_BOUND) + else if (k == kind::DT_SIZE_BOUND) { if (in[0].isConst()) { - Node res = NodeManager::currentNM()->mkNode( - kind::LEQ, - NodeManager::currentNM()->mkNode(kind::DT_SIZE, in[0]), - in[1]); + Node res = nm->mkNode(kind::LEQ, nm->mkNode(kind::DT_SIZE, in[0]), in[1]); return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - if (in.getKind() == kind::EQUAL) + if (k == kind::EQUAL) { if (in[0] == in[1]) { - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(true)); + return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); } - else + std::vector rew; + if (checkClash(in[0], in[1], rew)) { - std::vector rew; - if (checkClash(in[0], in[1], rew)) - { - Trace("datatypes-rewrite") << "Rewrite clashing equality " << in - << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(false)); - //}else if( rew.size()==1 && rew[0]!=in ){ - // Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << - // rew[0] << std::endl; - // return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); - } - else if (in[1] < in[0]) - { - Node ins = NodeManager::currentNM()->mkNode(in.getKind(), in[1], in[0]); - Trace("datatypes-rewrite") << "Swap equality " << in << " to " << ins - << std::endl; - return RewriteResponse(REWRITE_DONE, ins); - } - else - { - Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in - << " " << in[0].getKind() << " " - << in[1].getKind() << std::endl; - } + Trace("datatypes-rewrite") + << "Rewrite clashing equality " << in << " to false" << std::endl; + return RewriteResponse(REWRITE_DONE, nm->mkConst(false)); + //}else if( rew.size()==1 && rew[0]!=in ){ + // Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << + // rew[0] << std::endl; + // return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); } + else if (in[1] < in[0]) + { + Node ins = nm->mkNode(in.getKind(), in[1], in[0]); + Trace("datatypes-rewrite") + << "Swap equality " << in << " to " << ins << std::endl; + return RewriteResponse(REWRITE_DONE, ins); + } + Trace("datatypes-rewrite-debug") + << "Did not rewrite equality " << in << " " << in[0].getKind() << " " + << in[1].getKind() << std::endl; } return RewriteResponse(REWRITE_DONE, in); @@ -215,10 +198,7 @@ RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in) << inn << std::endl; return RewriteResponse(REWRITE_DONE, inn); } - else - { - return RewriteResponse(REWRITE_DONE, in); - } + return RewriteResponse(REWRITE_DONE, in); } return RewriteResponse(REWRITE_DONE, in); } @@ -322,33 +302,30 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in) return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(result)); } - else + const Datatype& dt = static_cast(in[0].getType().toType()).getDatatype(); + if (dt.getNumConstructors() == 1) { - const Datatype& dt = DatatypeType(in[0].getType().toType()).getDatatype(); - if (dt.getNumConstructors() == 1) - { - // only one constructor, so it must be - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "only one ctor for " << dt.getName() - << " and that is " << dt[0].getName() - << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(true)); - } - // could try dt.getNumConstructors()==2 && - // Datatype::indexOf(in.getOperator())==1 ? - else if (!options::dtUseTesters()) - { - unsigned tindex = Datatype::indexOf(in.getOperator().toExpr()); - Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality " - << in[0] << " " << tindex << std::endl; - Node neq = mkTester(in[0], tindex, dt); - Assert(neq != in); - Trace("datatypes-rewrite") - << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to " - << neq << std::endl; - return RewriteResponse(REWRITE_AGAIN_FULL, neq); - } + // only one constructor, so it must be + Trace("datatypes-rewrite") + << "DatatypesRewriter::postRewrite: " + << "only one ctor for " << dt.getName() << " and that is " + << dt[0].getName() << std::endl; + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(true)); + } + // could try dt.getNumConstructors()==2 && + // Datatype::indexOf(in.getOperator())==1 ? + else if (!options::dtUseTesters()) + { + unsigned tindex = Datatype::indexOf(in.getOperator().toExpr()); + Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality " + << in[0] << " " << tindex << std::endl; + Node neq = mkTester(in[0], tindex, dt); + Assert(neq != in); + Trace("datatypes-rewrite") + << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to " + << neq << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, neq); } return RewriteResponse(REWRITE_DONE, in); } @@ -368,7 +345,7 @@ bool DatatypesRewriter::checkClash(Node n1, Node n2, std::vector& rew) return true; } Assert(n1.getNumChildren() == n2.getNumChildren()); - for (unsigned i = 0; i < n1.getNumChildren(); i++) + for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) { if (checkClash(n1[i], n2[i], rew)) { @@ -397,18 +374,17 @@ Node DatatypesRewriter::getInstCons(Node n, const Datatype& dt, int index) { Assert(index >= 0 && index < (int)dt.getNumConstructors()); std::vector children; + NodeManager* nm = NodeManager::currentNM(); children.push_back(Node::fromExpr(dt[index].getConstructor())); Type t = n.getType().toType(); - for (unsigned i = 0; i < dt[index].getNumArgs(); i++) + for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++) { - Node nc = NodeManager::currentNM()->mkNode( - kind::APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[index].getSelectorInternal(t, i)), - n); + Node nc = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[index].getSelectorInternal(t, i)), + n); children.push_back(nc); } - Node n_ic = - NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, children); + Node n_ic = nm->mkNode(kind::APPLY_CONSTRUCTOR, children); if (dt.isParametric()) { TypeNode tn = TypeNode::fromType(t); @@ -424,12 +400,10 @@ Node DatatypesRewriter::getInstCons(Node n, const Datatype& dt, int index) dt[index].getSpecializedConstructorType(n.getType().toType()); Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl; - children[0] = NodeManager::currentNM()->mkNode( - kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tspec)), - children[0]); - n_ic = - NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, children); + children[0] = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType(tspec)), + children[0]); + n_ic = nm->mkNode(kind::APPLY_CONSTRUCTOR, children); Assert(n_ic.getType() == tn); } } @@ -445,7 +419,7 @@ int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt) int index = Datatype::indexOf(n.getOperator().toExpr()); const DatatypeConstructor& c = dt[index]; Type nt = n.getType().toType(); - for (unsigned i = 0; i < n.getNumChildren(); i++) + for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) { if (n[i].getKind() != kind::APPLY_SELECTOR_TOTAL || n[i].getOperator() != Node::fromExpr(c.getSelectorInternal(nt, i)) @@ -530,19 +504,16 @@ Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt) return NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n); } - else - { #ifdef CVC4_ASSERTIONS - Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i)); - Node a; - int ii = isTester(ret, a); - Assert(ii == i); - Assert(a == n); - return ret; + Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i)); + Node a; + int ii = isTester(ret, a); + Assert(ii == i); + Assert(a == n); + return ret; #else - return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i)); + return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i)); #endif - } } bool DatatypesRewriter::isNullaryApplyConstructor(Node n) @@ -560,7 +531,7 @@ bool DatatypesRewriter::isNullaryApplyConstructor(Node n) bool DatatypesRewriter::isNullaryConstructor(const DatatypeConstructor& c) { - for (unsigned j = 0; j < c.getNumArgs(); j++) + for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) { if (c[j].getType().getRangeType().isDatatype()) { @@ -595,7 +566,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstant(Node n) std::map eqc; std::map > eqc_nodes; // partition based on top symbol - for (unsigned j = 0; j < terms.size(); j++) + for (unsigned j = 0, size = terms.size(); j < size; j++) { Node t = terms[j]; Trace("dt-nconst") << " " << t << ", cdt=" << cdts[t] << std::endl; @@ -643,7 +614,8 @@ Node DatatypesRewriter::normalizeCodatatypeConstant(Node n) prt.clear(); // partition based on children : for the first child that causes a // split, break - for (unsigned k = 0; k < eqc_nodes[eqc_curr].size(); k++) + for (unsigned k = 0, size = eqc_nodes[eqc_curr].size(); k < size; + k++) { Node t = eqc_nodes[eqc_curr][k]; Assert(t.getNumChildren() == nchildren); @@ -664,14 +636,12 @@ Node DatatypesRewriter::normalizeCodatatypeConstant(Node n) } } // move into new eqc(s) - for (std::map >::iterator it = prt.begin(); - it != prt.end(); - ++it) + for (const std::pair >& p : prt) { int e = eqc_count; - for (unsigned j = 0; j < it->second.size(); j++) + for (unsigned j = 0, size = p.second.size(); j < size; j++) { - Node t = it->second[j]; + Node t = p.second[j]; eqc[t] = e; eqc_nodes[e].push_back(t); } @@ -701,11 +671,8 @@ Node DatatypesRewriter::normalizeCodatatypeConstant(Node n) std::map eqc_stack; return normalizeCodatatypeConstantEqc(s, eqc_stack, eqc, 0); } - else - { - Trace("dt-nconst") << "...invalid." << std::endl; - return Node::null(); - } + Trace("dt-nconst") << "...invalid." << std::endl; + return Node::null(); } // normalize constant : apply to top-level codatatype constants @@ -722,7 +689,7 @@ Node DatatypesRewriter::normalizeConstant(Node n) { std::vector children; bool childrenChanged = false; - for (unsigned i = 0; i < n.getNumChildren(); i++) + for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) { Node nc = normalizeConstant(n[i]); children.push_back(nc); @@ -732,16 +699,9 @@ Node DatatypesRewriter::normalizeConstant(Node n) { return NodeManager::currentNM()->mkNode(n.getKind(), children); } - else - { - return n; - } } } - else - { - return n; - } + return n; } Node DatatypesRewriter::collectRef(Node n, @@ -773,7 +733,7 @@ Node DatatypesRewriter::collectRef(Node n, std::vector children; children.push_back(n.getOperator()); bool childChanged = false; - for (unsigned i = 0; i < n.getNumChildren(); i++) + for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) { Node nc = collectRef(n[i], sk, rf, rf_pending, terms, cdts); if (nc.isNull()) @@ -808,18 +768,15 @@ Node DatatypesRewriter::collectRef(Node n, { return Node::null(); } - else + Assert(sk.size() == rf_pending.size()); + Node r = rf_pending[rf_pending.size() - 1 - index]; + if (r.isNull()) { - Assert(sk.size() == rf_pending.size()); - Node r = rf_pending[rf_pending.size() - 1 - index]; - if (r.isNull()) - { - r = NodeManager::currentNM()->mkBoundVar( - sk[rf_pending.size() - 1 - index].getType()); - rf_pending[rf_pending.size() - 1 - index] = r; - } - return r; + r = NodeManager::currentNM()->mkBoundVar( + sk[rf_pending.size() - 1 - index].getType()); + rf_pending[rf_pending.size() - 1 - index] = r; } + return r; } } } @@ -839,11 +796,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( { Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n << " depth=" << depth << std::endl; - if (eqc.find(n) == eqc.end()) - { - return n; - } - else + if (eqc.find(n) != eqc.end()) { int e = eqc[n]; std::map::iterator it = eqc_stack.find(e); @@ -853,31 +806,24 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( return NodeManager::currentNM()->mkConst( UninterpretedConstant(n.getType().toType(), debruijn)); } - else + std::vector children; + bool childChanged = false; + eqc_stack[e] = depth; + for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) { - std::vector children; - bool childChanged = false; - eqc_stack[e] = depth; - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - Node nc = - normalizeCodatatypeConstantEqc(n[i], eqc_stack, eqc, depth + 1); - children.push_back(nc); - childChanged = childChanged || nc != n[i]; - } - eqc_stack.erase(e); - if (childChanged) - { - Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); - children.insert(children.begin(), n.getOperator()); - return NodeManager::currentNM()->mkNode(n.getKind(), children); - } - else - { - return n; - } + Node nc = normalizeCodatatypeConstantEqc(n[i], eqc_stack, eqc, depth + 1); + children.push_back(nc); + childChanged = childChanged || nc != n[i]; + } + eqc_stack.erase(e); + if (childChanged) + { + Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); + children.insert(children.begin(), n.getOperator()); + return NodeManager::currentNM()->mkNode(n.getKind(), children); } } + return n; } Node DatatypesRewriter::replaceDebruijn(Node n, @@ -898,7 +844,7 @@ Node DatatypesRewriter::replaceDebruijn(Node n, { std::vector children; bool childChanged = false; - for (unsigned i = 0; i < n.getNumChildren(); i++) + for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) { Node nc = replaceDebruijn(n[i], orig, orig_tn, depth + 1); children.push_back(nc); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index dd318765b..fb9c02e94 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -69,6 +69,12 @@ public: * * This returns the normal form of the codatatype constant n. This runs a * DFA minimization algorithm based on the private functions below. + * + * In particular, we first call collectRefs to setup initial information + * about what terms occur in n. Then, we run a DFA minimization algorithm to + * partition these subterms in equivalence classes. Finally, we call + * normalizeCodatatypeConstantEqc to construct the normalized codatatype + * constant that is equivalent to n. */ static Node normalizeCodatatypeConstant(Node n); /** normalize constant @@ -99,18 +105,90 @@ private: /** rewrite tester term in */ static RewriteResponse rewriteTester(TNode in); - /** TODO (#1436) document these */ + /** collect references + * + * This function, given as input a codatatype term n, collects the necessary + * information for constructing a (canonical) codatatype constant that is + * equivalent to n if one exists, or null otherwise. + * + * In particular it returns a term ret such that all non-codatatype datatype + * subterms of n are replaced by a constant that is equal to them via a + * (mutually) recursive call to normalizeConstant above. Additionally, this + * function replaces references to mu-binders with fresh variables. + * In detail, mu-terms are represented by uninterpreted constants of datatype + * type that carry their Debruijn index. + * + * Consider the example of a codatatype representing a stream of integers: + * Stream := cons( head : Int, tail : Stream ) + * The stream 1,0,1,0,1,0... when written in mu-notation is the term: + * mu x. cons( 1, mu y. cons( 0, x ) ) + * This is represented in CVC4 by the Node: + * cons( 1, cons( 0, c[1] ) ) + * where c[1] is a uninterpreted constant datatype with Debruijn index 1, + * indicating that c[1] is nested underneath 1 level on the path to the + * term which it binds. On the other hand, the stream 1,0,0,0,0,... is + * represented by the codatatype term: + * cons( 1, cons( 0, c[0] ) ) + * + * Subterms that are references to mu-binders in n are replaced by a new + * variable. If n contains any subterm that is a reference to a mu-binder not + * bound in n, then we return null. For example we return null when n is: + * cons( 1, cons( 0, c[2] ) ) + * since c[2] is not bound by this codatatype term. + * + * All valid references to mu-binders are replaced by a variable that is unique + * for the term it references. For example, for the infinite tree codatatype: + * Tree : node( data : Int, left : Tree, right : Tree ) + * If n is the term: + * node( 0, c[0], node( 1, c[0], c[1] ) ) + * then the return value ret of this function is: + * node( 0, x, node( 1, y, x ) ) + * where x refers to the root of the term and y refers to the right tree of the + * root. + * + * The argument sk stores the current set of node that we are traversing + * beneath. The argument rf_pending stores, for each node that we are + * traversing beneath either null or the free variable that we are using to + * refer to its mu-binder. The remaining arguments store information that is + * relevant when performing normalization of n using the value of ret: + * + * rf : maps subterms of n to the corresponding term in ret for all subterms + * where the corresponding term in ret is different. + * terms : stores all subterms of ret. + * cdts : for each term t in terms, stores whether t is a codatatype. + */ static Node collectRef(Node n, std::vector& sk, std::map& rf, std::vector& rf_pending, std::vector& terms, std::map& cdts); - // eqc_stack stores depth + /** normalize codatatype constant eqc + * + * This recursive function returns a codatatype constant that is equivalent to + * n based on a pre-computed partition of the subterms of n into equivalence + * classes, as stored in the mapping eqc, which maps the subterms of n to + * equivalence class ids. The arguments eqc_stack and depth store information + * about the traversal in a term we have recursed, where + * + * eqc_stack : maps the depth of each term we have traversed to its equivalence + * class id. + * depth : the number of levels which we have traversed. + */ static Node normalizeCodatatypeConstantEqc(Node n, std::map& eqc_stack, std::map& eqc, int depth); + /** replace debruijn + * + * This function, given codatatype term n, returns a node + * where all subterms of n that have Debruijn indices that refer to a + * term of input depth are replaced by orig. For example, for the infinite Tree + * datatype, + * replaceDebruijn( node( 0, c[0], node( 1, c[0], c[1] ) ), t, Tree, 0 ) + * returns + * node( 0, t, node( 1, c[0], t ) ). + */ static Node replaceDebruijn(Node n, Node orig, TypeNode orig_tn,