Document term db (#1220)

* Document TermDb and related classes. Minor changes to quantifiers utils and their interface.  Address some comments left over from PR 1206.

* Minor

* Minor

* Change namespace style.

* Address review

* Fix incorrectly merged portion that led to regression failures.

* New clang format, fully document relevant domain.

* Clang format again.

* Minor

15 files changed, 745 insertions, 260 deletions

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index fb8ac4195..e79f3456b 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -23,11 +23,12 @@
 #include "theory/uf/equality_engine.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
 
@@ -116,8 +117,11 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
   }
 }
 
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
-  Assert( f.isNull() || f.getKind()==FORALL );
+Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
+                                                               Node q,
+                                                               int index)
+{
+  Assert(q.isNull() || q.getKind() == FORALL);
   Node r = getRepresentative( a );
   if( options::finiteModelFind() ){
     if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
@@ -141,27 +145,38 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
   if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
     return r;
   }else{
-    TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
-    std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
-    if( itir==d_int_rep[v_tn].end() ){
+    TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
+    std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
+    std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
+    if (itir != v_int_rep.end())
+    {
+      return itir->second;
+    }
+    else
+    {
       //find best selection for representative
       Node r_best;
-      //if( options::fmfRelevantDomain() && !f.isNull() ){
-      //  Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
-      //  r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
-      //  Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
+      // if( options::fmfRelevantDomain() && !q.isNull() ){
+      //  Trace("internal-rep-debug") << "Consult relevant domain to mkRep " <<
+      //  r << std::endl;
+      //  r_best = d_qe->getRelevantDomain()->getRelevantTerm( q, index, r );
+      //  Trace("internal-rep-debug") << "Returned " << r_best << " " << r <<
+      //  std::endl;
       //}
       std::vector< Node > eqc;
       getEquivalenceClass( r, eqc );
       Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
       for( unsigned i=0; i<eqc.size(); i++ ){
-        if( i>0 ) Trace("internal-rep-select") << ", ";
+        if (i > 0)
+        {
+          Trace("internal-rep-select") << ", ";
+        }
         Trace("internal-rep-select") << eqc[i];
       }
       Trace("internal-rep-select")  << " }, type = " << v_tn << std::endl;
       int r_best_score = -1;
       for( size_t i=0; i<eqc.size(); i++ ){
-        int score = getRepScore( eqc[i], f, index, v_tn );
+        int score = getRepScore(eqc[i], q, index, v_tn);
         if( score!=-2 ){
           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
             r_best = eqc[i];
@@ -182,14 +197,12 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       }
       Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
       Assert( r_best.getType().isSubtypeOf( v_tn ) );
-      d_int_rep[v_tn][r] = r_best;
+      v_int_rep[r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
       }
       return r_best;
-    }else{
-      return itir->second;
     }
   }
 }
@@ -311,7 +324,11 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod
 }
 
 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
+int EqualityQueryQuantifiersEngine::getRepScore(Node n,
+                                                Node q,
+                                                int index,
+                                                TypeNode v_tn)
+{
   if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
     return -2;
   }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
@@ -335,3 +352,7 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, Type
     }
   }
 }
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index c3e0a8c5b..0048cc14f 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -17,17 +17,87 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
 #define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
 
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-// TODO : (as part of #1171, #1214) further document and clean this class.
-/** equality query object using theory engine */
+/** EqualityQueryQuantifiersEngine class
+* This is a wrapper class around an equality engine that is used for
+* queries required by algorithms in the quantifiers theory.
+* It uses an equality engine, as determined by the quantifiers engine it points
+* to.
+*
+* The main extension of this class wrt EqualityQuery is the function
+* getInternalRepresentative, which is used by instantiation-based methods
+* that are agnostic with respect to choosing terms within an equivalence class.
+* Examples of such methods are finite model finding and enumerative
+* instantiation.
+* Method getInternalRepresentative returns the "best" representative based on
+* the internal heuristic,
+* which is currently based on choosing the term that was previously chosen as a
+* representative
+* earliest.
+*/
 class EqualityQueryQuantifiersEngine : public EqualityQuery
 {
-private:
+ public:
+  EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
+  virtual ~EqualityQueryQuantifiersEngine();
+  /** reset */
+  virtual bool reset(Theory::Effort e);
+  /* Called for new quantifiers */
+  virtual void registerQuantifier(Node q) {}
+  /** identify */
+  virtual std::string identify() const { return "EqualityQueryQE"; }
+  /** does the equality engine have term a */
+  bool hasTerm(Node a);
+  /** get the representative of a */
+  Node getRepresentative(Node a);
+  /** are a and b equal? */
+  bool areEqual(Node a, Node b);
+  /** are a and b disequal? */
+  bool areDisequal(Node a, Node b);
+  /** get equality engine
+  * This may either be the master equality engine or the model's equality
+  * engine.
+  */
+  eq::EqualityEngine* getEngine();
+  /** get list of members in the equivalence class of a */
+  void getEquivalenceClass(Node a, std::vector<Node>& eqc);
+  /** get congruent term
+  * If possible, returns a term n such that:
+  * (1) n is a term in the equality engine from getEngine().
+  * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class
+  * of args[i] for i=1...k
+  * Otherwise, returns the null node.
+  *
+  * Notice that f should be a "match operator", returned by
+  * TermDb::getMatchOperator.
+  */
+  TNode getCongruentTerm(Node f, std::vector<TNode>& args);
+  /** gets the current best representative in the equivalence
+   * class of a, based on some heuristic. Currently, the default heuristic
+   * chooses terms that were previously chosen as representatives
+   * on the earliest instantiation round.
+   *
+   * If q is non-null, then q/index is the quantified formula
+   * and variable position that we are choosing for instantiation.
+   *
+   * This function avoids certain terms that are "ineligible" for instantiation.
+   * If cbqi is active, we terms that contain instantiation constants
+   * are ineligible. As a result, this function may return
+   * Node::null() if all terms in the equivalence class of a
+   * are ineligible.
+   */
+  Node getInternalRepresentative(Node a, Node q, int index);
+
+ private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
   /** quantifiers equality inference */
@@ -36,9 +106,8 @@ private:
   std::map< TypeNode, std::map< Node, Node > > d_int_rep;
   /** rep score */
   std::map< Node, int > d_rep_score;
-  /** reset count */
+  /** the number of times reset( e ) has been called */
   int d_reset_count;
-
   /** processInferences : will merge equivalence classes in master equality engine, if possible */
   bool processInferences( Theory::Effort e );
   /** node contains */
@@ -47,26 +116,6 @@ private:
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
   /** flatten representatives */
   void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
-public:
-  EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
-  virtual ~EqualityQueryQuantifiersEngine();
-  /** reset */
-  bool reset( Theory::Effort e );
-  /** identify */
-  std::string identify() const { return "EqualityQueryQE"; }
-  /** general queries about equality */
-  bool hasTerm( Node a );
-  Node getRepresentative( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  eq::EqualityEngine* getEngine();
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
-  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
-  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
-      If cbqi is active, this will return a term in the equivalence class of "a" that does
-      not contain instantiation constants, if such a term exists.
-   */
-  Node getInternalRepresentative( Node a, Node f, int index );
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index db43d8bca..b0f118ad5 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -30,9 +30,10 @@ using namespace CVC4::theory::quantifiers::fmcheck;
 struct ModelBasisArgSort
 {
   std::vector< Node > d_terms;
+  // number of arguments that are model-basis terms
+  std::unordered_map<Node, unsigned, NodeHashFunction> d_mba_count;
   bool operator() (int i,int j) {
-    return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
-            d_terms[j].getAttribute(ModelBasisArgAttribute()) );
+    return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]);
   }
 };
 
