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.

1 files changed, 8 insertions, 70 deletions

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 7e3806e8c..cc9a24d08 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -21,9 +21,10 @@
 #include <unordered_set>
 
 #include "expr/attribute.h"
+#include "expr/node_trie.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/theory.h"
 #include "theory/type_enumerator.h"
-#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -37,69 +38,6 @@ namespace inst{
 
 namespace quantifiers {
 
-/** Term arg trie class
-*
-* This also referred to as a "term index" or a "signature table".
-*
-* This data structure stores a set expressions, indexed by 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 TermArgTrie 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].
-*/
-class TermArgTrie {
-public:
-  /** the data */
-  std::map< TNode, TermArgTrie > d_data;
-public:
- /** for leaf nodes : does this trie have data? */
- bool hasNodeData() { return !d_data.empty(); }
- /** for leaf nodes : get term corresponding to this leaf */
- TNode getNodeData() { return d_data.begin()->first; }
- /** exists term
- * Returns the term that is indexed by reps, if one exists, or
- * or returns null otherwise.
- */
- TNode existsTerm(std::vector<TNode>& reps, int argIndex = 0);
- /** add or get term
- * Returns the term that is previously indexed by reps, if one exists, or
- * Adds n to the trie, indexed by reps, and returns n.
- */
- TNode addOrGetTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0);
- /** add term
- * 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, and returns n.
- */
- bool addTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0);
- /** debug print this trie */
- void debugPrint(const char* c, Node n, unsigned depth = 0);
- /** clear all data from this trie */
- void clear() { d_data.clear(); }
- /** is empty */
- bool empty() { return d_data.empty(); }
-};/* class TermArgTrie */
-
 namespace fmcheck {
   class FullModelChecker;
 }
@@ -121,12 +59,12 @@ class TermGenEnv;
  * The primary responsibilities for this class are to :
  * (1) Maintain a list of all ground terms that exist in the quantifier-free
  *     solvers, as notified through the master equality engine.
- * (2) Build TermArgTrie objects that index all ground terms, per operator.
+ * (2) Build TNodeTrie objects that index all ground terms, per operator.
  *
  * Like other utilities, its reset(...) function is called
  * at the beginning of full or last call effort checks.
  * This initializes the database for the round. However,
- * notice that TermArgTrie objects are computed
+ * notice that TNodeTrie objects are computed
  * lazily for performance reasons.
  */
 class TermDb : public QuantifiersUtil {
@@ -213,10 +151,10 @@ class TermDb : public QuantifiersUtil {
   */
   Node getMatchOperator(Node n);
   /** get term arg index for all f-applications in the current context */
-  TermArgTrie* getTermArgTrie(Node f);
+  TNodeTrie* getTermArgTrie(Node f);
   /** get the term arg trie for f-applications in the equivalence class of eqc.
    */
-  TermArgTrie* getTermArgTrie(Node eqc, Node f);
+  TNodeTrie* getTermArgTrie(Node eqc, Node f);
   /** get congruent term
   * If possible, returns a term t such that:
   * (1) t is a term that is currently indexed by this database,
@@ -358,8 +296,8 @@ class TermDb : public QuantifiersUtil {
   /** mapping from terms to representatives of their arguments */
   std::map< TNode, std::vector< TNode > > d_arg_reps;
   /** map from operators to trie */
-  std::map< Node, TermArgTrie > d_func_map_trie;
-  std::map< Node, TermArgTrie > d_func_map_eqc_trie;
+  std::map<Node, TNodeTrie> d_func_map_trie;
+  std::map<Node, TNodeTrie> d_func_map_eqc_trie;
   /** mapping from operators to their representative relevant domains */
   std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom;
   /** has map */