Make (T)NodeTrie a general utility (#2489)

This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.

3 files changed, 209 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 35ef34dfa..61ab7b3fb 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -27,6 +27,8 @@ libcvc4_add_sources(
   node_manager_listeners.cpp
   node_manager_listeners.h
   node_self_iterator.h
+  node_trie.cpp
+  node_trie.h
   node_value.cpp
   node_value.h
   pickle_data.cpp
diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp
new file mode 100644
index 000000000..4404e78ca
--- /dev/null
+++ b/src/expr/node_trie.cpp
@@ -0,0 +1,95 @@
+/*********************                                                        */
+/*! \file node_trie.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 a trie class for Nodes and TNodes.
+ **/
+
+#include "expr/node_trie.h"
+
+namespace CVC4 {
+namespace theory {
+
+template <bool ref_count>
+NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm(
+    const std::vector<NodeTemplate<ref_count>>& reps) const
+{
+  const NodeTemplateTrie<ref_count>* tnt = this;
+  typename std::map<NodeTemplate<ref_count>,
+                    NodeTemplateTrie<ref_count>>::const_iterator it;
+  for (const NodeTemplate<ref_count> r : reps)
+  {
+    it = tnt->d_data.find(r);
+    if (it == tnt->d_data.end())
+    {
+      // didn't find this child, return null
+      return Node::null();
+    }
+    tnt = &it->second;
+  }
+  if (tnt->d_data.empty())
+  {
+    return Node::null();
+  }
+  return tnt->d_data.begin()->first;
+}
+
+template TNode NodeTemplateTrie<false>::existsTerm(
+    const std::vector<TNode>& reps) const;
+template Node NodeTemplateTrie<true>::existsTerm(
+    const std::vector<Node>& reps) const;
+
+template <bool ref_count>
+NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::addOrGetTerm(
+    NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
+{
+  NodeTemplateTrie<ref_count>* tnt = this;
+  for (const NodeTemplate<ref_count> r : reps)
+  {
+    tnt = &(tnt->d_data[r]);
+  }
+  if (tnt->d_data.empty())
+  {
+    // Store n in d_data. This should be interpretted as the "data" and not as a
+    // reference to a child.
+    tnt->d_data[n].clear();
+    return n;
+  }
+  return tnt->d_data.begin()->first;
+}
+
+template TNode NodeTemplateTrie<false>::addOrGetTerm(
+    TNode n, const std::vector<TNode>& reps);
+template Node NodeTemplateTrie<true>::addOrGetTerm(
+    Node n, const std::vector<Node>& reps);
+
+template <bool ref_count>
+void NodeTemplateTrie<ref_count>::debugPrint(const char* c,
+                                             unsigned depth) const
+{
+  for (const std::pair<const NodeTemplate<ref_count>,
+                       NodeTemplateTrie<ref_count>>& p : d_data)
+  {
+    for (unsigned i = 0; i < depth; i++)
+    {
+      Trace(c) << "  ";
+    }
+    Trace(c) << p.first << std::endl;
+    p.second.debugPrint(c, depth + 1);
+  }
+}
+
+template void NodeTemplateTrie<false>::debugPrint(const char* c,
+                                                  unsigned depth) const;
+template void NodeTemplateTrie<true>::debugPrint(const char* c,
+                                                 unsigned depth) const;
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h
new file mode 100644
index 000000000..d0c0f0627
--- /dev/null
+++ b/src/expr/node_trie.h
@@ -0,0 +1,112 @@
+/*********************                                                        */
+/*! \file node_trie.h
+ ** \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 A trie class for Nodes and TNodes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__NODE_TRIE_H
+#define __CVC4__EXPR__NODE_TRIE_H
+
+#include <map>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** NodeTemplate trie class
+ *
+ * This is a trie data structure whose distinguishing feature is that it has
+ * no "data" members and only references to children. The motivation for having
+ * no data members is efficiency.
+ *
+ * One use of this class is to represent "term indices" or a "signature tables"
+ * for symbols with fixed arities. In this use case, we "index" terms by the
+ * list of representatives of their arguments.
+ *
+ * For example, consider the equivalence classes :
+ *
+ * { a, d, f( d, c ), f( a, c ) }
+ * { b, f( b, d ) }
+ * { c, f( b, b ) }
+ *
+ * where the first elements ( a, b, c ) are the representatives of these
+ * classes. The NodeTemplateTrie t we may build for f is :
+ *
+ * t :
+ *   t.d_data[a] :
+ *     t.d_data[a].d_data[c] :
+ *       t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf)
+ *   t.d_data[b] :
+ *     t.d_data[b].d_data[b] :
+ *       t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf)
+ *     t.d_data[b].d_data[d] :
+ *       t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf)
+ *
+ * Leaf nodes store the terms that are indexed by the arguments, for example
+ * term f(d,c) is indexed by the representative arguments (a,c), and is stored
+ * as a the (single) key in the data of t.d_data[a].d_data[c].
+ */
+template <bool ref_count>
+class NodeTemplateTrie
+{
+ public:
+  /** The children of this node. */
+  std::map<NodeTemplate<ref_count>, NodeTemplateTrie<ref_count>> d_data;
+  /** For leaf nodes : does this node have data? */
+  bool hasData() const { return !d_data.empty(); }
+  /** For leaf nodes : get the node corresponding to this leaf. */
+  NodeTemplate<ref_count> getData() const { return d_data.begin()->first; }
+  /**
+   * Returns the term that is indexed by reps, if one exists, or
+   * or returns null otherwise.
+   */
+  NodeTemplate<ref_count> existsTerm(
+      const std::vector<NodeTemplate<ref_count>>& reps) const;
+  /**
+   * Returns the term that is previously indexed by reps, if one exists, or
+   * adds n to the trie, indexed by reps, and returns n.
+   */
+  NodeTemplate<ref_count> addOrGetTerm(
+      NodeTemplate<ref_count> n,
+      const std::vector<NodeTemplate<ref_count>>& reps);
+  /**
+   * Returns false if a term is previously indexed by reps.
+   * Returns true if no term is previously indexed by reps,
+   *   and adds n to the trie, indexed by reps.
+   */
+  inline bool addTerm(NodeTemplate<ref_count> n,
+                      const std::vector<NodeTemplate<ref_count>>& reps);
+  /** Debug print this trie on Trace c with indentation depth. */
+  void debugPrint(const char* c, unsigned depth = 0) const;
+  /** Clear all data from this trie. */
+  void clear() { d_data.clear(); }
+  /** Is this trie empty? */
+  bool empty() const { return d_data.empty(); }
+}; /* class NodeTemplateTrie */
+
+template <bool ref_count>
+bool NodeTemplateTrie<ref_count>::addTerm(
+    NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
+{
+  return addOrGetTerm(n, reps) == n;
+}
+
+/** Reference-counted version of the above data structure */
+typedef NodeTemplateTrie<true> NodeTrie;
+/** Non-reference-counted version of the above data structure */
+typedef NodeTemplateTrie<false> TNodeTrie;
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__EXPR__NODE_TRIE_H */