@@ -502,8 +503,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     std::vector< int > indices;
     ModelBasisArgSort mbas;
     for (int i=0; i<(int)conds.size(); i++) {
-      d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
       mbas.d_terms.push_back(conds[i]);
+      mbas.d_mba_count[conds[i]] =
+          d_qe->getTermDatabase()->getModelBasisArg(conds[i]);
       indices.push_back(i);
     }
     std::sort( indices.begin(), indices.end(), mbas );
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 6c058c258..580923fc9 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -38,9 +38,11 @@ public:
   EqualityQueryInstProp( QuantifiersEngine* qe );
   ~EqualityQueryInstProp(){};
   /** reset */
-  bool reset( Theory::Effort e );
+  virtual bool reset(Theory::Effort e);
+  /* Called for new quantifiers */
+  virtual void registerQuantifier(Node q) {}
   /** identify */
-  std::string identify() const { return "EqualityQueryInstProp"; }
+  virtual std::string identify() const { return "EqualityQueryInstProp"; }
   /** extends engine */
   bool extendsEngine() { return true; }
   /** contains term */
@@ -161,9 +163,11 @@ public:
   InstPropagator( QuantifiersEngine* qe );
   ~InstPropagator(){}
   /** reset */
-  bool reset( Theory::Effort e );
+  virtual bool reset(Theory::Effort e) override;
+  /* Called for new quantifiers */
+  virtual void registerQuantifier(Node q) override {}
   /** identify */
-  std::string identify() const { return "InstPropagator"; }
+  virtual std::string identify() const override { return "InstPropagator"; }
   /** get the notify mechanism */
   InstantiationNotify* getInstantiationNotify() { return &d_notify; }
 };
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 07df8bb21..ad6ab509d 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -19,6 +19,7 @@
 
 #include <iostream>
 #include <map>
+#include <vector>
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -33,52 +34,129 @@ namespace quantifiers {
   class TermUtil;
 }
 
+/** QuantifiersModule class
+*
+* This is the virtual class for defining subsolvers of the quantifiers theory.
+* It has a similar interface to a Theory object.
+*/
 class QuantifiersModule {
-protected:
-  QuantifiersEngine* d_quantEngine;
 public:
   QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   virtual ~QuantifiersModule(){}
-  //get quantifiers engine
-  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
-  /** presolve */
+  /** Presolve.
+   *
+   * Called at the beginning of check-sat call.
+   */
   virtual void presolve() {}
-  /* whether this module needs to check this round */
+  /** Needs check.
+   *
+   * Returns true if this module wishes a call to be made
+   * to check(e) during QuantifiersEngine::check(e).
+   */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
-  /* whether this module needs a model built */
+  /** Needs model.
+   *
+   * Whether this module needs a model built during a
+   * call to QuantifiersEngine::check(e)
+   * It returns one of QEFFORT_* from quantifiers_engine.h,
+   * which specifies the quantifiers effort in which it requires the model to
+   * be built.
+   */
   virtual unsigned needsModel( Theory::Effort e );
-  /* reset at a round */
+  /** Reset.
+   *
+   * Called at the beginning of QuantifiersEngine::check(e).
+   */
   virtual void reset_round( Theory::Effort e ){}
-  /* Call during quantifier engine's check */
+  /** Check.
+   *
+   *   Called during QuantifiersEngine::check(e) depending
+   *   if needsCheck(e) returns true.
+   */
   virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
-  /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */
+  /** Check complete?
+   *
+   * Returns false if the module's reasoning was globally incomplete
+   * (e.g. "sat" must be replaced with "incomplete").
+   *
+   * This is called just before the quantifiers engine will return
+   * with no lemmas added during a LAST_CALL effort check.
+   */
   virtual bool checkComplete() { return true; }
-  /* check was complete for quantified formula q (e.g. no lemmas implies a model) */
+  /** Check was complete for quantified formula q
+   *
+   * If for each quantified formula q, some module returns true for
+   * checkCompleteFor( q ),
+   * and no lemmas are added by the quantifiers theory, then we may answer
+   * "sat", unless
+   * we are incomplete for other reasons.
+   */
   virtual bool checkCompleteFor( Node q ) { return false; }
-  /* Called for new quantified formulas */
+  /** Pre register quantifier.
+   *
+   * Called once for new quantified formulas that are
+   * pre-registered by the quantifiers theory.
+   */
   virtual void preRegisterQuantifier( Node q ) { }
-  /* Called for new quantifiers after owners are finalized */
+  /** Register quantifier
+   *
+   * Called once for new quantified formulas that are
+   * pre-registered by the quantifiers theory, after
+   * internal ownership of quantified formulas is finalized.
+   */
   virtual void registerQuantifier( Node q ) = 0;
-  virtual void assertNode( Node n ) {}
-  virtual void propagate( Theory::Effort level ){}
+  /** Assert node.
+   *
+   * Called when a quantified formula q is asserted to the quantifiers theory
+   */
+  virtual void assertNode(Node q) {}
+  /* Get the next decision request.
+   *
+   * Identical to Theory::getNextDecisionRequest(...)
+   */
   virtual Node getNextDecisionRequest( unsigned& priority ) { return TNode::null(); }
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
-public:
+  //----------------------------general queries
+  /** get currently used the equality engine */
   eq::EqualityEngine * getEqualityEngine();
-  bool areDisequal( TNode n1, TNode n2 );
+  /** are n1 and n2 equal in the current used equality engine? */
   bool areEqual( TNode n1, TNode n2 );
+  /** are n1 and n2 disequal in the current used equality engine? */
+  bool areDisequal(TNode n1, TNode n2);
+  /** get the representative of n in the current used equality engine */
   TNode getRepresentative( TNode n );
+  /** get quantifiers engine that owns this module */
+  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+  /** get currently used term database */
   quantifiers::TermDb * getTermDatabase();
+  /** get currently used term utility object */
   quantifiers::TermUtil * getTermUtil();
+  //----------------------------end general queries
+ protected:
+  /** pointer to the quantifiers engine that owns this module */
+  QuantifiersEngine* d_quantEngine;
 };/* class QuantifiersModule */
 
