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.

25 files changed, 465 insertions, 284 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 */
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 77579489a..5ed623190 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -26,7 +26,6 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/valuation.h"
@@ -1334,13 +1333,16 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
   return EQUALITY_FALSE_IN_MODEL;
 }
 
-
-
-void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
+void TheoryDatatypes::addCarePairs(TNodeTrie* t1,
+                                   TNodeTrie* t2,
+                                   unsigned arity,
+                                   unsigned depth,
+                                   unsigned& n_pairs)
+{
   if( depth==arity ){
     if( t2!=NULL ){
-      Node f1 = t1->getNodeData();
-      Node f2 = t2->getNodeData();
+      Node f1 = t1->getData();
+      Node f2 = t2->getData();
       if( !areEqual( f1, f2 ) ){
         Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
@@ -1371,13 +1373,17 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::
     if( t2==NULL ){
       if( depth<(arity-1) ){
         //add care pairs internal to each child
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-          addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
+        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+        {
+          addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs);
         }
       }
       //add care pairs based on each pair of non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+           it != t1->d_data.end();
+           ++it)
+      {
+        std::map<TNode, TNodeTrie>::iterator it2 = it;
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
@@ -1389,11 +1395,15 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::
       }
     }else{
       //add care pairs based on product of indices, non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
-          if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
-            if( !areCareDisequal(it->first, it2->first) ){
-              addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+      {
+        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        {
+          if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+          {
+            if (!areCareDisequal(tt1.first, tt2.first))
+            {
+              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
             }
           }
         }
@@ -1406,7 +1416,7 @@ void TheoryDatatypes::computeCareGraph(){
   unsigned n_pairs = 0;
   Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl;
   Trace("dt-cg") << "Build indices..." << std::endl;
-  std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > > index;
+  std::map<TypeNode, std::map<Node, TNodeTrie> > index;
   std::map< Node, unsigned > arity;
   //populate indices
   unsigned functionTerms = d_functionTerms.size();
@@ -1432,10 +1442,13 @@ void TheoryDatatypes::computeCareGraph(){
     }
   }
   //for each index
-  for( std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > >::iterator iti = index.begin(); iti != index.end(); ++iti ){
-    for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = iti->second.begin(); itii != iti->second.end(); ++itii ){
-      Trace("dt-cg") << "Process index " << itii->first << ", " << iti->first << "..." << std::endl;
-      addCarePairs( &itii->second, NULL, arity[ itii->first ], 0, n_pairs );
+  for (std::pair<const TypeNode, std::map<Node, TNodeTrie> >& tt : index)
+  {
+    for (std::pair<const Node, TNodeTrie>& t : tt.second)
+    {
+      Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..."
+                     << std::endl;
+      addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs);
     }
   }
   Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 0a3017058..a7b40e282 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -25,6 +25,7 @@
 #include "context/cdlist.h"
 #include "expr/attribute.h"
 #include "expr/datatype.h"
+#include "expr/node_trie.h"
 #include "theory/datatypes/datatypes_sygus.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -32,11 +33,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-namespace quantifiers{
-  class TermArgTrie;
-}
-
 namespace datatypes {
 
 class TheoryDatatypes : public Theory {
@@ -253,7 +249,11 @@ private:
   TNode getEqcConstructor( TNode r );
 
  protected:
-  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
+  void addCarePairs(TNodeTrie* t1,
+                    TNodeTrie* t2,
+                    unsigned arity,
+                    unsigned depth,
+                    unsigned& n_pairs);
   /** compute care graph */
   void computeCareGraph() override;
 
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
index 3535b57b7..df6690273 100644
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
@@ -107,14 +107,14 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci,
                                         Node pv,
                                         Node catom,
                                         std::vector<Node>& arg_reps,
-                                        TermArgTrie* tat,
+                                        TNodeTrie* tat,
                                         unsigned index,
                                         std::map<Node, int>& match_score)
 {
   if (index == catom.getNumChildren())
   {
-    Assert(tat->hasNodeData());
-    Node gcatom = tat->getNodeData();
+    Assert(tat->hasData());
+    Node gcatom = tat->getData();
     Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom
                        << std::endl;
     for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++)
@@ -132,7 +132,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci,
     }
     return;
   }
-  std::map<TNode, TermArgTrie>::iterator it = tat->d_data.find(arg_reps[index]);
+  std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(arg_reps[index]);
   if (it != tat->d_data.end())
   {
     computeMatchScore(
@@ -165,7 +165,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci,
   TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase();
   Node rep = ee->getRepresentative(eqc);
   Node op = tdb->getMatchOperator(catom);
-  TermArgTrie* tat = tdb->getTermArgTrie(rep, op);
+  TNodeTrie* tat = tdb->getTermArgTrie(rep, op);
   Trace("cegqi-epr") << "EPR instantiation match term : " << catom
                      << ", check ground terms=" << (tat != NULL) << std::endl;
   if (tat)
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
index b4378e1d2..f5057ad86 100644
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
@@ -19,14 +19,13 @@
 
 #include <map>
 #include <vector>
+#include "expr/node_trie.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermArgTrie;
-
 /** Effectively Propositional (EPR) Instantiator
  *
  * This implements a selection function for the EPR fragment.
@@ -93,7 +92,7 @@ class EprInstantiator : public Instantiator
                          Node pv,
                          Node catom,
                          std::vector<Node>& arg_reps,
-                         TermArgTrie* tat,
+                         TNodeTrie* tat,
                          unsigned index,
                          std::map<Node, int>& match_score);
   void computeMatchScore(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 1d2f9a322..7408678e7 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1630,7 +1630,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
           //initial binding
           TNode f = s->getTgFunc( d_typ, d_status_num );
           Assert( !eqc.isNull() );
-          TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
+          TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f);
           if( tat ){
             d_match_children.push_back( tat->d_data.begin() );
             d_match_children_end.push_back( tat->d_data.end() );
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 450bd7991..8fff7eafe 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -18,6 +18,7 @@
 #define CONJECTURE_GENERATOR_H
 
 #include "context/cdhashmap.h"
+#include "expr/node_trie.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/type_enumerator.h"
 
@@ -25,8 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermArgTrie;
-
 //algorithm for computing candidate subgoals
 
 class ConjectureGenerator;
@@ -105,8 +104,8 @@ class TermGenerator
   //2 : variables must map to non-ground terms
   unsigned d_match_mode;
   //children
-  std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
-  std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end;
+  std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children;
+  std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children_end;
 
   void reset( TermGenEnv * s, TypeNode tn );
   bool getNextTerm( TermGenEnv * s, unsigned depth );
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 3f404c17f..612a1938a 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -57,7 +57,7 @@ void CandidateGeneratorQE::reset( Node eqc ){
     }else{
       eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
       if( ee->hasTerm( eqc ) ){
-        quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op );
+        TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op);
         if( tat ){
           //create an equivalence class iterator in eq class eqc
           Node rep = ee->getRepresentative( eqc );
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 646208ec6..f26df5b79 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -1028,7 +1028,7 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
                                                 Trigger* tparent)
 {
   int addedLemmas = 0;
-  quantifiers::TermArgTrie* tat;
+  TNodeTrie* tat;
   if( d_eqc.isNull() ){
     tat = qe->getTermDatabase()->getTermArgTrie( d_op );
   }else{
@@ -1040,10 +1040,12 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
       if (tat && !qe->inConflict())
       {
         Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
-          if( it->first!=r ){
+        for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
+        {
+          if (t.first != r)
+          {
             InstMatch m( q );
-            addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+            addInstantiations(m, qe, addedLemmas, 0, &(t.second));
             if( qe->inConflict() ){
               break;
             }
@@ -1066,13 +1068,13 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
                                                  QuantifiersEngine* qe,
                                                  int& addedLemmas,
                                                  unsigned argIndex,
-                                                 quantifiers::TermArgTrie* tat)
+                                                 TNodeTrie* tat)
 {
   Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
   if (argIndex == d_match_pattern.getNumChildren())
   {
     Assert( !tat->d_data.empty() );
-    TNode t = tat->getNodeData();
+    TNode t = tat->getData();
     Debug("simple-trigger") << "Actual term is " << t << std::endl;
     //convert to actual used terms
     for (std::map<unsigned, int>::iterator it = d_var_num.begin();
@@ -1096,14 +1098,15 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
       int v = d_var_num[argIndex];
       if( v!=-1 ){
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
-          Node t = it->first;
+        for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+        {
+          Node t = tt.first;
           Node prev = m.get( v );
           //using representatives, just check if equal
           Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
           if( prev.isNull() || prev==t ){
             m.setValue( v, t);
-            addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+            addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
             m.setValue( v, prev);
             if( qe->inConflict() ){
               break;
@@ -1115,7 +1118,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
       //inst constant from another quantified formula, treat as ground term  TODO: remove this?
     }
     Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
-    std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+    std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
     if( it!=tat->d_data.end() ){
       addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
     }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index abf269f3e..83d4ce82e 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -18,15 +18,13 @@
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
 
 #include <map>
+#include "expr/node_trie.h"
 #include "theory/quantifiers/inst_match_trie.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
-namespace quantifiers{
-  class TermArgTrie;
-}
 
 namespace inst {
 
@@ -662,7 +660,7 @@ class InstMatchGeneratorSimple : public IMGenerator {
                          QuantifiersEngine* qe,
                          int& addedLemmas,
                          unsigned argIndex,
-                         quantifiers::TermArgTrie* tat);
+                         TNodeTrie* tat);
 };/* class InstMatchGeneratorSimple */
 }
 }
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index dc1bf6908..1ba359228 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -22,9 +22,9 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
+#include "expr/node_trie.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -72,17 +72,21 @@ public:
   TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
 private:
   /** term index */
-  std::map< Node, TermArgTrie > d_uf_func_map_trie;
-  /** union find for terms beyond what is stored in equality engine */
-  std::map< Node, Node > d_uf;
-  std::map< Node, std::vector< Node > > d_uf_exp;
-  Node getUfRepresentative( Node a, std::vector< Node >& exp );
-  /** disequality list, stores explanations */
-  std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
-  /** add arg */
-  void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
-  /** register term */
-  void registerUfTerm( TNode n );
+ std::map<Node, TNodeTrie> d_uf_func_map_trie;
+ /** union find for terms beyond what is stored in equality engine */
+ std::map<Node, Node> d_uf;
+ std::map<Node, std::vector<Node> > d_uf_exp;
+ Node getUfRepresentative(Node a, std::vector<Node>& exp);
+ /** disequality list, stores explanations */
+ std::map<Node, std::map<Node, std::vector<Node> > > d_diseq_list;
+ /** add arg */
+ void addArgument(Node n,
+                  std::vector<Node>& args,
+                  std::vector<Node>& watch,
+                  bool is_watch);
+ /** register term */
+ void registerUfTerm(TNode n);
+
 public:
   enum {
     STATUS_CONFLICT,
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 93b220ea9..752d61489 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -196,9 +196,17 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
   }
 }
 
-void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
-                                               std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr,
-                                               unsigned pindex, unsigned paindex, unsigned iindex ){
+void LtePartialInst::getPartialInstantiations(std::vector<Node>& conj,
+                                              Node q,
+                                              Node bvl,
+                                              std::vector<Node>& vars,
+                                              std::vector<Node>& terms,
+                                              std::vector<TypeNode>& types,
+                                              TNodeTrie* curr,
+                                              unsigned pindex,
+                                              unsigned paindex,
+                                              unsigned iindex)
+{
   if( iindex==vars.size() ){
     Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
     if( bvl.isNull() ){
@@ -231,9 +239,19 @@ void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q
           //start traversing term index for the operator
           curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() );
         }
-        for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){
-          terms[d_pat_var_order[q][iindex]] = it->first;
-          getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 );
+        for (std::pair<const TNode, TNodeTrie>& t : curr->d_data)
+        {
+          terms[d_pat_var_order[q][iindex]] = t.first;
+          getPartialInstantiations(conj,
+                                   q,
+                                   bvl,
+                                   vars,
+                                   terms,
+                                   types,
+                                   &t.second,
+                                   pindex,
+                                   paindex + 1,
+                                   iindex + 1);
         }
       }
     }else{
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 63e810645..b8b0e34fa 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -17,15 +17,14 @@
 #ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H
 #define __CVC4__THEORY__LOCAL_THEORY_EXT_H
 
-#include "theory/quantifiers_engine.h"
 #include "context/cdo.h"
+#include "expr/node_trie.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermArgTrie;  
-
 class LtePartialInst : public QuantifiersModule {
 private:
   // was this module invoked
@@ -46,9 +45,16 @@ private:
   void reset();
   /** get instantiations */
   void getInstantiations( std::vector< Node >& lemmas );
-  void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
-                                 std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr,
-                                 unsigned pindex, unsigned paindex, unsigned iindex );
+  void getPartialInstantiations(std::vector<Node>& conj,
+                                Node q,
+                                Node bvl,
+                                std::vector<Node>& vars,
+                                std::vector<Node>& inst,
+                                std::vector<TypeNode>& types,
+                                TNodeTrie* curr,
+                                unsigned pindex,
+                                unsigned paindex,
+                                unsigned iindex);
   /** get eligible inst variables */
   void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
   
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 95ec24df9..5b57af14c 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1293,7 +1293,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     Assert( isHandledUfTerm( d_n ) );
     TNode f = getMatchOperator( p, d_n );
     Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
-    TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
+    TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f);
     if (qni == nullptr || qni->empty())
     {
       //inform irrelevant quantifiers
@@ -1672,7 +1672,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             }else{
               //binding a variable
               d_qni_bound[index] = repVar;
-              std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin();
+              std::map<TNode, TNodeTrie>::iterator it =
+                  d_qn[index]->d_data.begin();
               if( it != d_qn[index]->d_data.end() ) {
                 d_qni.push_back( it );
                 //set the match
@@ -1699,7 +1700,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
           }
           if( !val.isNull() ){
             //constrained by val
-            std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val );
+            std::map<TNode, TNodeTrie>::iterator it =
+                d_qn[index]->d_data.find(val);
             if( it!=d_qn[index]->d_data.end() ){
               Debug("qcf-match-debug") << "       Match" << std::endl;
               d_qni.push_back( it );
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 0469e958b..9fa37a96c 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -22,7 +22,7 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
-#include "theory/quantifiers/term_database.h"
+#include "expr/node_trie.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -45,8 +45,8 @@ private:
   MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
   //MatchGen * getChild( int i ) { return &d_children[i]; }
   //current matching information
-  std::vector< TermArgTrie * > d_qn;
-  std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni;
+  std::vector<TNodeTrie*> d_qn;
+  std::vector<std::map<TNode, TNodeTrie>::iterator> d_qni;
   bool doMatching( QuantConflictFind * p, QuantInfo * qi );
   //for matching : each index is either a variable or a ground term
   unsigned d_qni_size;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 482acacc2..44c5586c3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -32,49 +32,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) {
-  if( argIndex==(int)reps.size() ){
-    if( d_data.empty() ){
-      return Node::null();
-    }else{
-      return d_data.begin()->first;
-    }
-  }else{
-    std::map< TNode, TermArgTrie >::iterator it = d_data.find( reps[argIndex] );
-    if( it==d_data.end() ){
-      return Node::null();
-    }else{
-      return it->second.existsTerm( reps, argIndex+1 );
-    }
-  }
-}
-
-bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){
-  return addOrGetTerm( n, reps, argIndex )==n;
-}
-
-TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) {
-  if( argIndex==(int)reps.size() ){
-    if( d_data.empty() ){
-      //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
-      d_data[n].clear();
-      return n;
-    }else{
-      return d_data.begin()->first;
-    }
-  }else{
-    return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 );
-  }
-}
-
-void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
-  for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
-    for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  "; }
-    Trace(c) << it->first << std::endl;
-    it->second.debugPrint( c, n, depth+1 );
-  }
-}
-
 TermDb::TermDb(context::Context* c, context::UserContext* u,
                QuantifiersEngine* qe)
     : d_quantEngine(qe),
