Move some generic utilities out of quantifiers (#3139)

5 files changed, 600 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 61ab7b3fb..300af8e8c 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -16,6 +16,8 @@ libcvc4_add_sources(
   expr_stream.h
   kind_map.h
   matcher.h
+  match_trie.cpp
+  match_trie.h
   node.cpp
   node.h
   node_algorithm.cpp
@@ -37,6 +39,8 @@ libcvc4_add_sources(
   pickler.h
   symbol_table.cpp
   symbol_table.h
+  term_canonize.cpp
+  term_canonize.h
   type.cpp
   type.h
   type_checker.h
diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp
new file mode 100644
index 000000000..363c78c9e
--- /dev/null
+++ b/src/expr/match_trie.cpp
@@ -0,0 +1,199 @@
+/*********************                                                        */
+/*! \file match_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Implements a match trie, also known as a discrimination tree.
+ **/
+
+#include "expr/match_trie.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace expr {
+
+bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
+{
+  std::vector<Node> vars;
+  std::vector<Node> subs;
+  std::map<Node, Node> smap;
+
+  std::vector<std::vector<Node> > visit;
+  std::vector<MatchTrie*> visit_trie;
+  std::vector<int> visit_var_index;
+  std::vector<bool> visit_bound_var;
+
+  visit.push_back(std::vector<Node>{n});
+  visit_trie.push_back(this);
+  visit_var_index.push_back(-1);
+  visit_bound_var.push_back(false);
+  while (!visit.empty())
+  {
+    std::vector<Node> cvisit = visit.back();
+    MatchTrie* curr = visit_trie.back();
+    if (cvisit.empty())
+    {
+      Assert(n
+             == curr->d_data.substitute(
+                 vars.begin(), vars.end(), subs.begin(), subs.end()));
+      Trace("match-debug") << "notify : " << curr->d_data << std::endl;
+      if (!ntm->notify(n, curr->d_data, vars, subs))
+      {
+        return false;
+      }
+      visit.pop_back();
+      visit_trie.pop_back();
+      visit_var_index.pop_back();
+      visit_bound_var.pop_back();
+    }
+    else
+    {
+      Node cn = cvisit.back();
+      Trace("match-debug") << "traverse : " << cn << " at depth "
+                           << visit.size() << std::endl;
+      unsigned index = visit.size() - 1;
+      int vindex = visit_var_index[index];
+      if (vindex == -1)
+      {
+        if (!cn.isVar())
+        {
+          Node op = cn.hasOperator() ? cn.getOperator() : cn;
+          unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
+          std::map<unsigned, MatchTrie>::iterator itu =
+              curr->d_children[op].find(nchild);
+          if (itu != curr->d_children[op].end())
+          {
+            // recurse on the operator or self
+            cvisit.pop_back();
+            if (cn.hasOperator())
+            {
+              for (const Node& cnc : cn)
+              {
+                cvisit.push_back(cnc);
+              }
+            }
+            Trace("match-debug") << "recurse op : " << op << std::endl;
+            visit.push_back(cvisit);
+            visit_trie.push_back(&itu->second);
+            visit_var_index.push_back(-1);
+            visit_bound_var.push_back(false);
+          }
+        }
+        visit_var_index[index]++;
+      }
+      else
+      {
+        // clean up if we previously bound a variable
+        if (visit_bound_var[index])
+        {
+          Assert(!vars.empty());
+          smap.erase(vars.back());
+          vars.pop_back();
+          subs.pop_back();
+          visit_bound_var[index] = false;
+        }
+
+        if (vindex == static_cast<int>(curr->d_vars.size()))
+        {
+          Trace("match-debug")
+              << "finished checking " << curr->d_vars.size()
+              << " variables at depth " << visit.size() << std::endl;
+          // finished
+          visit.pop_back();
+          visit_trie.pop_back();
+          visit_var_index.pop_back();
+          visit_bound_var.pop_back();
+        }
+        else
+        {
+          Trace("match-debug") << "check variable #" << vindex << " at depth "
+                               << visit.size() << std::endl;
+          Assert(vindex < static_cast<int>(curr->d_vars.size()));
+          // recurse on variable?
+          Node var = curr->d_vars[vindex];
+          bool recurse = true;
+          // check if it is already bound
+          std::map<Node, Node>::iterator its = smap.find(var);
+          if (its != smap.end())
+          {
+            if (its->second != cn)
+            {
+              recurse = false;
+            }
+          }
+          else if (!var.getType().isSubtypeOf(cn.getType()))
+          {
+            recurse = false;
+          }
+          else
+          {
+            vars.push_back(var);
+            subs.push_back(cn);
+            smap[var] = cn;
+            visit_bound_var[index] = true;
+          }
+          if (recurse)
+          {
+            Trace("match-debug") << "recurse var : " << var << std::endl;
+            cvisit.pop_back();
+            visit.push_back(cvisit);
+            visit_trie.push_back(&curr->d_children[var][0]);
+            visit_var_index.push_back(-1);
+            visit_bound_var.push_back(false);
+          }
+          visit_var_index[index]++;
+        }
+      }
+    }
+  }
+  return true;
+}
+
+void MatchTrie::addTerm(Node n)
+{
+  Assert(!n.isNull());
+  std::vector<Node> visit;
+  visit.push_back(n);
+  MatchTrie* curr = this;
+  while (!visit.empty())
+  {
+    Node cn = visit.back();
+    visit.pop_back();
+    if (cn.hasOperator())
+    {
+      curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
+      for (const Node& cnc : cn)
+      {
+        visit.push_back(cnc);
+      }
+    }
+    else
+    {
+      if (cn.isVar()
+          && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
+                 == curr->d_vars.end())
+      {
+        curr->d_vars.push_back(cn);
+      }
+      curr = &(curr->d_children[cn][0]);
+    }
+  }
+  curr->d_data = n;
+}
+
+void MatchTrie::clear()
+{
+  d_children.clear();
+  d_vars.clear();
+  d_data = Node::null();
+}
+
+}  // namespace expr
+}  // namespace CVC4
diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h
new file mode 100644
index 000000000..ea8be44d9
--- /dev/null
+++ b/src/expr/match_trie.h
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file match_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Implements a match trie, also known as a discrimination tree.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__MATCH_TRIE_H
+#define CVC4__EXPR__MATCH_TRIE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/** A virtual class for notifications regarding matches. */
+class NotifyMatch
+{
+ public:
+  virtual ~NotifyMatch() {}
+  /**
+   * A notification that s is equal to n * { vars -> subs }. This function
+   * should return false if we do not wish to be notified of further matches.
+   */
+  virtual bool notify(Node s,
+                      Node n,
+                      std::vector<Node>& vars,
+                      std::vector<Node>& subs) = 0;
+};
+
+/**
+ * A trie (discrimination tree) storing a set of terms S, that can be used to
+ * query, for a given term t, all terms s from S that are matchable with t,
+ * that is s*sigma = t for some substitution sigma.
+ */
+class MatchTrie
+{
+ public:
+  /** Get matches
+   *
+   * This calls ntm->notify( n, s, vars, subs ) for each term s stored in this
+   * trie that is matchable with n where s = n * { vars -> subs } for some
+   * vars, subs. This function returns false if one of these calls to notify
+   * returns false.
+   */
+  bool getMatches(Node n, NotifyMatch* ntm);
+  /** Adds node n to this trie */
+  void addTerm(Node n);
+  /** Clear this trie */
+  void clear();
+
+ private:
+  /**
+   * The children of this node in the trie. Terms t are indexed by a
+   * depth-first (right to left) traversal on its subterms, where the
+   * top-symbol of t is indexed by:
+   * - (operator, #children) if t has an operator, or
+   * - (t, 0) if t does not have an operator.
+   */
+  std::map<Node, std::map<unsigned, MatchTrie> > d_children;
+  /** The set of variables in the domain of d_children */
+  std::vector<Node> d_vars;
+  /** The data of this node in the trie */
+  Node d_data;
+};
+
+}  // namespace expr
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
new file mode 100644
index 000000000..d9a5f6e1a
--- /dev/null
+++ b/src/expr/term_canonize.cpp
@@ -0,0 +1,210 @@
+/*********************                                                        */
+/*! \file term_canonize.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 "expr/term_canonize.h"
+
+// TODO #1216: move the code in this include
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace expr {
+
+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 getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
+    }
+    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);
+    d_fvIndex[x] = d_cn_free_var[tn].size();
+    d_cn_free_var[tn].push_back(x);
+  }
+  return d_cn_free_var[tn][i];
+}
+
+size_t TermCanonize::getIndexForFreeVariable(Node v) const
+{
+  std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
+  if (it == d_fvIndex.end())
+  {
+    return 0;
+  }
+  return it->second;
+}
+
+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,
+                                    bool doHoVar,
+                                    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 && theory::quantifiers::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, doHoVar, var_count, visited);
+    }
+    if (n.getMetaKind() == metakind::PARAMETERIZED)
+    {
+      Node op = n.getOperator();
+      if (doHoVar)
+      {
+        op = getCanonicalTerm(op, apply_torder, doHoVar, 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, bool doHoVar)
+{
+  std::map<TypeNode, unsigned> var_count;
+  std::map<TNode, Node> visited;
+  return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
+}
+
+}  // namespace expr
+}  // namespace CVC4
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
new file mode 100644
index 000000000..6049cd804
--- /dev/null
+++ b/src/expr/term_canonize.h
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file term_canonize.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Utilities for constructing canonical terms.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__TERM_CANONIZE_H
+#define CVC4__EXPR__TERM_CANONIZE_H
+
+#include <map>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/** TermCanonize
+ *
+ * This class contains utilities for canonizing terms with respect to
+ * free variables (which are of kind BOUND_VARIABLE). For example, this
+ * class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2)
+ * are effectively the same term.
+ */
+class TermCanonize
+{
+ public:
+  TermCanonize();
+  ~TermCanonize() {}
+
+  /** Maps operators to an identifier, useful for ordering. */
+  int getIdForOperator(Node op);
+  /** Maps types to an identifier, useful for ordering. */
+  int getIdForType(TypeNode t);
+  /** get term order
+   *
+   * Returns true if a <= b in the term ordering used by this class. The
+   * term order is determined by the leftmost position in a and b whose
+   * operators o_a and o_b are distinct at that position. Then a <= b iff
+   * getIdForOperator( o_a ) <= getIdForOperator( o_b ).
+   */
+  bool getTermOrder(Node a, Node b);
+  /** get canonical free variable #i of type tn */
+  Node getCanonicalFreeVar(TypeNode tn, unsigned i);
+  /** get canonical term
+   *
+   * This returns a canonical (alpha-equivalent) version of n, where
+   * bound variables in n may be replaced by other ones, and arguments of
+   * commutative operators of n may be sorted (if apply_torder is true). If
+   * doHoVar is true, we also canonicalize bound variables that occur in
+   * operators.
+   *
+   * In detail, we replace bound variables in n so the the leftmost occurrence
+   * of a bound variable for type T is the first canonical free variable for T,
+   * the second leftmost is the second, and so on, for each type T.
+   */
+  Node getCanonicalTerm(TNode n,
+                        bool apply_torder = false,
+                        bool doHoVar = true);
+
+ private:
+  /** the number of ids we have allocated for operators */
+  int d_op_id_count;
+  /** map from operators to id */
+  std::map<Node, int> d_op_id;
+  /** the number of ids we have allocated for types */
+  int d_typ_id_count;
+  /** map from type to id */
+  std::map<TypeNode, int> d_typ_id;
+  /** free variables for each type */
+  std::map<TypeNode, std::vector<Node> > d_cn_free_var;
+  /**
+   * Map from each free variable above to their index in their respective vector
+   */
+  std::map<Node, size_t> d_fvIndex;
+  /**
+   * Return the range of the free variable in the above map, or 0 if it does not
+   * exist.
+   */
+  size_t getIndexForFreeVariable(Node v) const;
+  /** get canonical term
+   *
+   * This is a helper function for getCanonicalTerm above. We maintain a
+   * counter of how many variables we have allocated for each type (var_count),
+   * and a cache of visited nodes (visited).
+   */
+  Node getCanonicalTerm(TNode n,
+                        bool apply_torder,
+                        bool doHoVar,
+                        std::map<TypeNode, unsigned>& var_count,
+                        std::map<TNode, Node>& visited);
+};
+
+}  // namespace expr
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__TERM_CANONIZE_H */