+/** Quantifiers utility
+*
+* This is a lightweight version of a quantifiers module that does not implement
+* methods
+* for checking satisfiability.
+*/
 class QuantifiersUtil {
 public:
   QuantifiersUtil(){}
   virtual ~QuantifiersUtil(){}
-  /* reset at a round */
+  /* reset
+  * Called at the beginning of an instantiation round
+  * Returns false if the reset failed. When reset fails, the utility should have
+  * added a lemma
+  * via a call to qe->addLemma. TODO: improve this contract #1163
+  */
   virtual bool reset( Theory::Effort e ) = 0;
+  /* Called for new quantifiers */
+  virtual void registerQuantifier(Node q) = 0;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
 };
@@ -238,8 +316,12 @@ public:
  static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c);
 };
 
-
-class QuantRelevance
+/** QuantRelevance
+* This class is used for implementing SinE-style heuristics (e.g. see Hoder et
+* al CADE 2011)
+* This is enabled by the option --relevant-triggers.
+*/
+class QuantRelevance : public QuantifiersUtil
 {
 private:
   /** for computing relevance */
@@ -255,8 +337,12 @@ private:
 public:
   QuantRelevance( bool cr ) : d_computeRel( cr ){}
   ~QuantRelevance(){}
-  /** register quantifier */
-  void registerQuantifier( Node f );
+  virtual bool reset(Theory::Effort e) override { return true; }
+  /** Called for new quantifiers after ownership of quantified formulas are
+   * finalized */
+  virtual void registerQuantifier(Node q) override;
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  virtual std::string identify() const override { return "QuantRelevance"; }
   /** set relevance */
   void setRelevance( Node s, int r );
   /** get relevance */
@@ -288,7 +374,9 @@ public:
   static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 };
 
