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.

14 files changed, 104 insertions, 177 deletions

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 */