Split term canonize utility to own file and document (#2398)

1 files changed, 199 insertions, 0 deletions

diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/theory/quantifiers/term_canonize.cpp
new file mode 100644
index 000000000..d257198d9
--- /dev/null
+++ b/src/theory/quantifiers/term_canonize.cpp
@@ -0,0 +1,199 @@
+/*********************                                                        */
+/*! \file term_canonize.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 term canonize.
+ **/
+
+#include "theory/quantifiers/term_canonize.h"
+
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {}
+
+int TermCanonize::getIdForOperator(Node op)
+{
+  std::map<Node, int>::iterator it = d_op_id.find(op);
+  if (it == d_op_id.end())
+  {
+    d_op_id[op] = d_op_id_count;
+    d_op_id_count++;
+    return d_op_id[op];
+  }
+  return it->second;
+}
+
+int TermCanonize::getIdForType(TypeNode t)
+{
+  std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
+  if (it == d_typ_id.end())
+  {
+    d_typ_id[t] = d_typ_id_count;
+    d_typ_id_count++;
+    return d_typ_id[t];
+  }
+  return it->second;
+}
+
+bool TermCanonize::getTermOrder(Node a, Node b)
+{
+  if (a.getKind() == BOUND_VARIABLE)
+  {
+    if (b.getKind() == BOUND_VARIABLE)
+    {
+      return a.getAttribute(InstVarNumAttribute())
+             < b.getAttribute(InstVarNumAttribute());
+    }
+    return true;
+  }
+  if (b.getKind() != BOUND_VARIABLE)
+  {
+    Node aop = a.hasOperator() ? a.getOperator() : a;
+    Node bop = b.hasOperator() ? b.getOperator() : b;
+    Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
+    Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
+    if (aop == bop)
+    {
+      if (a.getNumChildren() == b.getNumChildren())
+      {
+        for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
+        {
+          if (a[i] != b[i])
+          {
+            // first distinct child determines the ordering
+            return getTermOrder(a[i], b[i]);
+          }
+        }
+      }
+      else
+      {
+        return aop.getNumChildren() < bop.getNumChildren();
+      }
+    }
+    else
+    {
+      return getIdForOperator(aop) < getIdForOperator(bop);
+    }
+  }
+  return false;
+}
+
+Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i)
+{
+  Assert(!tn.isNull());
+  NodeManager* nm = NodeManager::currentNM();
+  while (d_cn_free_var[tn].size() <= i)
+  {
+    std::stringstream oss;
+    oss << tn;
+    std::string typ_name = oss.str();
+    while (typ_name[0] == '(')
+    {
+      typ_name.erase(typ_name.begin());
+    }
+    std::stringstream os;
+    os << typ_name[0] << i;
+    Node x = nm->mkBoundVar(os.str().c_str(), tn);
+    InstVarNumAttribute ivna;
+    x.setAttribute(ivna, d_cn_free_var[tn].size());
+    d_cn_free_var[tn].push_back(x);
+  }
+  return d_cn_free_var[tn][i];
+}
+
+struct sortTermOrder
+{
+  TermCanonize* d_tu;
+  bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
+};
+
+Node TermCanonize::getCanonicalTerm(TNode n,
+                                    bool apply_torder,
+                                    std::map<TypeNode, unsigned>& var_count,
+                                    std::map<TNode, Node>& visited)
+{
+  std::map<TNode, Node>::iterator it = visited.find(n);
+  if (it != visited.end())
+  {
+    return it->second;
+  }
+
+  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
+  if (n.getKind() == BOUND_VARIABLE)
+  {
+    TypeNode tn = n.getType();
+    // allocate variable
+    unsigned vn = var_count[tn];
+    var_count[tn]++;
+    Node fv = getCanonicalFreeVar(tn, vn);
+    visited[n] = fv;
+    Trace("canon-term-debug") << "...allocate variable." << std::endl;
+    return fv;
+  }
+  else if (n.getNumChildren() > 0)
+  {
+    // collect children
+    Trace("canon-term-debug") << "Collect children" << std::endl;
+    std::vector<Node> cchildren;
+    for (const Node& cn : n)
+    {
+      cchildren.push_back(cn);
+    }
+    // if applicable, first sort by term order
+    if (apply_torder && TermUtil::isComm(n.getKind()))
+    {
+      Trace("canon-term-debug")
+          << "Sort based on commutative operator " << n.getKind() << std::endl;
+      sortTermOrder sto;
+      sto.d_tu = this;
+      std::sort(cchildren.begin(), cchildren.end(), sto);
+    }
+    // now make canonical
+    Trace("canon-term-debug") << "Make canonical children" << std::endl;
+    for (unsigned i = 0, size = cchildren.size(); i < size; i++)
+    {
+      cchildren[i] =
+          getCanonicalTerm(cchildren[i], apply_torder, var_count, visited);
+    }
+    if (n.getMetaKind() == metakind::PARAMETERIZED)
+    {
+      Node op = n.getOperator();
+      op = getCanonicalTerm(op, apply_torder, var_count, visited);
+      Trace("canon-term-debug") << "Insert operator " << op << std::endl;
+      cchildren.insert(cchildren.begin(), op);
+    }
+    Trace("canon-term-debug")
+        << "...constructing for " << n << "." << std::endl;
+    Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
+    Trace("canon-term-debug")
+        << "...constructed " << ret << " for " << n << "." << std::endl;
+    visited[n] = ret;
+    return ret;
+  }
+  Trace("canon-term-debug") << "...return 0-child term." << std::endl;
+  return n;
+}
+
+Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder)
+{
+  std::map<TypeNode, unsigned> var_count;
+  std::map<TNode, Node> visited;
+  return getCanonicalTerm(n, apply_torder, var_count, visited);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4