-
+/** EqualityQuery
+* This is a wrapper class around equality engine.
+*/
 class EqualityQuery : public QuantifiersUtil {
 public:
   EqualityQuery(){}
@@ -307,7 +395,8 @@ public:
   virtual eq::EqualityEngine* getEngine() = 0;
   /** get the equivalence class of a */
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-  /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */
+  /** get the term that exists in EE that is congruent to f with args (f is
+   * returned by TermDb::getMatchOperator(...)) */
   virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
 };/* class EqualityQuery */
 
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index c9a7f07ab..d02ad667e 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -22,11 +22,12 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : 
 d_quantEngine(qe) {
@@ -94,7 +95,10 @@ bool QuantAttributes::checkRewriteRule( Node q ) {
 }
 
 Node QuantAttributes::getRewriteRule( Node q ) {
-  if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
+  if (q.getKind() == FORALL && q.getNumChildren() == 3
+      && q[2][0].getNumChildren() > 0
+      && q[2][0][0].getKind() == REWRITE_RULE)
+  {
     return q[2][0][0];
   }else{
     return Node::null();
@@ -121,12 +125,13 @@ bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
 Node QuantAttributes::getFunDefHead( Node q ) {
   //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
   if( q.getKind()==FORALL && q.getNumChildren()==3 ){
-
-    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
-      if( q[2][i].getKind()==INST_ATTRIBUTE ){
-        if( q[2][i][0].getAttribute(FunDefAttribute()) ){
-          return q[2][i][0];
-        }
+    Node ipl = q[2];
+    for (unsigned i = 0; i < ipl.getNumChildren(); i++)
+    {
+      if (ipl[i].getKind() == INST_ATTRIBUTE
+          && ipl[i][0].getAttribute(FunDefAttribute()))
+      {
+        return ipl[i][0];
       }
     }
   }
@@ -197,7 +202,7 @@ void QuantAttributes::computeAttributes( Node q ) {
     Node f = d_qattr[q].d_fundef_f;
     if( d_fun_defs.find( f )!=d_fun_defs.end() ){
       Message() << "Cannot define function " << f << " more than once." << std::endl;
-      exit( 1 );
+      AlwaysAssert(false);
     }
     d_fun_defs[f] = true;
     d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
@@ -383,3 +388,6 @@ Node QuantAttributes::getQuantIdNumNode( Node q ) {
   }
 }
 
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 1c35b646b..b618fc5d5 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -61,34 +61,53 @@ namespace quantifiers {
 //struct RrPriorityAttributeId {};
 //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
 
-
-/** This class stores attributes for quantified formulas 
-* TODO : document (as part of #1171, #1215)
-*/
-class QAttributes{
-public:
+/** This struct stores attributes for a single quantified formula */
+struct QAttributes
+{
+ public:
   QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
                   d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
   ~QAttributes(){}
+  /** does the quantified formula have a pattern? */
   bool d_hasPattern;
+  /** if non-null, this is the rewrite rule representation of the quantified
+   * formula */
   Node d_rr;
+  /** is this formula marked a conjecture? */
   bool d_conjecture;
+  /** is this formula marked an axiom? */
   bool d_axiom;
+  /** if non-null, this quantified formula is a function definition for function
+   * d_fundef_f */
   Node d_fundef_f;
+  /** is this formula marked as a sygus conjecture? */
   bool d_sygus;
+  /** is this formula marked as a synthesis (non-sygus) conjecture? */
   bool d_synthesis;
+  /** if a rewrite rule, then this is the priority value for the rewrite rule */
   int d_rr_priority;
+  /** stores the maximum instantiation level allowed for this quantified formula
+   * (-1 means allow any) */
   int d_qinstLevel;
+  /** is this formula marked for quantifier elimination? */
   bool d_quant_elim;
+  /** is this formula marked for partial quantifier elimination? */
   bool d_quant_elim_partial;
+  /** the instantiation pattern list for this quantified formula (its 3rd child)
+   */
   Node d_ipl;
+  /** the quantifier id associated with this formula */
   Node d_qid_num;
+  /** is this quantified formula a rewrite rule? */
   bool isRewriteRule() { return !d_rr.isNull(); }
+  /** is this quantified formula a function definition? */
   bool isFunDef() { return !d_fundef_f.isNull(); }
 };
 
-/** This class caches information about attributes of quantified formulas 
-* It also has static utility functions used for determining attributes and information about 
+/** This class caches information about attributes of quantified formulas
+*
+* It also has static utility functions used for determining attributes and
+* information about
 * quantified formulas.
 */
 class QuantAttributes
@@ -96,14 +115,23 @@ class QuantAttributes
 public:
   QuantAttributes( QuantifiersEngine * qe );
   ~QuantAttributes(){}
-  
   /** set user attribute
-    *   This function will apply a custom set of attributes to all top-level universal
-    *   quantifiers contained in n
-    */
-  static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value );
-  
-  //general queries concerning quantified formulas wrt modules
+  * This function applies an attribute
+  * This can be called when we mark expressions with attributes, e.g. (! q
+  * :attribute attr [node_values, str_value...]),
+  * It can also be called internally in various ways (for SyGus, quantifier
+  * elimination, etc.)
+  */
+  static void setUserAttribute(const std::string& attr,
+                               Node q,
+                               std::vector<Node>& node_values,
+                               std::string str_value);
+
+  /** compute quantifier attributes */
+  static void computeQuantAttributes(Node q, QAttributes& qa);
+  /** compute the attributes for q */
+  void computeAttributes(Node q);
+
   /** is quantifier treated as a rewrite rule? */
   static bool checkRewriteRule( Node q );
   /** get the rewrite rule associated with the quanfied formula */
@@ -145,10 +173,7 @@ public:
   int getQuantIdNum( Node q );
   /** get quant id num */
   Node getQuantIdNumNode( Node q );
-  /** compute quantifier attributes */
-  static void computeQuantAttributes( Node q, QAttributes& qa );
-  /** compute the attributes for q */
-  void computeAttributes( Node q );
+
 private:
   /** pointer to quantifiers engine */
   QuantifiersEngine * d_quantEngine;
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 749026b66..dcd24b433 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -98,6 +98,7 @@ bool RelevantDomain::reset( Theory::Effort e ) {
   return true;
 }
 
+void RelevantDomain::registerQuantifier(Node q) {}
 void RelevantDomain::compute(){
   if( !d_is_computed ){
     d_is_computed = true;
@@ -116,11 +117,12 @@ void RelevantDomain::compute(){
 
     Trace("rel-dom-debug") << "account for ground terms" << std::endl;
     TermDb * db = d_qe->getTermDatabase();
-    for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
-      Node op = it->first;
+    for (unsigned k = 0; k < db->getNumOperators(); k++)
+    {
+      Node op = db->getOperator(k);
       unsigned sz = db->getNumGroundTerms( op );
       for( unsigned i=0; i<sz; i++ ){
-        Node n = it->second[i];
+        Node n = db->getGroundTerm(op, i);
         //if it is a non-redundant term
         if( db->isTermActive( n ) ){
           for( unsigned j=0; j<n.getNumChildren(); j++ ){
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 6594b7352..fbf3520c6 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -23,31 +23,104 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+/** Relevant Domain
+ *
+ * This class computes the relevant domain of
+ * functions and quantified formulas based on
+ * techniques from "Complete Instantiation for Quantified
+ * Formulas in SMT" by Ge et al., CAV 2009.
+ *
+ * Calling compute() will compute a representation
+ * of relevant domain information, which be accessed
+ * by getRDomain(...) calls. It is intended to be called
+ * at full effort check, after we have initialized
+ * the term database.
+ */
 class RelevantDomain : public QuantifiersUtil
 {
-private:
+ public:
+  RelevantDomain(QuantifiersEngine* qe);
+  virtual ~RelevantDomain();
+  /** Reset. */
+  virtual bool reset(Theory::Effort e) override;
+  /** Register the quantified formula q */
+  virtual void registerQuantifier(Node q) override;
+  /** identify */
+  virtual std::string identify() const override { return "RelevantDomain"; }
+  /** Compute the relevant domain */
+  void compute();
+  /** Relevant domain representation.
+   *
+   * This data structure is inspired by the paper
+   * "Complete Instantiation for Quantified Formulas in SMT" by
+   * Ge et al., CAV 2009.
+   * Notice that relevant domains may be equated to one another,
+   * for example, if the quantified formula forall x. P( x, x )
+   * exists in the current context, then the relevant domain of
+   * arguments 1 and 2 of P are equated.
+   */
   class RDomain
   {
   public:
     RDomain() : d_parent( NULL ) {}
-    void reset() { d_parent = NULL; d_terms.clear(); }
-    RDomain * d_parent;
+    /** the set of terms in this relevant domain */
     std::vector< Node > d_terms;
+    /** reset this object */
+    void reset()
+    {
+      d_parent = NULL;
+      d_terms.clear();
+    }
+    /** merge this with r
+     * This sets d_parent of this to r and
+     * copies the terms of this to r.
+     */
     void merge( RDomain * r );
+    /** add term to the relevant domain */
     void addTerm( Node t );
+    /** get the parent of this */
     RDomain * getParent();
+    /** remove redundant terms for d_terms, removes
+     * duplicates modulo equality.
+     */
     void removeRedundantTerms( QuantifiersEngine * qe );
+    /** is n in this relevant domain? */
     bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
+
+   private:
+    /** the parent of this relevant domain */
+    RDomain* d_parent;
   };
+  /** get the relevant domain
+   *
+   * Gets object representing the relevant domain of the i^th argument of n.
+   *
+   * If getParent is true, we return the representative
+   * of the equivalence class of relevant domain objects,
+   * which is computed as a union find (see RDomain::d_parent).
+   */
+  RDomain* getRDomain(Node n, int i, bool getParent = true);
+
+ private:
+  /** the relevant domains for each quantified formula and function,
+   * for each variable # and argument #.
+   */
   std::map< Node, std::map< int, RDomain * > > d_rel_doms;
+  /** stores the function or quantified formula associated with
+   * each relevant domain object.
+   */
   std::map< RDomain *, Node > d_rn_map;
+  /** stores the argument or variable number associated with
+   * each relevant domain object.
+   */
   std::map< RDomain *, int > d_ri_map;
+  /** Quantifiers engine associated with this utility. */
   QuantifiersEngine* d_qe;
-  void computeRelevantDomain( Node q, Node n, bool hasPol, bool pol );
-  void computeRelevantDomainOpCh( RDomain * rf, Node n );
+  /** have we computed the relevant domain on this full effort check? */
   bool d_is_computed;
-  
-  //what each literal does
+  /** relevant domain literal
+   * Caches the effect of literals on the relevant domain.
+   */
   class RDomainLit {
   public:
     RDomainLit() : d_merge(false){
@@ -55,23 +128,33 @@ private:
       d_rd[1] = NULL;
     }
     ~RDomainLit(){}
+    /** whether this literal forces the merge of two relevant domains */
     bool d_merge;
+    /** the relevant domains that are merged as a result
+     * of this literal
+     */
     RDomain * d_rd[2];
+    /** the terms that are added to
+     * the relevant domain as a result of this literal
+     */
     std::vector< Node > d_val;
   };
+  /** Cache of the effect of literals on the relevant domain */
   std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit;
+  /** Compute the relevant domain for a subformula n of q,
+   * whose polarity is given by hasPol/pol.
+   */
+  void computeRelevantDomain(Node q, Node n, bool hasPol, bool pol);
+  /** Compute the relevant domain when the term n
+   * is in a position to be included in relevant domain rf.
+   */
+  void computeRelevantDomainOpCh(RDomain* rf, Node n);
+  /** compute relevant domain for literal.
+   *
+   * Updates the relevant domains based on a literal n in quantified
+   * formula q whose polarity is given by hasPol/pol.
+   */
   void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n );
-public:
-  RelevantDomain( QuantifiersEngine* qe );
-  virtual ~RelevantDomain();
-  /* reset */
-  bool reset( Theory::Effort e );
-  /** identify */
-  std::string identify() const { return "RelevantDomain"; }
-  //compute the relevant domain
-  void compute();
-
-  RDomain * getRDomain( Node n, int i, bool getParent = true );
 };/* class RelevantDomain */
 
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d4a71e43c..59405a5d5 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -104,6 +104,13 @@ void TermDb::registerQuantifier( Node q ) {
   }
 }
 
+unsigned TermDb::getNumOperators() { return d_ops.size(); }
+Node TermDb::getOperator(unsigned i)
+{
+  Assert(i < d_ops.size());
+  return d_ops[i];
+}
+
 /** ground terms */
 unsigned TermDb::getNumGroundTerms( Node f ) {
   std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
@@ -178,6 +185,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           
           Node op = getMatchOperator( n );
           Trace("term-db-debug") << "  match operator is : " << op << std::endl;
+          d_ops.push_back(op);
           d_op_map[op].push_back( n );
           added.insert( n );
           
@@ -720,7 +728,9 @@ void TermDb::setHasTerm( Node n ) {
 
 void TermDb::presolve() {
   if( options::incrementalSolving() ){
-    //reset the caches that are SAT context-independent
+    // reset the caches that are SAT context-independent but user
+    // context-dependent
+    d_ops.clear();
     d_op_map.clear();
     d_type_map.clear();
     d_processed.clear();
@@ -969,6 +979,12 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
   }
 }
 
+unsigned TermDb::getModelBasisArg(Node n)
+{
+  computeModelBasisArgAttribute(n);
+  return n.getAttribute(ModelBasisArgAttribute());
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index f4c6c3877..c5165ec2c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -37,18 +37,65 @@ 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:
-  bool hasNodeData() { return !d_data.empty(); }
-  TNode getNodeData() { return d_data.begin()->first; }
-  TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 );
-  TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
-  bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
-  void debugPrint( const char * c, Node n, unsigned depth = 0 );
-  void clear() { d_data.clear(); }
+ /** 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(); }
 };/* class TermArgTrie */
 
 namespace fmcheck {
@@ -62,19 +109,199 @@ class ConjectureGenerator;
 class TermGenerator;
 class TermGenEnv;
 
+/** Term Database
+*
+* 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. This
+*     is done lazily, for performance reasons.
+*/
 class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::QuantifiersEngine;
-  //TODO: eliminate most of these
-  friend class ::CVC4::theory::inst::Trigger;
-  friend class ::CVC4::theory::inst::HigherOrderTrigger;
-  friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
-  friend class ::CVC4::theory::quantifiers::QuantConflictFind;
-  friend class ::CVC4::theory::quantifiers::RelevantDomain;
+  // TODO: eliminate these
   friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
   friend class ::CVC4::theory::quantifiers::TermGenEnv;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-private:
+
+ public:
+  TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+  ~TermDb();
+  /** presolve (called once per user check-sat) */
+  void presolve();
+  /** reset (calculate which terms are active) */
+  virtual bool reset(Theory::Effort effort) override;
+  /** register quantified formula */
+  virtual void registerQuantifier(Node q) override;
+  /** identify */
+  virtual std::string identify() const override { return "TermDb"; }
+  /** get number of operators */
+  unsigned getNumOperators();
+  /** get operator at index i */
+  Node getOperator(unsigned i);
+  /** ground terms for operator
+  * Get the number of ground terms with operator f that have been added to the
+  * database
+  */
+  unsigned getNumGroundTerms(Node f);
+  /** get ground term for operator
+  * Get the i^th ground term with operator f that has been added to the database
+  */
+  Node getGroundTerm(Node f, unsigned i);
+  /** get num type terms
+  * Get the number of ground terms of tn that have been added to the database
+  */
+  unsigned getNumTypeGroundTerms(TypeNode tn);
+  /** get type ground term
+  * Returns the i^th ground term of type tn
+  */
+  Node getTypeGroundTerm(TypeNode tn, unsigned i);
+  /** add a term to the database
+  * withinQuant is whether n is within the body of a quantified formula
+  * withinInstClosure is whether n is within an inst-closure operator (see
+  * Bansal et al CAV 2015).
+  */
+  void addTerm(Node n,
+               std::set<Node>& added,
+               bool withinQuant = false,
+               bool withinInstClosure = false);
+  /** get match operator for term n
+  *
+  * If n has a kind that we index, this function will
+  * typically return n.getOperator().
+  *
+  * However, for parametric operators f, the match operator is an arbitrary
+  * chosen f-application.  For example, consider array select:
+  * A : (Array Int Int)
+  * B : (Array Bool Int)
+  * We require that terms like (select A 1) and (select B 2) are indexed in
+  * separate
+  * data structures despite the fact that
+  *    (select A 1).getOperator()==(select B 2).getOperator().
+  * Hence, for the above terms, we may return:
+  * getMatchOperator( (select A 1) ) = (select A 1), and
+  * getMatchOperator( (select B 2) ) = (select B 2).
+  * The match operator is the first instance of an application of the parametric
+  * operator of its type.
+  *
+  * If n has a kind that we do not index (like PLUS),
+  * then this function returns Node::null().
+  */
+  Node getMatchOperator(Node n);
+  /** get term arg index for all f-applications in the current context */
+  TermArgTrie* getTermArgTrie(Node f);
+  /** get the term arg trie for f-applications in the equivalence class of eqc.
+   */
+  TermArgTrie* 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,
+  * (2) t is of the form f( t1, ..., tk )
+  */
+  TNode getCongruentTerm(Node f, Node n);
+  /** get congruent term
+  * If possible, returns a term t such that:
+  * (1) t is a term that is currently indexed by this database,
+  * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ),
+  *     where ti is in the equivalence class of si for i=1...k
+  */
+  TNode getCongruentTerm(Node f, std::vector<TNode>& args);
+  /** in relevant domain
+  * Returns true if there is at least one term t such that:
+  * (1) t is a term that is currently indexed by this database,
+  * (2) t is of the form f( t1, ..., tk ) and ti is in the equivalence class of
+  * r.
+  */
+  bool inRelevantDomain(TNode f, unsigned i, TNode r);
+  /** evaluate term
+   *
+  * Returns a term n' such that n = n' is entailed based on the equality
+  * information qy.  This function may generate new terms. In particular,
+  * we typically rewrite maximal
+  * subterms of n to terms that exist in the equality engine specified by qy.
+  *
+  * useEntailmentTests is whether to use the theory engine's entailmentCheck
+  * call, for increased precision. This is not frequently used.
+  */
+  Node evaluateTerm(TNode n,
+                    EqualityQuery* qy = NULL,
+                    bool useEntailmentTests = false);
+  /** get entailed term
+   *
+  * If possible, returns a term n' such that:
+  * (1) n' exists in the current equality engine (as specified by qy),
+  * (2) n = n' is entailed in the current context.
+  * It returns null if no such term can be found.
+  * Wrt evaluateTerm, this version does not construct new terms, and
+  * thus is less aggressive.
+  */
+  TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL);
+  /** get entailed term
+   *
+  * If possible, returns a term n' such that:
+  * (1) n' exists in the current equality engine (as specified by qy),
+  * (2) n * subs = n' is entailed in the current context, where * is denotes
+  * substitution application.
+  * It returns null if no such term can be found.
+  * subsRep is whether the substitution maps to terms that are representatives
+  * according to qy.
+  * Wrt evaluateTerm, this version does not construct new terms, and
+  * thus is less aggressive.
+  */
+  TNode getEntailedTerm(TNode n,
+                        std::map<TNode, TNode>& subs,
+                        bool subsRep,
+                        EqualityQuery* qy = NULL);
+  /** is entailed
+  * Checks whether the current context entails n with polarity pol, based on the
+  * equality information qy.
+  * Returns true if the entailment can be successfully shown.
+  */
+  bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL);
+  /** is entailed
+   *
+  * Checks whether the current context entails ( n * subs ) with polarity pol,
+  * based on the equality information qy,
+  * where * denotes substitution application.
+  * subsRep is whether the substitution maps to terms that are representatives
+  * according to qy.
+  */
+  bool isEntailed(TNode n,
+                  std::map<TNode, TNode>& subs,
+                  bool subsRep,
+                  bool pol,
+                  EqualityQuery* qy = NULL);
+  /** is the term n active in the current context?
+   *
+  * By default, all terms are active. A term is inactive if:
+  * (1) it is congruent to another term
+  * (2) it is irrelevant based on the term database mode. This includes terms
+  * that only appear in literals that are not relevant.
+  * (3) it contains instantiation constants (used for CEGQI and cannot be used
+  * in instantiation).
+  * (4) it is explicitly set inactive by a call to setTermInactive(...).
+  * We store whether a term is inactive in a SAT-context-dependent map.
+  */
+  bool isTermActive(Node n);
+  /** set that term n is inactive in this context. */
+  void setTermInactive(Node n);
+  /** has term current
+   *
+  * This function is used in cases where we restrict which terms appear in the
+  * database, such as for heuristics used in local theory extensions
+  * and for --term-db-mode=relevant.
+  * It returns whether the term n should be indexed in the current context.
+  */
+  bool hasTermCurrent(Node n, bool useMode = true);
+  /** is term eligble for instantiation? */
+  bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false);
+  /** get eligible term in equivalence class */
+  Node getEligibleTermInEqc(TNode r);
+  /** is inst closure */
+  bool isInstClosure(Node r);
+
+ private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
   /** terms processed */
@@ -88,30 +315,17 @@ private:
   /** boolean terms */
   Node d_true;
   Node d_false;
-public:
-  TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
-  ~TermDb();
-  
-  /** register quantified formula */
-  void registerQuantifier( Node q );
-public:
-  /** presolve (called once per user check-sat) */
-  void presolve();
-  /** reset (calculate which terms are active) */
-  bool reset( Theory::Effort effort );
-  /** identify */
-  std::string identify() const { return "TermDb"; }  
-private:
+  /** list of all operators */
+  std::vector<Node> d_ops;
   /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** map from type nodes to terms of that type */
   std::map< TypeNode, std::vector< Node > > d_type_map;
   /** inactive map */
   NodeBoolMap d_inactive_map;
-
-  /** count number of non-redundant ground terms per operator */
+  /** count of the number of non-redundant ground terms per operator */
   std::map< Node, int > d_op_nonred_count;
-  /**mapping from UF terms to representatives of their arguments */
+  /** 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;
@@ -124,88 +338,58 @@ private:
   std::map< Node, Node > d_term_elig_eqc;  
   /** set has term */
   void setHasTerm( Node n );
-  /** evaluate term */
+  /** helper for evaluate term */
   Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests );
+  /** helper for get entailed term */
   TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+  /** helper for is entailed */
   bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
-  /** compute uf eqc terms */
+  /** compute uf eqc terms :
+  * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
+  */
   void computeUfEqcTerms( TNode f );
-  /** compute uf terms */
+  /** compute uf terms
+  * Ensure that an entry for f is in d_func_map_trie
+  */
   void computeUfTerms( TNode f );
-private: // for higher-order term indexing
+  /** compute arg reps
+  * Ensure that an entry for n is in d_arg_reps
+  */
+  void computeArgReps(TNode n);
+  //------------------------------higher-order term indexing
   /** a map from matchable operators to their representative */
   std::map< TNode, TNode > d_ho_op_rep;
   /** for each representative matchable operator, the list of other matchable operators in their equivalence class */
   std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves;
   /** get operator representative */
   Node getOperatorRepresentative( TNode op ) const;
-public:
-  /** ground terms for operator */
-  unsigned getNumGroundTerms( Node f );
-  /** get ground term for operator */
-  Node getGroundTerm( Node f, unsigned i );
-  /** get num type terms */
-  unsigned getNumTypeGroundTerms( TypeNode tn );
-  /** get type ground term */
-  Node getTypeGroundTerm( TypeNode tn, unsigned i );
-  /** add a term to the database */
-  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
-  /** get match operator */
-  Node getMatchOperator( Node n );
-  /** get term arg index */
-  TermArgTrie * getTermArgTrie( Node f );
-  TermArgTrie * getTermArgTrie( Node eqc, Node f );
-  /** exists term */
-  TNode getCongruentTerm( Node f, Node n );
-  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
-  /** compute arg reps */
-  void computeArgReps( TNode n );
-  /** in relevant domain */
-  bool inRelevantDomain( TNode f, unsigned i, TNode r );
-  /** evaluate a term under a substitution.  Return representative in EE if possible.
-   * subsRep is whether subs contains only representatives
-   */
-  Node evaluateTerm( TNode n, EqualityQuery * qy = NULL, bool useEntailmentTests = false );
-  /** get entailed term, does not construct new terms, less aggressive */
-  TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL );
-  TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL );
-  /** is entailed (incomplete check) */
-  bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL );
-  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
-  /** is active */
-  bool isTermActive( Node n );
-  void setTermInactive( Node n );
-  /** has term */
-  bool hasTermCurrent( Node n, bool useMode = true );
-  /** is term eligble for instantiation? */
-  bool isTermEligibleForInstantiation( TNode n, TNode f, bool print = false );
-  /** get has term eqc */
-  Node getEligibleTermInEqc( TNode r );
-  /** is inst closure */
-  bool isInstClosure( Node r );
-  
-//for model basis
-private:
-  //map from types to model basis terms
+  //------------------------------end higher-order term indexing
+
+  // TODO : as part of #1171, these should be moved somewhere else
+  // for model basis
+ private:
+  /** map from types to model basis terms */
   std::map< TypeNode, Node > d_model_basis_term;
-  //map from ops to model basis terms
+  /** map from ops to model basis terms */
   std::map< Node, Node > d_model_basis_op_term;
-  //map from instantiation terms to their model basis equivalent
+  /** map from instantiation terms to their model basis equivalent */
   std::map< Node, Node > d_model_basis_body;
   /** map from universal quantifiers to model basis terms */
   std::map< Node, std::vector< Node > > d_model_basis_terms;
-  // compute model basis arg
+  /** compute model basis arg */
   void computeModelBasisArgAttribute( Node n );
-public:
-  //get model basis term
-  Node getModelBasisTerm( TypeNode tn, int i = 0 );
-  //get model basis term for op
-  Node getModelBasisOpTerm( Node op );
-  //get model basis
-  Node getModelBasis( Node q, Node n );
-  //get model basis body
-  Node getModelBasisBody( Node q );
-  
+ public:
+  /** get model basis term */
+  Node getModelBasisTerm(TypeNode tn, int i = 0);
+  /** get model basis term for op */
+  Node getModelBasisOpTerm(Node op);
+  /** get model basis */
+  Node getModelBasis(Node q, Node n);
+  /** get model basis body */
+  Node getModelBasisBody(Node q);
+  /** get model basis arg */
+  unsigned getModelBasisArg(Node n);
+
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index a0b3b8ec2..f5cfd6df8 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -21,6 +21,7 @@
 #include <unordered_set>
 
 #include "expr/attribute.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/type_enumerator.h"
 
 namespace CVC4 {
@@ -109,7 +110,8 @@ namespace quantifiers {
 class TermDatabase;
 
 // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
-class TermUtil {
+class TermUtil : public QuantifiersUtil
+{
   // TODO : remove these
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class TermDatabase;
@@ -126,11 +128,14 @@ public:
   Node d_zero;
   Node d_one;
 
+  /** reset */
+  virtual bool reset(Theory::Effort e) override { return true; }
   /** register quantifier */
-  void registerQuantifier( Node q );
-
-//for inst constant
-private:
+  virtual void registerQuantifier(Node q) override;
+  /** identify */
+  virtual std::string identify() const override { return "TermUtil"; }
+  // for inst constant
+ private:
   /** map from universal quantifiers to the list of variables */
   std::map< Node, std::vector< Node > > d_vars;
   std::map< Node, std::map< Node, unsigned > > d_var_num;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a8930de6e..fdb70c85b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,14 +62,15 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 QuantifiersEngine::QuantifiersEngine(context::Context* c,
-                                     context::UserContext* u, TheoryEngine* te)
+                                     context::UserContext* u,
+                                     TheoryEngine* te)
     : d_te(te),
+      d_quant_attr(new quantifiers::QuantAttributes(this)),
       d_conflict_c(c, false),
       // d_quants(u),
       d_quants_red(u),
       d_lemmas_produced_c(u),
       d_skolemized(u),
-      d_quant_attr(new quantifiers::QuantAttributes(this)),
       d_ierCounter_c(c),
       // d_ierCounter(c),
       // d_ierCounter_lc(c),
@@ -78,16 +79,19 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_presolve_in(u),
       d_presolve_cache(u),
       d_presolve_cache_wq(u),
-      d_presolve_cache_wic(u) {
+      d_presolve_cache_wic(u)
+{
   //utilities
   d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
   d_util.push_back( d_eq_query );
 
+  // term util must come first
+  d_term_util = new quantifiers::TermUtil(this);
+  d_util.push_back(d_term_util);
+
   d_term_db = new quantifiers::TermDb( c, u, this );
   d_util.push_back( d_term_db );
   
-  d_term_util = new quantifiers::TermUtil( this );
-  
   if (options::ceGuidedInst()) {
     d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
   }else{
@@ -122,6 +126,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
 
   if( options::relevantTriggers() ){
     d_quant_rel = new QuantRelevance( false );
+    d_util.push_back(d_quant_rel);
   }else{
     d_quant_rel = NULL;
   }
@@ -740,16 +745,14 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       d_quants[f] = false;
       return false;
     }else{
-      // register with utilities : TODO (#1163) make this a standard call
-      
-      d_term_util->registerQuantifier( f );
-      d_term_db->registerQuantifier( f );
-      d_quant_attr->computeAttributes( f );
-      //register with quantifier relevance
-      if( d_quant_rel ){
-        d_quant_rel->registerQuantifier( f );
+      // register with utilities
+      for (unsigned i = 0; i < d_util.size(); i++)
+      {
+        d_util[i]->registerQuantifier(f);
       }
-      
+      // compute attributes
+      d_quant_attr->computeAttributes(f);
+
       for( unsigned i=0; i<d_modules.size(); i++ ){
         Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
         d_modules[i]->preRegisterQuantifier( f );
@@ -765,10 +768,6 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       }
       //TODO: remove this
       Node ceBody = d_term_util->getInstConstantBody( f );
-      //also register it with the strong solver
-      //if( options::finiteModelFind() ){
-      //  ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
-      //}
       Trace("quant-debug")  << "...finish." << std::endl;
       d_quants[f] = true;
       // flush lemmas
@@ -821,9 +820,6 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 void QuantifiersEngine::propagate( Theory::Effort level ){
   CodeTimer codeTimer(d_statistics.d_time);
 
-  for( int i=0; i<(int)d_modules.size(); i++ ){
-    d_modules[i]->propagate( level );
-  }
 }
 
 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b1608e497..0bb5b10e5 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -124,7 +124,16 @@ private:
   quantifiers::QModelBuilder* d_builder;
   /** utility for effectively propositional logic */
   QuantEPR * d_qepr;
-private:
+  /** term database */
+  quantifiers::TermDb* d_term_db;
+  /** sygus term database */
+  quantifiers::TermDbSygus* d_sygus_tdb;
+  /** term utilities */
+  quantifiers::TermUtil* d_term_util;
+  /** quantifiers attributes */
+  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+
+ private:
   /** instantiation engine */
   quantifiers::InstantiationEngine* d_inst_engine;
   /** model engine */
@@ -155,7 +164,8 @@ private:
   quantifiers::QuantAntiSkolem * d_anti_skolem;
   /** quantifiers instantiation propagtor */
   quantifiers::InstPropagator * d_inst_prop;
-public: //effort levels
+
+ public:  // effort levels (TODO : make an enum and use everywhere #1293)
   enum {
     QEFFORT_CONFLICT,
     QEFFORT_STANDARD,
@@ -194,14 +204,6 @@ private:
   std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
   /** quantifiers that have been skolemized */
   BoolMap d_skolemized;
-  /** term database */
-  quantifiers::TermDb* d_term_db;
-  /** term database */
-  quantifiers::TermDbSygus* d_sygus_tdb;
-  /** term utilities */
-  quantifiers::TermUtil* d_term_util;
-  /** quantifiers attributes */
-  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
   /** extended model object */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1a72944ff..d9e89902c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -523,11 +523,10 @@ public:
 
   /** if theories want to do something with model after building, do it here */
   virtual void postProcessModel( TheoryModel* m ){ }
-
   /**
    * Return a decision request, if the theory has one, or the NULL node
    * otherwise.
-   * If returning non-null node, hould set priority to
+   * If returning non-null node, should set priority to
    *                        0 if decision is necessary for model-soundness,
    *                        1 if decision is necessary for completeness,
    *                        >1 otherwise.