Document and clean datatypes rewriter (#1437)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 8 Dec 2017 19:54:00 +0000 (13:54 -0600)
committerGitHub <noreply@github.com>
Fri, 8 Dec 2017 19:54:00 +0000 (13:54 -0600)
src/Makefile.am
src/theory/datatypes/datatypes_rewriter.cpp [new file with mode: 0644]
src/theory/datatypes/datatypes_rewriter.h

index 69e9cd014b7aaf4defea4d75b68b42b29d6e022f..ff79cc4a46bc4bd5d57821ec44eba0b06775220c 100644 (file)
@@ -328,6 +328,7 @@ libcvc4_la_SOURCES = \
        theory/bv/theory_bv_utils.cpp \
        theory/bv/theory_bv_utils.h \
        theory/bv/type_enumerator.h \
+       theory/datatypes/datatypes_rewriter.cpp \
        theory/datatypes/datatypes_rewriter.h \
        theory/datatypes/datatypes_sygus.cpp \
        theory/datatypes/datatypes_sygus.h \
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
new file mode 100644 (file)
index 0000000..ff3f759
--- /dev/null
@@ -0,0 +1,921 @@
+/*********************                                                        */
+/*! \file datatypes_rewriter.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of rewriter for the theory of (co)inductive datatypes.
+ **
+ ** Implementation of rewriter for the theory of (co)inductive datatypes.
+ **/
+
+#include "theory/datatypes/datatypes_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+RewriteResponse DatatypesRewriter::postRewrite(TNode in)
+{
+  Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
+  if (in.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    return rewriteConstructor(in);
+  }
+  else if (in.getKind() == kind::APPLY_SELECTOR_TOTAL)
+  {
+    return rewriteSelector(in);
+  }
+  else if (in.getKind() == kind::APPLY_TESTER)
+  {
+    return rewriteTester(in);
+  }
+  else if (in.getKind() == kind::DT_SIZE)
+  {
+    if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
+    {
+      std::vector<Node> children;
+      for (unsigned i = 0; i < in[0].getNumChildren(); i++)
+      {
+        if (in[0][i].getType().isDatatype())
+        {
+          children.push_back(
+              NodeManager::currentNM()->mkNode(kind::DT_SIZE, in[0][i]));
+        }
+      }
+      TNode constructor = in[0].getOperator();
+      size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+      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);
+      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)
+  {
+    if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
+    {
+      std::vector<Node> children;
+      Node res;
+      Rational r = in[1].getConst<Rational>();
+      Rational rmo = Rational(r - Rational(1));
+      for (unsigned i = 0; i < in[0].getNumChildren(); i++)
+      {
+        if (in[0][i].getType().isDatatype())
+        {
+          if (r.isZero())
+          {
+            res = NodeManager::currentNM()->mkConst(false);
+            break;
+          }
+          else
+          {
+            children.push_back(NodeManager::currentNM()->mkNode(
+                kind::DT_HEIGHT_BOUND,
+                in[0][i],
+                NodeManager::currentNM()->mkConst(rmo)));
+          }
+        }
+      }
+      if (res.isNull())
+      {
+        res = children.size() == 0
+                  ? NodeManager::currentNM()->mkConst(true)
+                  : (children.size() == 1 ? children[0]
+                                          : NodeManager::currentNM()->mkNode(
+                                                kind::AND, children));
+      }
+      Trace("datatypes-rewrite")
+          << "DatatypesRewriter::postRewrite: rewrite height " << in << " to "
+          << res << std::endl;
+      return RewriteResponse(REWRITE_AGAIN_FULL, res);
+    }
+  }
+  else if (in.getKind() == 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]);
+      return RewriteResponse(REWRITE_AGAIN_FULL, res);
+    }
+  }
+
+  if (in.getKind() == kind::EQUAL)
+  {
+    if (in[0] == in[1])
+    {
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(true));
+    }
+    else
+    {
+      std::vector<Node> 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;
+      }
+    }
+  }
+
+  return RewriteResponse(REWRITE_DONE, in);
+}
+
+RewriteResponse DatatypesRewriter::preRewrite(TNode in)
+{
+  Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
+  // must prewrite to apply type ascriptions since rewriting does not preserve
+  // types
+  if (in.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    TypeNode tn = in.getType();
+    Type t = tn.toType();
+    DatatypeType dt = DatatypeType(t);
+
+    // check for parametric datatype constructors
+    // to ensure a normal form, all parameteric datatype constructors must have
+    // a type ascription
+    if (dt.isParametric())
+    {
+      if (in.getOperator().getKind() != kind::APPLY_TYPE_ASCRIPTION)
+      {
+        Trace("datatypes-rewrite-debug")
+            << "Ascribing type to parametric datatype constructor " << in
+            << std::endl;
+        Node op = in.getOperator();
+        // get the constructor object
+        const DatatypeConstructor& dtc =
+            Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
+        // create ascribed constructor type
+        Node tc = NodeManager::currentNM()->mkConst(
+            AscriptionType(dtc.getSpecializedConstructorType(t)));
+        Node op_new = NodeManager::currentNM()->mkNode(
+            kind::APPLY_TYPE_ASCRIPTION, tc, op);
+        // make new node
+        std::vector<Node> children;
+        children.push_back(op_new);
+        children.insert(children.end(), in.begin(), in.end());
+        Node inr =
+            NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, children);
+        Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
+        return RewriteResponse(REWRITE_DONE, inr);
+      }
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, in);
+}
+
+RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in)
+{
+  if (in.isConst())
+  {
+    Trace("datatypes-rewrite-debug") << "Normalizing constant " << in
+                                     << std::endl;
+    Node inn = normalizeConstant(in);
+    // constant may be a subterm of another constant, so cannot assume that this
+    // will succeed for codatatypes
+    // Assert( !inn.isNull() );
+    if (!inn.isNull() && inn != in)
+    {
+      Trace("datatypes-rewrite") << "Normalized constant " << in << " -> "
+                                 << inn << std::endl;
+      return RewriteResponse(REWRITE_DONE, inn);
+    }
+    else
+    {
+      return RewriteResponse(REWRITE_DONE, in);
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, in);
+}
+
+RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
+{
+  if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    // Have to be careful not to rewrite well-typed expressions
+    // where the selector doesn't match the constructor,
+    // e.g. "pred(zero)".
+    TypeNode tn = in.getType();
+    TypeNode argType = in[0].getType();
+    TNode selector = in.getOperator();
+    TNode constructor = in[0].getOperator();
+    size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+    const Datatype& dt = Datatype::datatypeOf(selector.toExpr());
+    const DatatypeConstructor& c = dt[constructorIndex];
+    Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : "
+                                     << in;
+    Trace("datatypes-rewrite-debug") << ", cindex = " << constructorIndex
+                                     << ", selector is " << selector
+                                     << std::endl;
+    int selectorIndex = c.getSelectorIndexInternal(selector.toExpr());
+    Trace("datatypes-rewrite-debug") << "Internal selector index is "
+                                     << selectorIndex << std::endl;
+    if (selectorIndex >= 0)
+    {
+      Assert(selectorIndex < (int)c.getNumArgs());
+      if (dt.isCodatatype() && in[0][selectorIndex].isConst())
+      {
+        // must replace all debruijn indices with self
+        Node sub = replaceDebruijn(in[0][selectorIndex], in[0], argType, 0);
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial codatatype selector "
+                                   << in << " to " << sub << std::endl;
+        if (sub != in)
+        {
+          return RewriteResponse(REWRITE_AGAIN_FULL, sub);
+        }
+      }
+      else
+      {
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial selector " << in
+                                   << std::endl;
+        return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
+      }
+    }
+    else
+    {
+      Node gt;
+      bool useTe = true;
+      // if( !tn.isSort() ){
+      //  useTe = false;
+      //}
+      if (tn.isDatatype())
+      {
+        const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
+        useTe = !dta.isCodatatype();
+      }
+      if (useTe)
+      {
+        TypeEnumerator te(tn);
+        gt = *te;
+      }
+      else
+      {
+        gt = tn.mkGroundTerm();
+      }
+      if (!gt.isNull())
+      {
+        // Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+        if (tn.isDatatype() && !tn.isInstantiatedDatatype())
+        {
+          gt = NodeManager::currentNM()->mkNode(
+              kind::APPLY_TYPE_ASCRIPTION,
+              NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())),
+              gt);
+        }
+        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                                   << "Rewrite trivial selector " << in
+                                   << " to distinguished ground term " << gt
+                                   << std::endl;
+        return RewriteResponse(REWRITE_DONE, gt);
+      }
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, in);
+}
+
+RewriteResponse DatatypesRewriter::rewriteTester(TNode in)
+{
+  if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    bool result = Datatype::indexOf(in.getOperator().toExpr())
+                  == Datatype::indexOf(in[0].getOperator().toExpr());
+    Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
+                               << "Rewrite trivial tester " << in << " "
+                               << result << std::endl;
+    return RewriteResponse(REWRITE_DONE,
+                           NodeManager::currentNM()->mkConst(result));
+  }
+  else
+  {
+    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);
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, in);
+}
+
+bool DatatypesRewriter::checkClash(Node n1, Node n2, std::vector<Node>& rew)
+{
+  Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2
+                                   << std::endl;
+  if (n1.getKind() == kind::APPLY_CONSTRUCTOR
+      && n2.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    if (n1.getOperator() != n2.getOperator())
+    {
+      Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " "
+                                       << n2 << " " << n1.getOperator() << " "
+                                       << n2.getOperator() << std::endl;
+      return true;
+    }
+    Assert(n1.getNumChildren() == n2.getNumChildren());
+    for (unsigned i = 0; i < n1.getNumChildren(); i++)
+    {
+      if (checkClash(n1[i], n2[i], rew))
+      {
+        return true;
+      }
+    }
+  }
+  else if (n1 != n2)
+  {
+    if (n1.isConst() && n2.isConst())
+    {
+      Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " "
+                                       << n2 << std::endl;
+      return true;
+    }
+    else
+    {
+      Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
+      rew.push_back(eq);
+    }
+  }
+  return false;
+}
+/** get instantiate cons */
+Node DatatypesRewriter::getInstCons(Node n, const Datatype& dt, int index)
+{
+  Assert(index >= 0 && index < (int)dt.getNumConstructors());
+  std::vector<Node> children;
+  children.push_back(Node::fromExpr(dt[index].getConstructor()));
+  Type t = n.getType().toType();
+  for (unsigned i = 0; i < dt[index].getNumArgs(); i++)
+  {
+    Node nc = NodeManager::currentNM()->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);
+  if (dt.isParametric())
+  {
+    TypeNode tn = TypeNode::fromType(t);
+    // add type ascription for ambiguous constructor types
+    if (!n_ic.getType().isComparableTo(tn))
+    {
+      Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for "
+                                    << n_ic << ", ascribe to " << n.getType()
+                                    << std::endl;
+      Debug("datatypes-parametric") << "Constructor is " << dt[index]
+                                    << std::endl;
+      Type tspec =
+          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);
+      Assert(n_ic.getType() == tn);
+    }
+  }
+  Assert(isInstCons(n, n_ic, dt) == index);
+  // n_ic = Rewriter::rewrite( n_ic );
+  return n_ic;
+}
+
+int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt)
+{
+  if (n.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    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++)
+    {
+      if (n[i].getKind() != kind::APPLY_SELECTOR_TOTAL
+          || n[i].getOperator() != Node::fromExpr(c.getSelectorInternal(nt, i))
+          || n[i][0] != t)
+      {
+        return -1;
+      }
+    }
+    return index;
+  }
+  return -1;
+}
+
+int DatatypesRewriter::isTester(Node n, Node& a)
+{
+  if (options::dtUseTesters())
+  {
+    if (n.getKind() == kind::APPLY_TESTER)
+    {
+      a = n[0];
+      return Datatype::indexOf(n.getOperator().toExpr());
+    }
+  }
+  else
+  {
+    if (n.getKind() == kind::EQUAL)
+    {
+      for (int i = 1; i >= 0; i--)
+      {
+        if (n[i].getKind() == kind::APPLY_CONSTRUCTOR)
+        {
+          const Datatype& dt =
+              Datatype::datatypeOf(n[i].getOperator().toExpr());
+          int ic = isInstCons(n[1 - i], n[i], dt);
+          if (ic != -1)
+          {
+            a = n[1 - i];
+            return ic;
+          }
+        }
+      }
+    }
+  }
+  return -1;
+}
+
+int DatatypesRewriter::isTester(Node n)
+{
+  if (options::dtUseTesters())
+  {
+    if (n.getKind() == kind::APPLY_TESTER)
+    {
+      return Datatype::indexOf(n.getOperator().toExpr());
+    }
+  }
+  else
+  {
+    if (n.getKind() == kind::EQUAL)
+    {
+      for (int i = 1; i >= 0; i--)
+      {
+        if (n[i].getKind() == kind::APPLY_CONSTRUCTOR)
+        {
+          const Datatype& dt =
+              Datatype::datatypeOf(n[i].getOperator().toExpr());
+          int ic = isInstCons(n[1 - i], n[i], dt);
+          if (ic != -1)
+          {
+            return ic;
+          }
+        }
+      }
+    }
+  }
+  return -1;
+}
+
+Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt)
+{
+  if (options::dtUseTesters())
+  {
+    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;
+#else
+    return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
+#endif
+  }
+}
+
+bool DatatypesRewriter::isNullaryApplyConstructor(Node n)
+{
+  Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
+  for (unsigned i = 0; i < n.getNumChildren(); i++)
+  {
+    if (n[i].getType().isDatatype())
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+bool DatatypesRewriter::isNullaryConstructor(const DatatypeConstructor& c)
+{
+  for (unsigned j = 0; j < c.getNumArgs(); j++)
+  {
+    if (c[j].getType().getRangeType().isDatatype())
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+Node DatatypesRewriter::normalizeCodatatypeConstant(Node n)
+{
+  Trace("dt-nconst") << "Normalize " << n << std::endl;
+  std::map<Node, Node> rf;
+  std::vector<Node> sk;
+  std::vector<Node> rf_pending;
+  std::vector<Node> terms;
+  std::map<Node, bool> cdts;
+  Node s = collectRef(n, sk, rf, rf_pending, terms, cdts);
+  if (!s.isNull())
+  {
+    Trace("dt-nconst") << "...symbolic normalized is : " << s << std::endl;
+    for (std::map<Node, Node>::iterator it = rf.begin(); it != rf.end(); ++it)
+    {
+      Trace("dt-nconst") << "  " << it->first << " = " << it->second
+                         << std::endl;
+    }
+    // now run DFA minimization on term structure
+    Trace("dt-nconst") << "  " << terms.size()
+                       << " total subterms :" << std::endl;
+    int eqc_count = 0;
+    std::map<Node, int> eqc_op_map;
+    std::map<Node, int> eqc;
+    std::map<int, std::vector<Node> > eqc_nodes;
+    // partition based on top symbol
+    for (unsigned j = 0; j < terms.size(); j++)
+    {
+      Node t = terms[j];
+      Trace("dt-nconst") << "    " << t << ", cdt=" << cdts[t] << std::endl;
+      int e;
+      if (cdts[t])
+      {
+        Assert(t.getKind() == kind::APPLY_CONSTRUCTOR);
+        Node op = t.getOperator();
+        std::map<Node, int>::iterator it = eqc_op_map.find(op);
+        if (it == eqc_op_map.end())
+        {
+          e = eqc_count;
+          eqc_op_map[op] = eqc_count;
+          eqc_count++;
+        }
+        else
+        {
+          e = it->second;
+        }
+      }
+      else
+      {
+        e = eqc_count;
+        eqc_count++;
+      }
+      eqc[t] = e;
+      eqc_nodes[e].push_back(t);
+    }
+    // partition until fixed point
+    int eqc_curr = 0;
+    bool success = true;
+    while (success)
+    {
+      success = false;
+      int eqc_end = eqc_count;
+      while (eqc_curr < eqc_end)
+      {
+        if (eqc_nodes[eqc_curr].size() > 1)
+        {
+          // look at all nodes in this equivalence class
+          unsigned nchildren = eqc_nodes[eqc_curr][0].getNumChildren();
+          std::map<int, std::vector<Node> > prt;
+          for (unsigned j = 0; j < nchildren; j++)
+          {
+            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++)
+            {
+              Node t = eqc_nodes[eqc_curr][k];
+              Assert(t.getNumChildren() == nchildren);
+              Node tc = t[j];
+              // refer to loops
+              std::map<Node, Node>::iterator itr = rf.find(tc);
+              if (itr != rf.end())
+              {
+                tc = itr->second;
+              }
+              Assert(eqc.find(tc) != eqc.end());
+              prt[eqc[tc]].push_back(t);
+            }
+            if (prt.size() > 1)
+            {
+              success = true;
+              break;
+            }
+          }
+          // move into new eqc(s)
+          for (std::map<int, std::vector<Node> >::iterator it = prt.begin();
+               it != prt.end();
+               ++it)
+          {
+            int e = eqc_count;
+            for (unsigned j = 0; j < it->second.size(); j++)
+            {
+              Node t = it->second[j];
+              eqc[t] = e;
+              eqc_nodes[e].push_back(t);
+            }
+            eqc_count++;
+          }
+        }
+        eqc_nodes.erase(eqc_curr);
+        eqc_curr++;
+      }
+    }
+    // add in already occurring loop variables
+    for (std::map<Node, Node>::iterator it = rf.begin(); it != rf.end(); ++it)
+    {
+      Trace("dt-nconst-debug") << "Mapping equivalence class of " << it->first
+                               << " -> " << it->second << std::endl;
+      Assert(eqc.find(it->second) != eqc.end());
+      eqc[it->first] = eqc[it->second];
+    }
+    // we now have a partition of equivalent terms
+    Trace("dt-nconst") << "Computed equivalence classes ids : " << std::endl;
+    for (std::map<Node, int>::iterator it = eqc.begin(); it != eqc.end(); ++it)
+    {
+      Trace("dt-nconst") << "  " << it->first << " -> " << it->second
+                         << std::endl;
+    }
+    // traverse top-down based on equivalence class
+    std::map<int, int> eqc_stack;
+    return normalizeCodatatypeConstantEqc(s, eqc_stack, eqc, 0);
+  }
+  else
+  {
+    Trace("dt-nconst") << "...invalid." << std::endl;
+    return Node::null();
+  }
+}
+
+// normalize constant : apply to top-level codatatype constants
+Node DatatypesRewriter::normalizeConstant(Node n)
+{
+  TypeNode tn = n.getType();
+  if (tn.isDatatype())
+  {
+    if (tn.isCodatatype())
+    {
+      return normalizeCodatatypeConstant(n);
+    }
+    else
+    {
+      std::vector<Node> children;
+      bool childrenChanged = false;
+      for (unsigned i = 0; i < n.getNumChildren(); i++)
+      {
+        Node nc = normalizeConstant(n[i]);
+        children.push_back(nc);
+        childrenChanged = childrenChanged || nc != n[i];
+      }
+      if (childrenChanged)
+      {
+        return NodeManager::currentNM()->mkNode(n.getKind(), children);
+      }
+      else
+      {
+        return n;
+      }
+    }
+  }
+  else
+  {
+    return n;
+  }
+}
+
+Node DatatypesRewriter::collectRef(Node n,
+                                   std::vector<Node>& sk,
+                                   std::map<Node, Node>& rf,
+                                   std::vector<Node>& rf_pending,
+                                   std::vector<Node>& terms,
+                                   std::map<Node, bool>& cdts)
+{
+  Assert(n.isConst());
+  TypeNode tn = n.getType();
+  Node ret = n;
+  bool isCdt = false;
+  if (tn.isDatatype())
+  {
+    if (!tn.isCodatatype())
+    {
+      // nested datatype within codatatype : can be normalized independently
+      // since all loops should be self-contained
+      ret = normalizeConstant(n);
+    }
+    else
+    {
+      isCdt = true;
+      if (n.getKind() == kind::APPLY_CONSTRUCTOR)
+      {
+        sk.push_back(n);
+        rf_pending.push_back(Node::null());
+        std::vector<Node> children;
+        children.push_back(n.getOperator());
+        bool childChanged = false;
+        for (unsigned i = 0; i < n.getNumChildren(); i++)
+        {
+          Node nc = collectRef(n[i], sk, rf, rf_pending, terms, cdts);
+          if (nc.isNull())
+          {
+            return Node::null();
+          }
+          childChanged = nc != n[i] || childChanged;
+          children.push_back(nc);
+        }
+        sk.pop_back();
+        if (childChanged)
+        {
+          ret = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR,
+                                                 children);
+          if (!rf_pending.back().isNull())
+          {
+            rf[rf_pending.back()] = ret;
+          }
+        }
+        else
+        {
+          Assert(rf_pending.back().isNull());
+        }
+        rf_pending.pop_back();
+      }
+      else
+      {
+        // a loop
+        const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
+        uint32_t index = i.toUnsignedInt();
+        if (index >= sk.size())
+        {
+          return Node::null();
+        }
+        else
+        {
+          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;
+        }
+      }
+    }
+  }
+  Trace("dt-nconst-debug") << "Return term : " << ret << " from " << n
+                           << std::endl;
+  if (std::find(terms.begin(), terms.end(), ret) == terms.end())
+  {
+    terms.push_back(ret);
+    Assert(ret.getType() == tn);
+    cdts[ret] = isCdt;
+  }
+  return ret;
+}
+// eqc_stack stores depth
+Node DatatypesRewriter::normalizeCodatatypeConstantEqc(
+    Node n, std::map<int, int>& eqc_stack, std::map<Node, int>& eqc, int depth)
+{
+  Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n
+                           << " depth=" << depth << std::endl;
+  if (eqc.find(n) == eqc.end())
+  {
+    return n;
+  }
+  else
+  {
+    int e = eqc[n];
+    std::map<int, int>::iterator it = eqc_stack.find(e);
+    if (it != eqc_stack.end())
+    {
+      int debruijn = depth - it->second - 1;
+      return NodeManager::currentNM()->mkConst(
+          UninterpretedConstant(n.getType().toType(), debruijn));
+    }
+    else
+    {
+      std::vector<Node> 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 DatatypesRewriter::replaceDebruijn(Node n,
+                                        Node orig,
+                                        TypeNode orig_tn,
+                                        unsigned depth)
+{
+  if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn)
+  {
+    unsigned index =
+        n.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+    if (index == depth)
+    {
+      return orig;
+    }
+  }
+  else if (n.getNumChildren() > 0)
+  {
+    std::vector<Node> children;
+    bool childChanged = false;
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      Node nc = replaceDebruijn(n[i], orig, orig_tn, depth + 1);
+      children.push_back(nc);
+      childChanged = childChanged || nc != n[i];
+    }
+    if (childChanged)
+    {
+      if (n.hasOperator())
+      {
+        children.insert(children.begin(), n.getOperator());
+      }
+      return NodeManager::currentNM()->mkNode(n.getKind(), children);
+    }
+  }
+  return n;
+}
+
+} /* CVC4::theory::datatypes namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
index 4fcb6d718f5b0873ee13e7ae532155bcb3dfbf9a..dd318765bc9845f8c8c0f3e93ae249b798326e44 100644 (file)
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Rewriter for the theory of inductive datatypes
+ ** \brief Rewriter for the theory of (co)inductive datatypes
  **
- ** Rewriter for the theory of inductive datatypes.
+ ** Rewriter for the theory of (co)inductive datatypes.
  **/
 
 #include "cvc4_private.h"
@@ -29,663 +29,92 @@ namespace theory {
 namespace datatypes {
 
 class DatatypesRewriter {
-
 public:
+ static RewriteResponse postRewrite(TNode in);
+
+ static RewriteResponse preRewrite(TNode in);
+
+ static inline void init() {}
+ static inline void shutdown() {}
+ /** get instantiate cons
+  *
+  * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
+  * where C is the index^{th} constructor of datatype dt.
+  */
+ static Node getInstCons(Node n, const Datatype& dt, int index);
+ /** is instantiation cons
+  *
+  * If this method returns a value >=0, then that value, call it index,
+  * is such that n = C( sel^{C,1}( t ), ..., sel^{C,m}( t ) ),
+  * where C is the index^{th} constructor of dt.
+  */
+ static int isInstCons(Node t, Node n, const Datatype& dt);
+ /** is tester
+  *
+  * This method returns a value >=0 if n is a tester predicate. The return
+  * value indicates the constructor index that the tester n is for. If this
+  * method returns a value >=0, then it updates a to the argument that the
+  * tester n applies to.
+  */
+ static int isTester(Node n, Node& a);
+ /** is tester, same as above but does not update an argument */
+ static int isTester(Node n);
+ /** make tester is-C( n ), where C is the i^{th} constructor of dt */
+ static Node mkTester(Node n, int i, const Datatype& dt);
+ /** returns true iff n is a constructor term with no datatype children */
+ static bool isNullaryApplyConstructor(Node n);
+ /** returns true iff c is a constructor with no datatype children */
+ static bool isNullaryConstructor(const DatatypeConstructor& c);
+ /** normalize codatatype constant
+  *
+  * This returns the normal form of the codatatype constant n. This runs a
+  * DFA minimization algorithm based on the private functions below.
+  */
+ static Node normalizeCodatatypeConstant(Node n);
+ /** normalize constant
+  *
+  * This method returns the normal form of n, which calls the above function
+  * on all top-level codatatype subterms of n.
+  */
+ static Node normalizeConstant(Node n);
+ /** check clash
+  *
+  * This method returns true if and only if n1 and n2 have a skeleton that has
+  * conflicting constructors at some term position.
+  * Examples of terms that clash are:
+  *   C( x, y ) and D( z )
+  *   C( D( x ), y ) and C( E( x ), y )
+  * Examples of terms that do not clash are:
+  *   C( x, y ) and C( D( x ), y )
+  *   C( D( x ), y ) and C( x, E( z ) )
+  *   C( x, y ) and z
+  */
+ static bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
 
-  static RewriteResponse postRewrite(TNode in) {
-    Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl;
-
-    if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
-      /*
-      TypeNode tn = in.getType();
-      Type t = tn.toType();
-      DatatypeType dt = DatatypeType(t);
-      // enable this rewrite if we support subtypes of tuples
-      if( tn.isTuple() ){
-        Node nn = normalizeTupleConstructorApp( in );
-        if( nn!=in ){
-          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: Rewrite tuple constructor " << in << " to " << nn << std::endl;
-          return RewriteResponse(REWRITE_AGAIN_FULL, nn);
-        }
-      }
-      */
-      if( in.isConst() ){
-        Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl;
-        Node inn = normalizeConstant( in );
-        //constant may be a subterm of another constant, so cannot assume that this will succeed for codatatypes
-        //Assert( !inn.isNull() );
-        if( !inn.isNull() && inn!=in ){
-          Trace("datatypes-rewrite") << "Normalized constant " << in << " -> " << inn << std::endl;
-          return RewriteResponse(REWRITE_DONE, inn);
-        }else{
-          return RewriteResponse(REWRITE_DONE, in);
-        }
-      }
-    }
-
-    if(in.getKind() == kind::APPLY_TESTER) {
-      if(in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
-        bool result = Datatype::indexOf(in.getOperator().toExpr()) == Datatype::indexOf(in[0].getOperator().toExpr());
-        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                   << "Rewrite trivial tester " << in
-                                   << " " << result << std::endl;
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(result));
-      } else {
-        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));
-        }
-        //TODO : else if( 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);
-        }
-      }
-    }
-    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
-      // Have to be careful not to rewrite well-typed expressions
-      // where the selector doesn't match the constructor,
-      // e.g. "pred(zero)".
-      TypeNode tn = in.getType();
-      TypeNode argType = in[0].getType();
-      TNode selector = in.getOperator();
-      TNode constructor = in[0].getOperator();
-      size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
-      const Datatype& dt = Datatype::datatypeOf(selector.toExpr());
-      const DatatypeConstructor& c = dt[constructorIndex];
-      Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : " << in;
-      Trace("datatypes-rewrite-debug") << ", cindex = " << constructorIndex << ", selector is " << selector << std::endl;
-      int selectorIndex = c.getSelectorIndexInternal( selector.toExpr() );
-      Trace("datatypes-rewrite-debug") << "Internal selector index is " << selectorIndex << std::endl;
-      if( selectorIndex>=0 ){
-        Assert( selectorIndex<(int)c.getNumArgs() );
-        if( dt.isCodatatype() && in[0][selectorIndex].isConst() ){
-          //must replace all debruijn indices with self  
-          Node sub = replaceDebruijn( in[0][selectorIndex], in[0], argType, 0 );
-          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                     << "Rewrite trivial codatatype selector " << in << " to " << sub << std::endl;
-          if( sub!=in ){
-            return RewriteResponse(REWRITE_AGAIN_FULL, sub );
-          }
-        }else{
-          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                   << "Rewrite trivial selector " << in << std::endl;
-          return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
-        }
-      }else{
-        Node gt;
-        bool useTe = true;
-        //if( !tn.isSort() ){
-        //  useTe = false;
-        //}
-        if( tn.isDatatype() ){
-          const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
-          useTe = !dta.isCodatatype();
-        }
-        if( useTe ){
-          TypeEnumerator te(tn);
-          gt = *te;
-        }else{
-          gt = tn.mkGroundTerm();
-        }
-        if( !gt.isNull() ){
-          //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
-          if( tn.isDatatype() && !tn.isInstantiatedDatatype() ){
-            gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                                                  NodeManager::currentNM()->mkConst(AscriptionType(tn.toType())), gt);
-          }
-          Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
-                                     << "Rewrite trivial selector " << in
-                                     << " to distinguished ground term "
-                                     << gt << std::endl;
-          return RewriteResponse(REWRITE_DONE,gt );
-        }
-      }
-    }
-    if(in.getKind() == kind::DT_SIZE ){
-      if( in[0].getKind()==kind::APPLY_CONSTRUCTOR ){
-        std::vector< Node > children;
-        for( unsigned i=0; i<in[0].getNumChildren(); i++ ){
-          if( in[0][i].getType().isDatatype() ){
-            children.push_back( NodeManager::currentNM()->mkNode( kind::DT_SIZE, in[0][i] ) );
-          }
-        }
-        TNode constructor = in[0].getOperator();
-        size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
-        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);
-        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 ){
-      if( in[0].getKind()==kind::APPLY_CONSTRUCTOR ){
-        std::vector< Node > children;
-        Node res;
-        Rational r = in[1].getConst<Rational>();
-        Rational rmo = Rational( r-Rational(1) );
-        for( unsigned i=0; i<in[0].getNumChildren(); i++ ){
-          if( in[0][i].getType().isDatatype() ){
-            if( r.isZero() ){
-              res = NodeManager::currentNM()->mkConst(false);
-              break;
-            }else{
-              children.push_back( NodeManager::currentNM()->mkNode( kind::DT_HEIGHT_BOUND, in[0][i], NodeManager::currentNM()->mkConst(rmo) ) );
-            }
-          }
-        }
-        if( res.isNull() ){
-          res = children.size()==0 ? NodeManager::currentNM()->mkConst(true) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
-        }
-        Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite height " << in << " to " << res << std::endl;
-        return RewriteResponse(REWRITE_AGAIN_FULL, res );
-      }
-    }else if( in.getKind()==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] );
-        return RewriteResponse(REWRITE_AGAIN_FULL, res );
-      }
-    }
-
-    if(in.getKind() == kind::EQUAL ) {
-      if(in[0] == in[1]) {
-        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-      }else{
-        std::vector< Node > 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;
-        }
-      }
-    }
-
-    return RewriteResponse(REWRITE_DONE, in);
-  }
-
-  static RewriteResponse preRewrite(TNode in) {
-    Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl;
-    //must prewrite to apply type ascriptions since rewriting does not preserve types
-    if(in.getKind() == kind::APPLY_CONSTRUCTOR ){
-      TypeNode tn = in.getType();
-      Type t = tn.toType();
-      DatatypeType dt = DatatypeType(t);
-      
-      //check for parametric datatype constructors
-      // to ensure a normal form, all parameteric datatype constructors must have a type ascription
-      if( dt.isParametric() ){
-        if( in.getOperator().getKind()!=kind::APPLY_TYPE_ASCRIPTION ){
-          Trace("datatypes-rewrite-debug") << "Ascribing type to parametric datatype constructor " << in << std::endl;
-          Node op = in.getOperator();
-          //get the constructor object
-          const DatatypeConstructor& dtc = Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())];
-          //create ascribed constructor type
-          Node tc = NodeManager::currentNM()->mkConst(AscriptionType(dtc.getSpecializedConstructorType(t)));
-          Node op_new = NodeManager::currentNM()->mkNode( kind::APPLY_TYPE_ASCRIPTION, tc, op );
-          //make new node
-          std::vector< Node > children;
-          children.push_back( op_new );
-          children.insert( children.end(), in.begin(), in.end() );
-          Node inr = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-          Trace("datatypes-rewrite-debug") << "Created " << inr << std::endl;
-          return RewriteResponse(REWRITE_DONE, inr);
-        }
-      }
-    }
-    return RewriteResponse(REWRITE_DONE, in);
-  }
-
-  static inline void init() {}
-  static inline void shutdown() {}
-
-  static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
-    Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
-    if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
-      if( n1.getOperator() != n2.getOperator()) {
-        //enable this check if we support subtypes with tuples
-        //if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){
-        Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
-        return true;
-        //}
-      }
-      Assert( n1.getNumChildren() == n2.getNumChildren() );
-      for( unsigned i=0; i<n1.getNumChildren(); i++ ) {
-        if( checkClash( n1[i], n2[i], rew ) ) {
-          return true;
-        }
-      }
-    }else if( n1!=n2 ){
-      if( n1.isConst() && n2.isConst() ){
-        Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " " << n2 << std::endl;
-        return true;
-      }else{
-        Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n1, n2 );
-        rew.push_back( eq );
-      }
-    }
-    return false;
-  }
-  /** get instantiate cons */
-  static Node getInstCons( Node n, const Datatype& dt, int index ) {
-    Assert( index>=0 && index<(int)dt.getNumConstructors() );
-    std::vector< Node > children;
-    children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
-    Type t = n.getType().toType();
-    for( unsigned i=0; i<dt[index].getNumArgs(); i++ ){
-      Node nc = NodeManager::currentNM()->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 );
-    if( dt.isParametric() ){
-      TypeNode tn = TypeNode::fromType( t );
-      //add type ascription for ambiguous constructor types
-      if(!n_ic.getType().isComparableTo(tn)) {
-        Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
-        Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
-        Type tspec = 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 );
-        Assert( n_ic.getType()==tn );
-      }
-    }
-    Assert( isInstCons( n, n_ic, dt )==index );
-    //n_ic = Rewriter::rewrite( n_ic );
-    return n_ic;
-  }
-
-  static int isInstCons( Node t, Node n, const Datatype& dt ){
-    if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
-      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++ ){
-        if( n[i].getKind()!=kind::APPLY_SELECTOR_TOTAL ||
-            n[i].getOperator()!=Node::fromExpr( c.getSelectorInternal( nt, i ) ) ||
-            n[i][0]!=t ){
-          return -1;
-        }
-      }
-      return index;
-    }
-    return -1;
-  }
-
-  static int isTester( Node n, Node& a ) {
-    if( options::dtUseTesters() ){
-      if( n.getKind()==kind::APPLY_TESTER ){
-        a = n[0];
-        return Datatype::indexOf( n.getOperator().toExpr() );
-      }
-    }else{
-      if( n.getKind()==kind::EQUAL ){
-        for( int i=1; i>=0; i-- ){
-          if( n[i].getKind()==kind::APPLY_CONSTRUCTOR ){
-            const Datatype& dt = Datatype::datatypeOf(n[i].getOperator().toExpr());
-            int ic = isInstCons( n[1-i], n[i], dt );
-            if( ic!=-1 ){
-              a = n[1-i];
-              return ic;
-            }
-          }
-        }
-      }
-    }
-    return -1;
-  }
-  static int isTester( Node n ) {
-    if( options::dtUseTesters() ){
-      if( n.getKind()==kind::APPLY_TESTER ){
-        return Datatype::indexOf( n.getOperator().toExpr() );
-      }
-    }else{
-      if( n.getKind()==kind::EQUAL ){
-        for( int i=1; i>=0; i-- ){
-          if( n[i].getKind()==kind::APPLY_CONSTRUCTOR ){
-            const Datatype& dt = Datatype::datatypeOf(n[i].getOperator().toExpr());
-            int ic = isInstCons( n[1-i], n[i], dt );
-            if( ic!=-1 ){
-              return ic;
-            }
-          }
-        }
-      }
-    }
-    return -1;
-  }
-
-  static Node mkTester( Node n, int i, const Datatype& dt ){
-    if( options::dtUseTesters() ){
-      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;
-#else
-      return n.eqNode( DatatypesRewriter::getInstCons( n, dt, i ) );
-#endif
-    }
-  }
-  static bool isNullaryApplyConstructor( Node n ){
-    Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( n[i].getType().isDatatype() ){
-        return false;
-      }
-    }
-    return true;
-  }
-  static bool isNullaryConstructor( const DatatypeConstructor& c ){
-    for( unsigned j=0; j<c.getNumArgs(); j++ ){
-      if( c[j].getType().getRangeType().isDatatype() ){
-        return false;
-      }
-    }
-    return true;
-  }
 private:
-  static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending,
-                          std::vector< Node >& terms, std::map< Node, bool >& cdts ){
-    Assert( n.isConst() );
-    TypeNode tn = n.getType();
-    Node ret = n;
-    bool isCdt = false;
-    if( tn.isDatatype() ){
-      if( !tn.isCodatatype() ){
-        //nested datatype within codatatype : can be normalized independently since all loops should be self-contained
-        ret = normalizeConstant( n );
-      }else{
-        isCdt = true;
-        if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
-          sk.push_back( n );
-          rf_pending.push_back( Node::null() );
-          std::vector< Node > children;
-          children.push_back( n.getOperator() );
-          bool childChanged = false;
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            Node nc = collectRef( n[i], sk, rf, rf_pending, terms, cdts );
-            if( nc.isNull() ){
-              return Node::null();
-            }
-            childChanged = nc!=n[i] || childChanged;
-            children.push_back( nc );
-          }
-          sk.pop_back();
-          if( childChanged ){
-            ret = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-            if( !rf_pending.back().isNull() ){
-              rf[rf_pending.back()] = ret;
-            }
-          }else{
-            Assert( rf_pending.back().isNull() );
-          }
-          rf_pending.pop_back();
-        }else{
-          //a loop
-          const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
-          uint32_t index = i.toUnsignedInt();
-          if( index>=sk.size() ){
-            return Node::null();
-          }else{
-            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;
-          }
-        }
-      }
-    }
-    Trace("dt-nconst-debug") << "Return term : " << ret << " from " << n << std::endl;
-    if( std::find( terms.begin(), terms.end(), ret )==terms.end() ){
-      terms.push_back( ret );
-      Assert( ret.getType()==tn );
-      cdts[ret] = isCdt;
-    }
-    return ret;
-  }
-  //eqc_stack stores depth
-  static Node normalizeCodatatypeConstantEqc( Node n, std::map< int, int >& eqc_stack, std::map< Node, int >& eqc, int depth ){
-    Trace("dt-nconst-debug") << "normalizeCodatatypeConstantEqc: " << n << " depth=" << depth << std::endl;
-    if( eqc.find( n )==eqc.end() ){
-      return n;
-    }else{
-      int e = eqc[n];
-      std::map< int, int >::iterator it = eqc_stack.find( e );
-      if( it!=eqc_stack.end() ){
-        int debruijn = depth - it->second - 1;
-        return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
-      }else{
-        std::vector< Node > 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;
-        }
-      }
-    }
-  }
-  static Node replaceDebruijn( Node n, Node orig, TypeNode orig_tn, unsigned depth ) {
-    if( n.getKind()==kind::UNINTERPRETED_CONSTANT && n.getType()==orig_tn ){
-      unsigned index = n.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
-      if( index==depth ){
-        return orig;
-      }
-    }else if( n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = replaceDebruijn( n[i], orig, orig_tn, depth+1 );
-        children.push_back( nc );
-        childChanged = childChanged || nc!=n[i];
-      }
-      if( childChanged ){
-        if( n.hasOperator() ){
-          children.insert( children.begin(), n.getOperator() );
-        }
-        return NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-    return n;
-  }
-public:
-  static Node normalizeCodatatypeConstant( Node n ){
-    Trace("dt-nconst") << "Normalize " << n << std::endl;
-    std::map< Node, Node > rf;
-    std::vector< Node > sk;
-    std::vector< Node > rf_pending;
-    std::vector< Node > terms;
-    std::map< Node, bool > cdts;
-    Node s = collectRef( n, sk, rf, rf_pending, terms, cdts );
-    if( !s.isNull() ){
-      Trace("dt-nconst") << "...symbolic normalized is : " << s << std::endl;
-      for( std::map< Node, Node >::iterator it = rf.begin(); it != rf.end(); ++it ){
-        Trace("dt-nconst") << "  " << it->first << " = " << it->second << std::endl;
-      }
-      //now run DFA minimization on term structure
-      Trace("dt-nconst") << "  " << terms.size() << " total subterms :" << std::endl;
-      int eqc_count = 0;
-      std::map< Node, int > eqc_op_map;
-      std::map< Node, int > eqc;
-      std::map< int, std::vector< Node > > eqc_nodes;
-      //partition based on top symbol
-      for( unsigned j=0; j<terms.size(); j++ ){
-        Node t = terms[j];
-        Trace("dt-nconst") << "    " << t << ", cdt=" << cdts[t] << std::endl;
-        int e;
-        if( cdts[t] ){
-          Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
-          Node op = t.getOperator();
-          std::map< Node, int >::iterator it = eqc_op_map.find( op );
-          if( it==eqc_op_map.end() ){
-            e = eqc_count;
-            eqc_op_map[op] = eqc_count;
-            eqc_count++;
-          }else{
-            e = it->second;
-          }
-        }else{
-          e = eqc_count;
-          eqc_count++;
-        }
-        eqc[t] = e;
-        eqc_nodes[e].push_back( t );
-      }
-      //partition until fixed point
-      int eqc_curr = 0;
-      bool success = true;
-      while( success ){
-        success = false;
-        int eqc_end = eqc_count;
-        while( eqc_curr<eqc_end ){
-          if( eqc_nodes[eqc_curr].size()>1 ){
-            //look at all nodes in this equivalence class
-            unsigned nchildren = eqc_nodes[eqc_curr][0].getNumChildren();
-            std::map< int, std::vector< Node > > prt;
-            for( unsigned j=0; j<nchildren; j++ ){
-              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++ ){
-                Node t = eqc_nodes[eqc_curr][k];
-                Assert( t.getNumChildren()==nchildren );
-                Node tc = t[j];
-                //refer to loops
-                std::map< Node, Node >::iterator itr = rf.find( tc );
-                if( itr!=rf.end() ){
-                  tc = itr->second;
-                }
-                Assert( eqc.find( tc)!=eqc.end() );
-                prt[eqc[tc]].push_back( t );
-              }
-              if( prt.size()>1 ){
-                success = true;
-                break;
-              }
-            }
-            //move into new eqc(s)
-            for( std::map< int, std::vector< Node > >::iterator it = prt.begin(); it != prt.end(); ++it ){
-              int e = eqc_count;
-              for( unsigned j=0; j<it->second.size(); j++ ){
-                Node t = it->second[j];
-                eqc[t] = e;
-                eqc_nodes[e].push_back( t );
-              }
-              eqc_count++;
-            }
-          }
-          eqc_nodes.erase( eqc_curr );
-          eqc_curr++;
-        }
-      }
-      //add in already occurring loop variables
-      for( std::map< Node, Node >::iterator it = rf.begin(); it != rf.end(); ++it ){
-        Trace("dt-nconst-debug") << "Mapping equivalence class of " << it->first << " -> " << it->second << std::endl;
-        Assert( eqc.find(it->second)!=eqc.end() );
-        eqc[it->first] = eqc[it->second];
-      }
-      //we now have a partition of equivalent terms
-      Trace("dt-nconst") << "Computed equivalence classes ids : " << std::endl;
-      for( std::map< Node, int >::iterator it = eqc.begin(); it != eqc.end(); ++it ){
-        Trace("dt-nconst") << "  " << it->first << " -> " << it->second << std::endl;
-      }
-      //traverse top-down based on equivalence class
-      std::map< int, int > eqc_stack;
-      return normalizeCodatatypeConstantEqc( s, eqc_stack, eqc, 0 );
-    }else{
-      Trace("dt-nconst") << "...invalid." << std::endl;
-      return Node::null();
-    }
-  }
-  static Node normalizeTupleConstructorApp( Node n ){
-    Assert( n.getType().isTuple() );
-    Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
-    const Datatype& dt = n.getType().getDatatype();
-    //may apply a different constructor based on child types
-    std::vector< TypeNode > cht;
-    std::vector< Node > ch;
-    bool childTypeChange = false;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      TypeNode tci = n[i].getType(); 
-      cht.push_back( tci );
-      ch.push_back( n[i] );
-      if( tci!=TypeNode::fromType( dt[0][i].getRangeType() ) ){
-        childTypeChange = true;
-      }
-    }
-    if( childTypeChange ){
-      TypeNode ttn = NodeManager::currentNM()->mkTupleType( cht );
-      const Datatype& dtt = ttn.getDatatype();
-      ch.insert( ch.begin(), Node::fromExpr( dtt[0].getConstructor() ) );
-      return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, ch );
-    }
-    return n;
-  }  
-  //normalize constant : apply to top-level codatatype constants
-  static Node normalizeConstant( Node n ){
-    TypeNode tn = n.getType();
-    if( tn.isDatatype() ){
-      // enable this if we support subtyping with tuples
-      //if( tn.isTuple() ){
-      //  return normalizeTupleConstructorApp( n );
-      //} 
-      if( tn.isCodatatype() ){
-        return normalizeCodatatypeConstant( n );
-      }else{
-        std::vector< Node > children;
-        bool childrenChanged = false;
-        for( unsigned i = 0; i<n.getNumChildren(); i++ ){
-          Node nc = normalizeConstant( n[i] );
-          children.push_back( nc );
-          childrenChanged = childrenChanged || nc!=n[i];
-        }
-        if( childrenChanged ){
-          return NodeManager::currentNM()->mkNode( n.getKind(), children );
-        }else{
-          return n;
-        }
-      }
-    }else{
-      return n;
-    }
-  }
+ /** rewrite constructor term in */
+ static RewriteResponse rewriteConstructor(TNode in);
+ /** rewrite selector term in */
+ static RewriteResponse rewriteSelector(TNode in);
+ /** rewrite tester term in */
+ static RewriteResponse rewriteTester(TNode in);
+
+ /** TODO (#1436) document these */
+ static Node collectRef(Node n,
+                        std::vector<Node>& sk,
+                        std::map<Node, Node>& rf,
+                        std::vector<Node>& rf_pending,
+                        std::vector<Node>& terms,
+                        std::map<Node, bool>& cdts);
+ // eqc_stack stores depth
+ static Node normalizeCodatatypeConstantEqc(Node n,
+                                            std::map<int, int>& eqc_stack,
+                                            std::map<Node, int>& eqc,
+                                            int depth);
+ static Node replaceDebruijn(Node n,
+                             Node orig,
+                             TypeNode orig_tn,
+                             unsigned depth);
 };/* class DatatypesRewriter */
 
 }/* CVC4::theory::datatypes namespace */