@@ -1056,12 +1013,13 @@ bool TermDb::reset( Theory::Effort effort ){
   return true;
 }
 
-TermArgTrie * TermDb::getTermArgTrie( Node f ) {
+TNodeTrie* TermDb::getTermArgTrie(Node f)
+{
   if( options::ufHo() ){
     f = getOperatorRepresentative( f );
   }
   computeUfTerms( f );
-  std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
+  std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
   if( itut!=d_func_map_trie.end() ){
     return &itut->second;
   }else{
@@ -1069,19 +1027,21 @@ TermArgTrie * TermDb::getTermArgTrie( Node f ) {
   }
 }
 
-TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
+TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
+{
   if( options::ufHo() ){
     f = getOperatorRepresentative( f );
   }
   computeUfEqcTerms( f );
-  std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f );
+  std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
   if( itut==d_func_map_eqc_trie.end() ){
     return NULL;
   }else{
     if( eqc.isNull() ){
       return &itut->second;
     }else{
-      std::map< TNode, TermArgTrie >::iterator itute = itut->second.d_data.find( eqc );
+      std::map<TNode, TNodeTrie>::iterator itute =
+          itut->second.d_data.find(eqc);
       if( itute!=itut->second.d_data.end() ){
         return &itute->second;
       }else{
@@ -1096,7 +1056,7 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) {
     f = getOperatorRepresentative( f );
   }
   computeUfTerms( f );
-  std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
+  std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
   if( itut!=d_func_map_trie.end() ){
     computeArgReps( n );
     return itut->second.existsTerm( d_arg_reps[n] );
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 */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index ec6406a6a..83c66c2d3 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -21,7 +21,6 @@
 #include "expr/node_algorithm.h"
 #include "options/sets_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/theory_model.h"
@@ -1774,11 +1773,16 @@ void TheorySetsPrivate::addSharedTerm(TNode n) {
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 }
 
-void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
+void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
+                                     TNodeTrie* t2,
+                                     unsigned arity,
+                                     unsigned depth,
+                                     unsigned& n_pairs)
+{
   if( depth==arity ){
     if( t2!=NULL ){
-      Node f1 = t1->getNodeData();
-      Node f2 = t2->getNodeData();
+      Node f1 = t1->getData();
+      Node f2 = t2->getData();
       if( !ee_areEqual( f1, f2 ) ){
         Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
@@ -1818,13 +1822,17 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers
     if( t2==NULL ){
       if( depth<(arity-1) ){
         //add care pairs internal to each child
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-          addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
+        for (std::pair<const TNode, TNodeTrie>& t : t1->d_data)
+        {
+          addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs);
         }
       }
       //add care pairs based on each pair of non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+           it != t1->d_data.end();
+           ++it)
+      {
+        std::map<TNode, TNodeTrie>::iterator it2 = it;
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
@@ -1836,11 +1844,15 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers
       }
     }else{
       //add care pairs based on product of indices, non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
-          if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
-            if( !ee_areCareDisequal(it->first, it2->first) ){
-              addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+      {
+        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        {
+          if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+          {
+            if (!ee_areCareDisequal(tt1.first, tt2.first))
+            {
+              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
             }
           }
         }
@@ -1855,7 +1867,7 @@ void TheorySetsPrivate::computeCareGraph() {
       unsigned n_pairs = 0;
       Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
       Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
-      std::map< TypeNode, quantifiers::TermArgTrie > index;
+      std::map<TypeNode, TNodeTrie> index;
       unsigned arity = 0;
       //populate indices
       for( unsigned i=0; i<it->second.size(); i++ ){
@@ -1882,9 +1894,11 @@ void TheorySetsPrivate::computeCareGraph() {
       }
       if( arity>0 ){
         //for each index
-        for( std::map< TypeNode, quantifiers::TermArgTrie >::iterator iti = index.begin(); iti != index.end(); ++iti ){
-          Trace("sets-cg") << "Process index " << iti->first << "..." << std::endl;
-          addCarePairs( &iti->second, NULL, arity, 0, n_pairs );
+        for (std::pair<const TypeNode, TNodeTrie>& tt : index)
+        {
+          Trace("sets-cg") << "Process index " << tt.first << "..."
+                           << std::endl;
+          addCarePairs(&tt.second, nullptr, arity, 0, n_pairs);
         }
       }
       Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index d36e0ddb1..447ac33a1 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -21,18 +21,13 @@
 
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
-
+#include "expr/node_trie.h"
+#include "theory/sets/theory_sets_rels.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
-#include "theory/sets/theory_sets_rels.h"
 
 namespace CVC4 {
 namespace theory {
-
-namespace quantifiers{
-  class TermArgTrie;
-}
-
 namespace sets {
 
 /** Internal classes, forward declared here */
@@ -83,9 +78,13 @@ private:
   Node getUnivSet( TypeNode tn );
   bool hasLemmaCached( Node lem );
   bool hasProcessed();
-  
-  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
-  
+
+  void addCarePairs(TNodeTrie* t1,
+                    TNodeTrie* t2,
+                    unsigned arity,
+                    unsigned depth,
+                    unsigned& n_pairs);
+
   Node d_true;
   Node d_false;
   Node d_zero;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e8b753768..9da6fd277 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -24,7 +24,6 @@
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/ext_theory.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_rewriter.h"
 #include "theory/strings/type_enumerator.h"
@@ -1118,11 +1117,15 @@ void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
   }
 }
 
-void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ) {
+void TheoryStrings::addCarePairs(TNodeTrie* t1,
+                                 TNodeTrie* t2,
+                                 unsigned arity,
+                                 unsigned depth)
+{
   if( depth==arity ){
     if( t2!=NULL ){
-      Node f1 = t1->getNodeData();
-      Node f2 = t2->getNodeData();
+      Node f1 = t1->getData();
+      Node f2 = t2->getData();
       if( !d_equalityEngine.areEqual( f1, f2 ) ){
         Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
@@ -1151,13 +1154,17 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
     if( t2==NULL ){
       if( depth<(arity-1) ){
         //add care pairs internal to each child
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-          addCarePairs( &it->second, NULL, arity, depth+1 );
+        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+        {
+          addCarePairs(&tt.second, nullptr, arity, depth + 1);
         }
       }
       //add care pairs based on each pair of non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+           it != t1->d_data.end();
+           ++it)
+      {
+        std::map<TNode, TNodeTrie>::iterator it2 = it;
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
@@ -1169,11 +1176,15 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
       }
     }else{
       //add care pairs based on product of indices, non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
-          if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
-            if( !areCareDisequal(it->first, it2->first) ){
-              addCarePairs( &it->second, &it2->second, arity, depth+1 );
+      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+      {
+        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        {
+          if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+          {
+            if (!areCareDisequal(tt1.first, tt2.first))
+            {
+              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
             }
           }
         }
@@ -1185,7 +1196,7 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
 void TheoryStrings::computeCareGraph(){
   //computing the care graph here is probably still necessary, due to operators that take non-string arguments  TODO: verify
   Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
-  std::map< Node, quantifiers::TermArgTrie > index;
+  std::map<Node, TNodeTrie> index;
   std::map< Node, unsigned > arity;
   unsigned functionTerms = d_functionsTerms.size();
   for (unsigned i = 0; i < functionTerms; ++ i) {
@@ -1206,9 +1217,11 @@ void TheoryStrings::computeCareGraph(){
     }
   }
   //for each index
-  for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){
-    Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
-    addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
+  for (std::pair<const Node, TNodeTrie>& tt : index)
+  {
+    Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
+                        << tt.first << "..." << std::endl;
+    addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
   }
 }
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index ec250288b..aa86f1bc1 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -22,6 +22,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "expr/attribute.h"
+#include "expr/node_trie.h"
 #include "theory/decision_manager.h"
 #include "theory/strings/regexp_elim.h"
 #include "theory/strings/regexp_operation.h"
@@ -35,11 +36,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-namespace quantifiers{
-  class TermArgTrie;
-}
-
 namespace strings {
 
 /**
@@ -557,7 +553,10 @@ private:
   //--------------------------------end for checkMemberships
 
  private:
-  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
+  void addCarePairs(TNodeTrie* t1,
+                    TNodeTrie* t2,
+                    unsigned arity,
+                    unsigned depth);
 
  public:
   /** preregister term */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3e9e2354d..645e1f656 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -28,7 +28,6 @@
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/quantifiers/term_database.h"
 #include "options/theory_options.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
@@ -557,12 +556,15 @@ bool TheoryUF::areCareDisequal(TNode x, TNode y){
   return false;
 }
 
-//TODO: move quantifiers::TermArgTrie to src/theory/
-void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){
+void TheoryUF::addCarePairs(TNodeTrie* t1,
+                            TNodeTrie* t2,
+                            unsigned arity,
+                            unsigned depth)
+{
   if( depth==arity ){
     if( t2!=NULL ){
-      Node f1 = t1->getNodeData();
-      Node f2 = t2->getNodeData();
+      Node f1 = t1->getData();
+      Node f2 = t2->getData();
       if( !d_equalityEngine.areEqual( f1, f2 ) ){
         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
         vector< pair<TNode, TNode> > currentPairs;
@@ -592,13 +594,17 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
     if( t2==NULL ){
       if( depth<(arity-1) ){
         //add care pairs internal to each child
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-          addCarePairs( &it->second, NULL, arity, depth+1 );
+        for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+        {
+          addCarePairs(&tt.second, NULL, arity, depth + 1);
         }
       }
       //add care pairs based on each pair of non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+      for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+           it != t1->d_data.end();
+           ++it)
+      {
+        std::map<TNode, TNodeTrie>::iterator it2 = it;
         ++it2;
         for( ; it2 != t1->d_data.end(); ++it2 ){
           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
@@ -610,11 +616,15 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
       }
     }else{
       //add care pairs based on product of indices, non-disequal arguments
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
-        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
-          if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
-            if( !areCareDisequal(it->first, it2->first) ){
-              addCarePairs( &it->second, &it2->second, arity, depth+1 );
+      for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+      {
+        for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+        {
+          if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+          {
+            if (!areCareDisequal(tt1.first, tt2.first))
+            {
+              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
             }
           }
         }
@@ -628,7 +638,7 @@ void TheoryUF::computeCareGraph() {
   if (d_sharedTerms.size() > 0) {
     //use term indexing
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
-    std::map< Node, quantifiers::TermArgTrie > index;
+    std::map<Node, TNodeTrie> index;
     std::map< Node, unsigned > arity;
     unsigned functionTerms = d_functionsTerms.size();
     for (unsigned i = 0; i < functionTerms; ++ i) {
@@ -644,14 +654,16 @@ void TheoryUF::computeCareGraph() {
         }
       }
       if( has_trigger_arg ){
-        index[op].addTerm( f1, reps, arg_start_index );
+        index[op].addTerm(f1, reps);
         arity[op] = reps.size();
       }
     }
     //for each index
-    for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){
-      Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
-      addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
+    for (std::pair<const Node, TNodeTrie>& tt : index)
+    {
+      Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
+                           << tt.first << "..." << std::endl;
+      addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
     }
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl;
   }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 2fd23a657..a0380f73a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -20,24 +20,16 @@
 #ifndef __CVC4__THEORY__UF__THEORY_UF_H
 #define __CVC4__THEORY__UF__THEORY_UF_H
 
+#include "context/cdhashset.h"
+#include "context/cdo.h"
 #include "expr/node.h"
-//#include "expr/attribute.h"
-
+#include "expr/node_trie.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/symmetry_breaker.h"
 
-#include "context/cdo.h"
-#include "context/cdhashset.h"
-
-
 namespace CVC4 {
 namespace theory {
-
-namespace quantifiers{
-  class TermArgTrie;
-}
-
 namespace uf {
 
 class UfTermDb;
@@ -313,7 +305,10 @@ private:
   }
 private:
   bool areCareDisequal(TNode x, TNode y);
-  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
+  void addCarePairs(TNodeTrie* t1,
+                    TNodeTrie* t2,
+                    unsigned arity,
+                    unsigned depth);
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */