(Refactor) Split term util (#1303)

* Fix some documentation.

* Move model basis out of term db.

* Moving

* Finished moving.

* Document Skolemize and term enumeration.

* Minor

* Model basis to first order model.

* Change function name.

* Minor

* Clang format.

* Minor

* Format

* Minor

* Format

* Address review.

28 files changed, 1185 insertions, 582 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 29bbc6a2c..c418d0fb1 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -12,17 +12,19 @@
  ** \brief Implementation of abstract MBQI builder
  **/
 
-
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ambqi_builder.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/term_database.h"
+#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 {
+
 
 void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {
   d_def.clear();
@@ -807,7 +809,7 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
     }
     if( fapps.empty() ){
       //choose arbitrary value
-      Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+      Node mbt = fm->getModelBasisOpTerm(f);
       Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
       fapps.push_back( mbt );
     }
@@ -958,3 +960,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod
     return true;
   }
 }
+
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 2a2ba8d4f..f3244937d 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -14,11 +14,12 @@
  ** This class manages integer bounds for quantifiers
  **/
 
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/bounded_integers.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
 
@@ -455,7 +456,9 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
       for( unsigned i=0; i<f[0].getNumChildren(); i++) {
         if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
           TypeNode tn = f[0][i].getType();
-          if( tn.isSort() || getTermUtil()->mayComplete( tn ) ){
+          if (tn.isSort()
+              || d_quantEngine->getTermEnumeration()->mayComplete(tn))
+          {
             success = true;
             setBoundedVar( f, f[0][i], BOUND_FINITE );
             break;
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 0a66109a0..712112615 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -302,7 +302,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
   if( d_firstTime ){
     //must return something
     d_firstTime = false;
-    return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
+    return d_qe->getTermForType(d_match_pattern_type);
   }
   return Node::null();
 }
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 7fcc3f2af..3af623f13 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -20,6 +20,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
@@ -296,7 +297,7 @@ void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& mode
     Node dr = Rewriter::rewrite( d[i] );
     if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
       if( constructed_cand ){
-        ic.push_back( d_qe->getTermUtil()->getSkolemizedBody( dr[0] ).negate() );
+        ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(dr[0]).negate());
       }
       if( sk_refine ){
         Assert( !isGround() );
@@ -347,9 +348,11 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){
     Node ce_q = d_ce_sk[0][k];
     if( !ce_q.isNull() ){
       Assert( !d_inner_vars_disj[k].empty() );
-      Assert( d_inner_vars_disj[k].size()==d_qe->getTermUtil()->d_skolem_constants[ce_q].size() );
+      std::vector<Node> skolems;
+      d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems);
+      Assert(d_inner_vars_disj[k].size() == skolems.size());
       std::vector< Node > model_values;
-      getModelValues( d_qe->getTermUtil()->d_skolem_constants[ce_q], model_values );
+      getModelValues(skolems, model_values);
       sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() );
       sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() );
     }else{
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 9d2d2fe98..c1b6c82ad 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
@@ -472,7 +473,8 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   Node s;
   if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
     Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl;
-    s = d_qe->getTermUtil()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
+    s = d_qe->getTermEnumeration()->getEnumerateTerm(
+        TypeNode::fromType(dt.getSygusType()), 0);
   }else{
     Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
     sol_index = d_prog_to_sol_index[prog];
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 9e69a31d3..a62b5f50b 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
@@ -676,7 +677,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
       std::vector< TypeNode > to_erase;
       for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){
         TypeNode stn = it->first;
-        Node ns = d_qe->getTermUtil()->getEnumerateTerm( stn, index );
+        Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(stn, index);
         if( ns.isNull() ){
           to_erase.push_back( stn );
         }else{
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index e7749cd92..36fac5e80 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -18,13 +18,13 @@
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
 
-
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -1139,7 +1139,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
 
 
 Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
-  d_closed_enum_type = qe->getTermUtil()->isClosedEnumerableType( tn );
+  d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn);
 }
 
 
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 508f58a07..e5a096c87 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -13,10 +13,12 @@
  **
  **/
 
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/conjecture_generator.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
@@ -398,7 +400,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
             std::vector< TNode > args;
             Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl;
             Node n;
-            if( getTermUtil()->isInductionTerm( r ) ){
+            if (Skolemize::isInductionTerm(r))
+            {
               n = d_op_arg_index[r].getGroundTerm( this, args );
             }else{
               n = r;
@@ -556,12 +559,13 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){
           //check each skolem variable
           bool disproven = true;
-          //std::vector< Node > sk;
-          //getTermUtil()->getSkolemConstants( q, sk, true );
+          std::vector<Node> skolems;
+          d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems);
           Trace("sg-conjecture") << "    CONJECTURE : ";
           std::vector< Node > ce;
-          for( unsigned j=0; j<getTermUtil()->d_skolem_constants[q].size(); j++ ){
-            TNode k = getTermUtil()->d_skolem_constants[q][j];
+          for (unsigned j = 0; j < skolems.size(); j++)
+          {
+            TNode k = skolems[j];
             TNode rk = getRepresentative( k );
             std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk );
             //check if it is a ground term
@@ -569,7 +573,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               Trace("sg-conjecture") << "ACTIVE : " << q;
               if( Trace.isOn("sg-gen-eqc") ){
                 Trace("sg-conjecture") << " { ";
-                for( unsigned k=0; k<getTermUtil()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermUtil()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; }
+                for (unsigned k = 0; k < skolems.size(); k++)
+                {
+                  Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "")
+                                         << " ";
+                }
                 Trace("sg-conjecture") << "}";
               }
               Trace("sg-conjecture") << std::endl;
@@ -1051,12 +1059,14 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
 
 void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
   if( n.getNumChildren()>0 ){
+    TermEnumeration* te = d_quantEngine->getTermEnumeration();
     std::vector< int > vec;
     std::vector< TypeNode > types;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       vec.push_back( 0 );
       TypeNode tn = n[i].getType();
-      if( getTermUtil()->isClosedEnumerableType( tn ) ){
+      if (te->isClosedEnumerableType(tn))
+      {
         types.push_back( tn );
       }else{
         return;
@@ -1074,7 +1084,9 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
         vec.push_back( size_limit );
       }else{
         //see if we can iterate current
-        if( vec_sum<size_limit && !getTermUtil()->getEnumerateTerm( types[index], vec[index]+1 ).isNull() ){
+        if (vec_sum < size_limit
+            && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull())
+        {
           vec[index]++;
           vec_sum++;
           vec.push_back( size_limit - vec_sum );
@@ -1089,7 +1101,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
       }
       if( success ){
         if( vec.size()==n.getNumChildren() ){
-          Node lc = getTermUtil()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] );
+          Node lc =
+              te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]);
           if( !lc.isNull() ){
             for( unsigned i=0; i<vec.size(); i++ ){
               Trace("sg-gt-enum-debug") << vec[i] << " ";
@@ -1102,7 +1115,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
             std::vector< Node > children;
             children.push_back( n.getOperator() );
             for( unsigned i=0; i<(vec.size()-1); i++ ){
-              Node nn = getTermUtil()->getEnumerateTerm( types[i], vec[i] );
+              Node nn = te->getEnumerateTerm(types[i], vec[i]);
               Assert( !nn.isNull() );
               Assert( nn.getType()==n[i].getType() );
               children.push_back( nn );
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 462dc23d0..f4cf1b32a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -12,13 +12,15 @@
  ** \brief Implementation of model engine model class
  **/
 
+#include "theory/quantifiers/first_order_model.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ambqi_builder.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 
 #define USE_INDEX_ORDERING
@@ -104,7 +106,7 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
   //check if there is even any domain elements at all
   if (!d_rep_set.hasType(tn)) {
     Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
-    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    Node mbt = getModelBasisTerm(tn);
     Trace("fmc-model-debug") << "Add to representative set..." << std::endl;
     d_rep_set.add(tn, mbt);
   }else if( d_rep_set.d_type_reps[tn].size()==0 ){
@@ -200,6 +202,118 @@ bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
   return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end();
 }
 
+Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
+{
+  if (d_model_basis_term.find(tn) == d_model_basis_term.end())
+  {
+    Node mbt;
+    if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+    {
+      mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+    }
+    else
+    {
+      if (options::fmfFreshDistConst())
+      {
+        mbt = d_qe->getTermDatabase()->getOrMakeTypeFreshVariable(tn);
+      }
+      else
+      {
+        mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+      }
+    }
+    ModelBasisAttribute mba;
+    mbt.setAttribute(mba, true);
+    d_model_basis_term[tn] = mbt;
+    Trace("model-basis-term") << "Choose " << mbt << " as model basis term for "
+                              << tn << std::endl;
+  }
+  return d_model_basis_term[tn];
+}
+
+bool FirstOrderModel::isModelBasisTerm(Node n)
+{
+  return n == getModelBasisTerm(n.getType());
+}
+
+Node FirstOrderModel::getModelBasisOpTerm(Node op)
+{
+  if (d_model_basis_op_term.find(op) == d_model_basis_op_term.end())
+  {
+    TypeNode t = op.getType();
+    std::vector<Node> children;
+    children.push_back(op);
+    for (int i = 0; i < (int)(t.getNumChildren() - 1); i++)
+    {
+      children.push_back(getModelBasisTerm(t[i]));
+    }
+    if (children.size() == 1)
+    {
+      d_model_basis_op_term[op] = op;
+    }
+    else
+    {
+      d_model_basis_op_term[op] =
+          NodeManager::currentNM()->mkNode(APPLY_UF, children);
+    }
+  }
+  return d_model_basis_op_term[op];
+}
+
+Node FirstOrderModel::getModelBasis(Node q, Node n)
+{
+  // make model basis
+  if (d_model_basis_terms.find(q) == d_model_basis_terms.end())
+  {
+    for (unsigned j = 0; j < q[0].getNumChildren(); j++)
+    {
+      d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
+    }
+  }
+  Node gn = d_qe->getTermUtil()->substituteInstConstants(
+      n, q, d_model_basis_terms[q]);
+  return gn;
+}
+
+Node FirstOrderModel::getModelBasisBody(Node q)
+{
+  if (d_model_basis_body.find(q) == d_model_basis_body.end())
+  {
+    Node n = d_qe->getTermUtil()->getInstConstantBody(q);
+    d_model_basis_body[q] = getModelBasis(q, n);
+  }
+  return d_model_basis_body[q];
+}
+
+void FirstOrderModel::computeModelBasisArgAttribute(Node n)
+{
+  if (!n.hasAttribute(ModelBasisArgAttribute()))
+  {
+    // ensure that the model basis terms have been defined
+    if (n.getKind() == APPLY_UF)
+    {
+      getModelBasisOpTerm(n.getOperator());
+    }
+    uint64_t val = 0;
+    // determine if it has model basis attribute
+    for (unsigned j = 0; j < n.getNumChildren(); j++)
+    {
+      if (n[j].getAttribute(ModelBasisAttribute()))
+      {
+        val++;
+      }
+    }
+    ModelBasisArgAttribute mbaa;
+    n.setAttribute(mbaa, val);
+  }
+}
+
+unsigned FirstOrderModel::getModelBasisArg(Node n)
+{
+  computeModelBasisArgAttribute(n);
+  return n.getAttribute(ModelBasisArgAttribute());
+}
+
 FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
 FirstOrderModel(qe, c,name) {
 
@@ -676,14 +790,6 @@ Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
   return st;
 }
 
-bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
-  return n==getModelBasisTerm(n.getType());
-}
-
-Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {
-  return d_qe->getTermDatabase()->getModelBasisTerm(tn);
-}
-
 Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Trace("fmc-model") << "Get function value for " << op << std::endl;
   TypeNode type = op.getType();
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 8a00c70f6..6305a3807 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -26,6 +26,18 @@ namespace theory {
 
 class QuantifiersEngine;
 
+struct ModelBasisAttributeId
+{
+};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+//                     0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId
+{
+};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
+    ModelBasisArgAttribute;
+
 namespace quantifiers {
 
 class TermDb;
@@ -42,24 +54,16 @@ class FirstOrderModelAbs;
 struct IsStarAttributeId {};
 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 
+// TODO (#1301) : document and refactor this class
 class FirstOrderModel : public TheoryModel
 {
-protected:
-  /** quant engine */
-  QuantifiersEngine * d_qe;
-  /** list of quantifiers asserted in the current context */
-  context::CDList<Node> d_forall_asserts;
-  /** quantified formulas marked as relevant */
-  unsigned d_rlv_count;
-  std::map< Node, unsigned > d_forall_rlv;
-  std::vector< Node > d_forall_rlv_vec;
-  Node d_last_forall_rlv;
-  std::vector< Node > d_forall_rlv_assert;
-  /** get variable id */
-  std::map< Node, std::map< Node, int > > d_quant_var_id;
-  /** get current model value (deprecated) */
-  //virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
-public: //for Theory Quantifiers:
+ public:
+  FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
+  virtual ~FirstOrderModel() throw() {}
+  virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
+  virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
+  virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
+  virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; }
   /** assert quantifier */
   void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
@@ -68,30 +72,14 @@ public: //for Theory Quantifiers:
   Node getAssertedQuantifier( unsigned i, bool ordered = false );
   /** initialize model for term */
   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
-  virtual void processInitializeModelForTerm( Node n ) = 0;
-  virtual void processInitializeQuantifier( Node q ) {}
-public:
-  FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
-  virtual ~FirstOrderModel() throw() {}
-  virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
-  virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
-  virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
-  virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
   // initialize the model
   void initialize();
-  virtual void processInitialize( bool ispre ) = 0;
   /** get variable id */
   int getVariableId(TNode q, TNode n) {
     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
   }
-  /** get some domain element */
-  Node getSomeDomainElement(TypeNode tn);
   /** do we need to do any work? */
   bool checkNeeded();
-private:
-  //list of inactive quantified formulas
-  std::map< TNode, bool > d_quant_active;
-public:
   /** reset round */
   void reset_round();
   /** mark quantified formula relevant */
@@ -107,6 +95,54 @@ public:
   bool isQuantifierActive( TNode q );
   /** is quantified formula asserted */
   bool isQuantifierAsserted( TNode q );
+  /** get model basis term */
+  Node getModelBasisTerm(TypeNode tn);
+  /** is model basis term */
+  bool isModelBasisTerm(Node n);
+  /** 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);
+  /** get some domain element */
+  Node getSomeDomainElement(TypeNode tn);
+
+ protected:
+  /** quant engine */
+  QuantifiersEngine* d_qe;
+  /** list of quantifiers asserted in the current context */
+  context::CDList<Node> d_forall_asserts;
+  /** quantified formulas marked as relevant */
+  unsigned d_rlv_count;
+  std::map<Node, unsigned> d_forall_rlv;
+  std::vector<Node> d_forall_rlv_vec;
+  Node d_last_forall_rlv;
+  std::vector<Node> d_forall_rlv_assert;
+  /** get variable id */
+  std::map<Node, std::map<Node, int> > d_quant_var_id;
+  /** process initialize model for term */
+  virtual void processInitializeModelForTerm(Node n) = 0;
+  /** process intialize quantifier */
+  virtual void processInitializeQuantifier(Node q) {}
+  /** process initialize */
+  virtual void processInitialize(bool ispre) = 0;
+
+ private:
+  // list of inactive quantified formulas
+  std::map<TNode, bool> d_quant_active;
+  /** map from types to model basis terms */
+  std::map<TypeNode, Node> d_model_basis_term;
+  /** 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 */
+  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 */
+  void computeModelBasisArgAttribute(Node n);
 };/* class FirstOrderModel */
 
 
@@ -180,8 +216,6 @@ public:
   bool isStar(Node n);
   Node getStar(TypeNode tn);
   Node getStarElement(TypeNode tn);
-  bool isModelBasisTerm(Node n);
-  Node getModelBasisTerm(TypeNode tn);
   bool isInterval(Node n);
   Node getInterval( Node lb, Node ub );
   bool isInRange( Node v, Node i );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index b0f118ad5..5847449cf 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -433,7 +433,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     Trace("fmc-model-debug") << std::endl;
     //possibly get default
     if( needsDefault ){
-      Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+      Node nmb = fm->getModelBasisOpTerm(op);
       //add default value if necessary
       if( fm->hasTerm( nmb ) ){
         Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
@@ -504,8 +504,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     ModelBasisArgSort mbas;
     for (int i=0; i<(int)conds.size(); i++) {
       mbas.d_terms.push_back(conds[i]);
-      mbas.d_mba_count[conds[i]] =
-          d_qe->getTermDatabase()->getModelBasisArg(conds[i]);
+      mbas.d_mba_count[conds[i]] = fm->getModelBasisArg(conds[i]);
       indices.push_back(i);
     }
     std::sort( indices.begin(), indices.end(), mbas );
@@ -556,7 +555,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
 void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
   if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
     d_preinitialized_types[tn] = true;
-    Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    Node mb = fm->getModelBasisTerm(tn);
     if( !mb.isConst() ){
       Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl;
       fm->d_equalityEngine->addTerm( mb );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 0b248056c..dcc863f3e 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -287,7 +287,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     if( options::quantFunWellDefined() ){
       Node hd = QuantAttributes::getFunDefHead( f );
       if( !hd.isNull() ){
-        hd = d_quantEngine->getTermUtil()->getInstConstantNode( hd, f );
+        hd = d_quantEngine->getTermUtil()
+                 ->substituteBoundVariablesToInstConstants(hd, f);
         patTermsF.push_back( hd );
         tinfo[hd].init( f, hd );
       }
@@ -512,7 +513,10 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
   if( tr ){
     if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
       //partial trigger : generate implication to mark user pattern
-      Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermUtil()->getVariableNode( tr->getInstPattern(), q ) );
+      Node pat =
+          d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
+              tr->getInstPattern(), q);
+      Node ipl = NodeManager::currentNM()->mkNode(INST_PATTERN_LIST, pat);
       Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
       Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
       Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 1f3f56820..22af9dd00 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -178,7 +178,9 @@ void InstantiationEngine::registerQuantifier( Node f ){
     //}
     //take into account user patterns
     if( f.getNumChildren()==3 ){
-      Node subsPat = d_quantEngine->getTermUtil()->getInstConstantNode( f[2], f );
+      Node subsPat =
+          d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
+              f[2], f);
       //add patterns
       for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
         //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 57187b7ab..b84499ee4 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -153,7 +153,7 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
 }
 
 bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
-  Node icn = d_qe->getTermUtil()->getInstConstantNode( n, f );
+  Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f);
   Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
   std::vector< Node > var;
   d_qe->getTermUtil()->getVarContainsNode( f, icn, var );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 7c5259cb7..8fd659009 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -141,10 +141,10 @@ void QModelBuilder::debugModel( TheoryModel* m ){
   }
 }
 
-
-
-bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
-  if( argIndex<(int)n.getNumChildren() ){
+bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
+{
+  if (argIndex < n.getNumChildren())
+  {
     Node r;
     if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
       r = n[ argIndex ];
@@ -153,10 +153,10 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
     }
     std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
     if( it==d_data.end() ){
-      d_data[r].addTerm2( fm, n, argIndex+1 );
+      d_data[r].addTerm(fm, n, argIndex + 1);
       return true;
     }else{
-      return it->second.addTerm2( fm, n, argIndex+1 );
+      return it->second.addTerm(fm, n, argIndex + 1);
     }
   }else{
     return false;
@@ -189,7 +189,7 @@ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node q = fm->getAssertedQuantifier( i );
       if( d_qe->getModel()->isQuantifierActive( q ) ){
-        int lems = initializeQuantifier( q, q );
+        int lems = initializeQuantifier(q, q, f);
         d_statistics.d_init_inst_gen_lemmas += lems;
         d_addedLemmas += lems;
         if( d_qe->inConflict() ){
@@ -285,7 +285,8 @@ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
   return TheoryEngineModelBuilder::processBuildModel( m );
 }
 
-int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
+int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
+{
   if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
     //create the basis match if necessary
     if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
@@ -304,8 +305,9 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
       //  }
       //}
       d_quant_basis_match[f] = InstMatch( f );
-      for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
-        Node t = d_qe->getTermDatabase()->getModelBasisTerm( f[0][j].getType() );
+      for (unsigned j = 0; j < f[0].getNumChildren(); j++)
+      {
+        Node t = fm->getModelBasisTerm(f[0][j].getType());
         //calculate the basis match for f
         d_quant_basis_match[f].setValue( j, t );
       }
@@ -540,7 +542,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
     for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
       //the literal n is phase-required for quantifier f
       Node n = it->first;
-      Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
+      Node gn = fm->getModelBasis(f, n);
       Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
       bool value;
       //if the corresponding ground abstraction literal has a SAT value
@@ -727,7 +729,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
   if( !d_uf_model_constructed[op] ){
     //construct the model for the uninterpretted function/predicate
     bool setDefaultVal = true;
-    Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+    Node defaultTerm = fmig->getModelBasisOpTerm(op);
     Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
     //set the values in the model
     std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
@@ -770,7 +772,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
       if( defaultVal.isNull() ){
         if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
         {
-          Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
+          Node mbt = fmig->getModelBasisTerm(defaultTerm.getType());
           fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
               mbt);
         }
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 2dc561074..73e2937ab 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -60,13 +60,11 @@ public:
 
 
 class TermArgBasisTrie {
-private:
-  bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
 public:
   /** the data */
   std::map< Node, TermArgBasisTrie > d_data;
-public:
-  bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
+  /** add term to the trie */
+  bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0);
 };/* class TermArgBasisTrie */
 
 /** model builder class
@@ -93,7 +91,7 @@ protected:
   //reset
   virtual void reset( FirstOrderModel* fm ) = 0;
   //initialize quantifiers, return number of lemmas produced
-  virtual int initializeQuantifier( Node f, Node fp );
+  virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm);
   //analyze model
   virtual void analyzeModel( FirstOrderModel* fm );
   //analyze quantifiers
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index b3acb408f..88b16bfd3 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -187,7 +187,7 @@ int ModelEngine::checkModel(){
         Trace("model-engine-debug") << r << " ";
       }
       Trace("model-engine-debug") << std::endl;
-      Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+      Node mbt = fm->getModelBasisTerm(it->first);
       Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
     }
   }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 0094bc147..bd56b9d9b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -609,7 +609,8 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
     //check constraints
     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
       //apply substitution to the tconstraint
-      Node cons = p->getTermUtil()->getInstantiatedNode( it->first, d_q, terms );
+      Node cons =
+          p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms);
       cons = it->second ? cons : cons.negate();
       if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
         return true;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 9f6617d5a..0ffed5243 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
@@ -1793,7 +1794,8 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
       Node sub;
       std::vector< unsigned > sub_vars;
       //return skolemized body
-      return TermUtil::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
+      return Skolemize::mkSkolemizedBody(
+          n, nn, fvTypes, fvs, sk, sub, sub_vars);
     }
   }else{
     //check if it contains a quantifier as a subterm
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index d852667de..b28dca1ed 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -293,7 +293,9 @@ bool RewriteEngine::checkCompleteFor( Node q ) {
 Node RewriteEngine::getInstConstNode( Node n, Node q ) {
   std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
   if( it==d_inst_const_node[q].end() ){
-    Node nn = d_quantEngine->getTermUtil()->getInstConstantNode( n, q );
+    Node nn =
+        d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
+            n, q);
     d_inst_const_node[q][n] = nn;
     return nn;
   }else{
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
new file mode 100644
index 000000000..2f210cc20
--- /dev/null
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -0,0 +1,385 @@
+/*********************                                                        */
+/*! \file skolemize.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 skolemization utility
+ **/
+
+#include "theory/quantifiers/skolemize.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/sort_inference.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u)
+    : d_quantEngine(qe), d_skolemized(u)
+{
+}
+
+Node Skolemize::process(Node q)
+{
+  // do skolemization
+  if (d_skolemized.find(q) == d_skolemized.end())
+  {
+    Node body = getSkolemizedBody(q);
+    NodeBuilder<> nb(kind::OR);
+    nb << q << body.notNode();
+    Node lem = nb;
+    d_skolemized[q] = lem;
+    return lem;
+  }
+  return Node::null();
+}
+
+bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
+{
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+      d_skolem_constants.find(q);
+  if (it != d_skolem_constants.end())
+  {
+    skolems.insert(skolems.end(), it->second.begin(), it->second.end());
+    return true;
+  }
+  return false;
+}
+
+Node Skolemize::getSkolemConstant(Node q, unsigned i)
+{
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+      d_skolem_constants.find(q);
+  if (it != d_skolem_constants.end())
+  {
+    if (i < it->second.size())
+    {
+      return it->second[i];
+    }
+  }
+  return Node::null();
+}
+
+void Skolemize::getSelfSel(const Datatype& dt,
+                           const DatatypeConstructor& dc,
+                           Node n,
+                           TypeNode ntn,
+                           std::vector<Node>& selfSel)
+{
+  TypeNode tspec;
+  if (dt.isParametric())
+  {
+    tspec = TypeNode::fromType(
+        dc.getSpecializedConstructorType(n.getType().toType()));
+    Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
+                          << std::endl;
+    Assert(tspec.getNumChildren() == dc.getNumArgs());
+  }
+  Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
+                        << dt.getName() << std::endl;
+  for (unsigned j = 0; j < dc.getNumArgs(); j++)
+  {
+    std::vector<Node> ssc;
+    if (dt.isParametric())
+    {
+      Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
+                            << std::endl;
+      if (tspec[j] == ntn)
+      {
+        ssc.push_back(n);
+      }
+    }
+    else
+    {
+      TypeNode tn = TypeNode::fromType(dc[j].getRangeType());
+      Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
+      if (tn == ntn)
+      {
+        ssc.push_back(n);
+      }
+    }
+    /* TODO: more than weak structural induction
+    else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
+    )==visited.end() ){
+      visited.push_back( tn );
+      const Datatype& dt =
+    ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
+      std::vector< Node > disj;
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        getSelfSel( dt[i], n, ntn, ssc );
+      }
+      visited.pop_back();
+    }
+    */
+    for (unsigned k = 0; k < ssc.size(); k++)
+    {
+      Node ss = NodeManager::currentNM()->mkNode(
+          APPLY_SELECTOR_TOTAL,
+          dc.getSelectorInternal(n.getType().toType(), j),
+          n);
+      if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
+      {
+        selfSel.push_back(ss);
+      }
+    }
+  }
+}
+
+Node Skolemize::mkSkolemizedBody(Node f,
+                                 Node n,
+                                 std::vector<TypeNode>& argTypes,
+                                 std::vector<TNode>& fvs,
+                                 std::vector<Node>& sk,
+                                 Node& sub,
+                                 std::vector<unsigned>& sub_vars)
+{
+  Assert(sk.empty() || sk.size() == f[0].getNumChildren());
+  // calculate the variables and substitution
+  std::vector<TNode> ind_vars;
+  std::vector<unsigned> ind_var_indicies;
+  std::vector<TNode> vars;
+  std::vector<unsigned> var_indicies;
+  for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+  {
+    if (isInductionTerm(f[0][i]))
+    {
+      ind_vars.push_back(f[0][i]);
+      ind_var_indicies.push_back(i);
+    }
+    else
+    {
+      vars.push_back(f[0][i]);
+      var_indicies.push_back(i);
+    }
+    Node s;
+    // make the new function symbol or use existing
+    if (i >= sk.size())
+    {
+      if (argTypes.empty())
+      {
+        s = NodeManager::currentNM()->mkSkolem(
+            "skv", f[0][i].getType(), "created during skolemization");
+      }
+      else
+      {
+        TypeNode typ = NodeManager::currentNM()->mkFunctionType(
+            argTypes, f[0][i].getType());
+        Node op = NodeManager::currentNM()->mkSkolem(
+            "skop", typ, "op created during pre-skolemization");
+        // DOTHIS: set attribute on op, marking that it should not be selected
+        // as trigger
+        std::vector<Node> funcArgs;
+        funcArgs.push_back(op);
+        funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
+        s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
+      }
+      sk.push_back(s);
+    }
+    else
+    {
+      Assert(sk[i].getType() == f[0][i].getType());
+    }
+  }
+  Node ret;
+  if (vars.empty())
+  {
+    ret = n;
+  }
+  else
+  {
+    std::vector<Node> var_sk;
+    for (unsigned i = 0; i < var_indicies.size(); i++)
+    {
+      var_sk.push_back(sk[var_indicies[i]]);
+    }
+    Assert(vars.size() == var_sk.size());
+    ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
+  }
+  if (!ind_vars.empty())
+  {
+    Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
+    Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
+    Node n_str_ind;
+    TypeNode tn = ind_vars[0].getType();
+    Node k = sk[ind_var_indicies[0]];
+    Node nret = ret.substitute(ind_vars[0], k);
+    // note : everything is under a negation
+    // the following constructs ~( R( x, k ) => ~P( x ) )
+    if (options::dtStcInduction() && tn.isDatatype())
+    {
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      std::vector<Node> disj;
+      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+      {
+        std::vector<Node> selfSel;
+        getSelfSel(dt, dt[i], k, tn, selfSel);
+        std::vector<Node> conj;
+        conj.push_back(
+            NodeManager::currentNM()
+                ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k)
+                .negate());
+        for (unsigned j = 0; j < selfSel.size(); j++)
+        {
+          conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
+        }
+        disj.push_back(conj.size() == 1
+                           ? conj[0]
+                           : NodeManager::currentNM()->mkNode(OR, conj));
+      }
+      Assert(!disj.empty());
+      n_str_ind = disj.size() == 1
+                      ? disj[0]
+                      : NodeManager::currentNM()->mkNode(AND, disj);
+    }
+    else if (options::intWfInduction() && tn.isInteger())
+    {
+      Node icond = NodeManager::currentNM()->mkNode(
+          GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
+      Node iret =
+          ret.substitute(
+                 ind_vars[0],
+                 NodeManager::currentNM()->mkNode(
+                     MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
+              .negate();
+      n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
+      n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
+    }
+    else
+    {
+      Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
+                      << ", type = " << tn << std::endl;
+      Assert(false);
+    }
+    Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
+
+    std::vector<Node> rem_ind_vars;
+    rem_ind_vars.insert(
+        rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
+    if (!rem_ind_vars.empty())
+    {
+      Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
+      nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
+      nret = Rewriter::rewrite(nret);
+      sub = nret;
+      sub_vars.insert(
+          sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
+      n_str_ind = NodeManager::currentNM()
+                      ->mkNode(FORALL, bvl, n_str_ind.negate())
+                      .negate();
+    }
+    ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
+  }
+  Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
+                                << " returns : " << ret << std::endl;
+  // if it has an instantiation level, set the skolemized body to that level
+  if (f.hasAttribute(InstLevelAttribute()))
+  {
+    theory::QuantifiersEngine::setInstantiationLevelAttr(
+        ret, f.getAttribute(InstLevelAttribute()));
+  }
+
+  if (Trace.isOn("quantifiers-sk"))
+  {
+    Trace("quantifiers-sk") << "Skolemize : ";
+    for (unsigned i = 0; i < sk.size(); i++)
+    {
+      Trace("quantifiers-sk") << sk[i] << " ";
+    }
+    Trace("quantifiers-sk") << "for " << std::endl;
+    Trace("quantifiers-sk") << "   " << f << std::endl;
+  }
+
+  return ret;
+}
+
+Node Skolemize::getSkolemizedBody(Node f)
+{
+  Assert(f.getKind() == FORALL);
+  if (d_skolem_body.find(f) == d_skolem_body.end())
+  {
+    std::vector<TypeNode> fvTypes;
+    std::vector<TNode> fvs;
+    Node sub;
+    std::vector<unsigned> sub_vars;
+    d_skolem_body[f] = mkSkolemizedBody(
+        f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars);
+    // store sub quantifier information
+    if (!sub.isNull())
+    {
+      // if we are skolemizing one at a time, we already know the skolem
+      // constants of the sub-quantified formula, store them
+      Assert(d_skolem_constants[sub].empty());
+      for (unsigned i = 0; i < sub_vars.size(); i++)
+      {
+        d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
+      }
+    }
+    Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
+    if (options::sortInference())
+    {
+      for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
+      {
+        // carry information for sort inference
+        d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar(
+            f, f[0][i], d_skolem_constants[f][i]);
+      }
+    }
+  }
+  return d_skolem_body[f];
+}
+
+bool Skolemize::isInductionTerm(Node n)
+{
+  TypeNode tn = n.getType();
+  if (options::dtStcInduction() && tn.isDatatype())
+  {
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    return !dt.isCodatatype();
+  }
+  if (options::intWfInduction() && n.getType().isInteger())
+  {
+    return true;
+  }
+  return false;
+}
+
+bool Skolemize::printSkolemization(std::ostream& out)
+{
+  bool printed = false;
+  for (NodeNodeMap::iterator it = d_skolemized.begin();
+       it != d_skolemized.end();
+       ++it)
+  {
+    Node q = (*it).first;
+    printed = true;
+    out << "(skolem " << q << std::endl;
+    out << "  ( ";
+    for (unsigned i = 0; i < d_skolem_constants[q].size(); i++)
+    {
+      if (i > 0)
+      {
+        out << " ";
+      }
+      out << d_skolem_constants[q][i];
+    }
+    out << " )" << std::endl;
+    out << ")" << std::endl;
+  }
+  return printed;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
new file mode 100644
index 000000000..c3fb1da29
--- /dev/null
+++ b/src/theory/quantifiers/skolemize.h
@@ -0,0 +1,146 @@
+/*********************                                                        */
+/*! \file skolemize.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 utilities for skolemization
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#define __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "context/cdhashmap.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers/quant_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Skolemization utility
+ *
+ * This class constructs Skolemization lemmas.
+ * Given a quantified formula q = (forall x. P),
+ * its skolemization lemma is of the form:
+ *   (~ forall x. P ) => ~P * { x -> d_skolem_constants[q] }
+ *
+ * This class also incorporates techniques for
+ * skolemization with "inductive strenghtening", see
+ * Section 2 of Reynolds et al., "Induction for SMT
+ * Solvers", VMCAI 2015. In the case that x is an inductive
+ * datatype or an integer, then we may strengthen the conclusion
+ * based on weak well-founded induction. For example, for
+ * quantification on lists, a skolemization with inductive
+ * strengthening is a lemma of this form:
+ *   (~ forall x : List. P( x ) ) =>
+ *   ~P( k ) ^ ( is-cons( k ) => P( tail( k ) ) )
+ * For the integers it is:
+ *   (~ forall x : Int. P( x ) ) =>
+ *   ~P( k ) ^ ( x>0 => P( x-1 ) )
+ *
+ *
+ * Inductive strenghtening is not enabled by
+ * default and can be enabled by option:
+ *   --quant-ind
+ */
+class Skolemize
+{
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+
+ public:
+  Skolemize(QuantifiersEngine* qe, context::UserContext* u);
+  ~Skolemize() {}
+  /** skolemize quantified formula q
+   * If the return value ret of this function
+   * is non-null, then ret is a new skolemization lemma
+   * we generated for q. These lemmas are constructed
+   * once per user-context.
+   */
+  Node process(Node q);
+  /** get skolem constants for quantified formula q */
+  bool getSkolemConstants(Node q, std::vector<Node>& skolems);
+  /** get the i^th skolem constant for quantified formula q */
+  Node getSkolemConstant(Node q, unsigned i);
+  /** make skolemized body
+   *
+   * This returns the skolemized body n of a
+   * quantified formula q with inductive strenghtening,
+   * where typically n is q[1].
+   *
+   * The skolem constants/functions we generate by this
+   * skolemization are added to sk.
+   *
+   * The arguments fvTypes and fvs are used if we are
+   * performing skolemization within a nested quantified
+   * formula. In this case, skolem constants we introduce
+   * must be parameterized based on fvTypes and must be
+   * applied to fvs.
+   *
+   * The last two arguments sub and sub_vars are used for
+   * to carry the body and indices of other induction
+   * variables if a quantified formula to skolemize
+   * has multiple induction variables. See page 5
+   * of Reynolds et al., VMCAI 2015.
+   */
+  static Node mkSkolemizedBody(Node q,
+                               Node n,
+                               std::vector<TypeNode>& fvTypes,
+                               std::vector<TNode>& fvs,
+                               std::vector<Node>& sk,
+                               Node& sub,
+                               std::vector<unsigned>& sub_vars);
+  /** get the skolemized body for quantified formula q */
+  Node getSkolemizedBody(Node q);
+  /** is n a variable that we can apply inductive strenghtening to? */
+  static bool isInductionTerm(Node n);
+  /** print all skolemizations
+   * This is used for the command line option
+   *   --dump-instantiations
+   * which prints an informal justification
+   * of steps taken by the quantifiers module.
+   * Returns true if we printed at least one
+   * skolemization.
+   */
+  bool printSkolemization(std::ostream& out);
+
+ private:
+  /** get self selectors
+   * For datatype constructor dtc with type dt,
+   * this collects the set of datatype selector applications,
+   * applied to term n, whose return type in ntn, and stores
+   * them in the vector selfSel.
+   */
+  static void getSelfSel(const Datatype& dt,
+                         const DatatypeConstructor& dc,
+                         Node n,
+                         TypeNode ntn,
+                         std::vector<Node>& selfSel);
+  /** quantifiers engine that owns this module */
+  QuantifiersEngine* d_quantEngine;
+  /** quantified formulas that have been skolemized */
+  NodeNodeMap d_skolemized;
+  /** map from quantified formulas to the list of skolem constants */
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
+      d_skolem_constants;
+  /** map from quantified formulas to their skolemized body */
+  std::unordered_map<Node, Node, NodeHashFunction> d_skolem_body;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 59405a5d5..a3225e404 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -112,8 +112,9 @@ Node TermDb::getOperator(unsigned i)
 }
 
 /** ground terms */
-unsigned TermDb::getNumGroundTerms( Node f ) {
-  std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
+unsigned TermDb::getNumGroundTerms(Node f) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
   if( it!=d_op_map.end() ){
     return it->second.size();
   }else{
@@ -121,13 +122,25 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
   }
 }
 
-Node TermDb::getGroundTerm( Node f, unsigned i ) {
-  Assert( i<d_op_map[f].size() );
-  return d_op_map[f][i];
+Node TermDb::getGroundTerm(Node f, unsigned i) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it = d_op_map.find(f);
+  if (it != d_op_map.end())
+  {
+    Assert(i < it->second.size());
+    return it->second[i];
+  }
+  else
+  {
+    Assert(false);
+    return Node::null();
+  }
 }
 
-unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) {
-  std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn );
+unsigned TermDb::getNumTypeGroundTerms(TypeNode tn) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_map.find(tn);
   if( it!=d_type_map.end() ){
     return it->second.size();
   }else{
@@ -135,9 +148,61 @@ unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) {
   }
 }
 
-Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
-  Assert( i<d_type_map[tn].size() );
-  return d_type_map[tn][i];
+Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_map.find(tn);
+  if (it != d_type_map.end())
+  {
+    Assert(i < it->second.size());
+    return it->second[i];
+  }
+  else
+  {
+    Assert(false);
+    return Node::null();
+  }
+}
+
+Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn)
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_map.find(tn);
+  if (it != d_type_map.end())
+  {
+    Assert(!it->second.empty());
+    return it->second[0];
+  }
+  else
+  {
+    return getOrMakeTypeFreshVariable(tn);
+  }
+}
+
+Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
+{
+  std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
+      d_type_fv.find(tn);
+  if (it == d_type_fv.end())
+  {
+    std::stringstream ss;
+    ss << language::SetLanguage(options::outputLanguage());
+    ss << "e_" << tn;
+    Node k = NodeManager::currentNM()->mkSkolem(
+        ss.str(), tn, "is a termDb fresh variable");
+    Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
+                   << std::endl;
+    if (options::instMaxLevel() != -1)
+    {
+      QuantifiersEngine::setInstantiationLevelAttr(k, 0);
+    }
+    d_type_fv[tn] = k;
+    return k;
+  }
+  else
+  {
+    return it->second;
+  }
 }
 
 Node TermDb::getMatchOperator( Node n ) {
@@ -179,10 +244,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
         //if this is an atomic trigger, consider adding it
         if( inst::Trigger::isAtomicTrigger( n ) ){
           Trace("term-db") << "register term in db " << n << std::endl;
-          if( options::finiteModelFind() ){
-            computeModelBasisArgAttribute( n );
-          }
-          
+
           Node op = getMatchOperator( n );
           Trace("term-db-debug") << "  match operator is : " << op << std::endl;
           d_ops.push_back(op);
@@ -893,98 +955,6 @@ TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
   return d_func_map_trie[f].existsTerm( args );
 }
 
-
-Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
-  if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
-    Node mbt;
-    if( tn.isInteger() || tn.isReal() ){
-      mbt = NodeManager::currentNM()->mkConst(Rational(0));
-    }else if( d_quantEngine->getTermUtil()->isClosedEnumerableType( tn ) ){
-      mbt = tn.mkGroundTerm();
-    }else{
-      if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
-        std::stringstream ss;
-        ss << language::SetLanguage(options::outputLanguage());
-        ss << "e_" << tn;
-        mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
-        Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
-        if( options::instMaxLevel()!=-1 ){
-          QuantifiersEngine::setInstantiationLevelAttr( mbt, 0 );
-        }
-      }else{
-        mbt = d_type_map[ tn ][ 0 ];
-      }
-    }
-    ModelBasisAttribute mba;
-    mbt.setAttribute(mba,true);
-    d_model_basis_term[tn] = mbt;
-    Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl;
-  }
-  return d_model_basis_term[tn];
-}
-
-Node TermDb::getModelBasisOpTerm( Node op ){
-  if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){
-    TypeNode t = op.getType();
-    std::vector< Node > children;
-    children.push_back( op );
-    for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
-      children.push_back( getModelBasisTerm( t[i] ) );
-    }
-    if( children.size()==1 ){
-      d_model_basis_op_term[op] = op;
-    }else{
-      d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-    }
-  }
-  return d_model_basis_op_term[op];
-}
-
-Node TermDb::getModelBasis( Node q, Node n ){
-  //make model basis
-  if( d_model_basis_terms.find( q )==d_model_basis_terms.end() ){
-    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
-      d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) );
-    }
-  }
-  Node gn = n.substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), 
-                          d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
-                          d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() );
-  return gn;
-}
-
-Node TermDb::getModelBasisBody( Node q ){
-  if( d_model_basis_body.find( q )==d_model_basis_body.end() ){
-    Node n = d_quantEngine->getTermUtil()->getInstConstantBody( q );
-    d_model_basis_body[q] = getModelBasis( q, n );
-  }
-  return d_model_basis_body[q];
-}
-
-void TermDb::computeModelBasisArgAttribute( Node n ){
-  if( !n.hasAttribute(ModelBasisArgAttribute()) ){
-    //ensure that the model basis terms have been defined
-    if( n.getKind()==APPLY_UF ){
-      getModelBasisOpTerm( n.getOperator() );
-    }
-    uint64_t val = 0;
-    //determine if it has model basis attribute
-    for( unsigned j=0; j<n.getNumChildren(); j++ ){
-      if( n[j].getAttribute(ModelBasisAttribute()) ){
-        val++;
-      }
-    }
-    ModelBasisArgAttribute mbaa;
-    n.setAttribute( mbaa, val );
-  }
-}
-
-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 c5165ec2c..de766cc2a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -110,13 +110,23 @@ 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.
-*/
+ *
+ * This class is a key utility used by
+ * a number of approaches for quantifier instantiation,
+ * including E-matching, conflict-based instantiation,
+ * and model-based instantiation.
+ *
+ * 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.
+ *
+ * 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
+ * lazily for performance reasons.
+ */
 class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::QuantifiersEngine;
   // TODO: eliminate these
@@ -144,19 +154,30 @@ class TermDb : public QuantifiersUtil {
   * Get the number of ground terms with operator f that have been added to the
   * database
   */
-  unsigned getNumGroundTerms(Node f);
+  unsigned getNumGroundTerms(Node f) const;
   /** 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);
+  Node getGroundTerm(Node f, unsigned i) const;
   /** get num type terms
   * Get the number of ground terms of tn that have been added to the database
   */
-  unsigned getNumTypeGroundTerms(TypeNode tn);
+  unsigned getNumTypeGroundTerms(TypeNode tn) const;
   /** get type ground term
   * Returns the i^th ground term of type tn
   */
-  Node getTypeGroundTerm(TypeNode tn, unsigned i);
+  Node getTypeGroundTerm(TypeNode tn, unsigned i) const;
+  /** get or make ground term
+  * Returns the first ground term of type tn,
+  * or makes one if none exist.
+  */
+  Node getOrMakeTypeGroundTerm(TypeNode tn);
+  /** make fresh variable
+  * Returns a fresh variable of type tn.
+  * This will return only a single fresh
+  * variable per type.
+  */
+  Node getOrMakeTypeFreshVariable(TypeNode tn);
   /** 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
@@ -197,21 +218,22 @@ class TermDb : public QuantifiersUtil {
   /** 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 )
+  * (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, 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
+  * (2) t is of the form f( t1, ..., tk ) where ti is in the
+  *     equivalence class of args[i] 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.
+  * (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
@@ -296,9 +318,13 @@ class TermDb : public QuantifiersUtil {
   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 */
+  /** get eligible term in equivalence class of r */
   Node getEligibleTermInEqc(TNode r);
-  /** is inst closure */
+  /** is r a inst closure node?
+   * This terminology was used for specifying
+   * a particular status of nodes for
+   * Bansal et al., CAV 2015.
+   */
   bool isInstClosure(Node r);
 
  private:
@@ -321,6 +347,8 @@ class TermDb : public QuantifiersUtil {
   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;
+  /** map from type nodes to a fresh variable we introduced */
+  std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv;
   /** inactive map */
   NodeBoolMap d_inactive_map;
   /** count of the number of non-redundant ground terms per operator */
@@ -364,32 +392,6 @@ class TermDb : public QuantifiersUtil {
   /** get operator representative */
   Node getOperatorRepresentative( TNode op ) const;
   //------------------------------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 */
-  std::map< Node, Node > d_model_basis_op_term;
-  /** 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 */
-  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);
-  /** get model basis arg */
-  unsigned getModelBasisArg(Node n);
-
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
new file mode 100644
index 000000000..67ee88c07
--- /dev/null
+++ b/src/theory/quantifiers/term_enumeration.cpp
@@ -0,0 +1,133 @@
+/*********************                                                        */
+/*! \file term_enumeration.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 term enumeration utility
+ **/
+
+#include "theory/quantifiers/term_enumeration.h"
+
+#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
+{
+  Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
+                        << std::endl;
+  std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it =
+      d_typ_enum_map.find(tn);
+  size_t teIndex;
+  if (it == d_typ_enum_map.end())
+  {
+    teIndex = d_typ_enum.size();
+    d_typ_enum_map[tn] = teIndex;
+    d_typ_enum.push_back(TypeEnumerator(tn));
+  }
+  else
+  {
+    teIndex = it->second;
+  }
+  while (index >= d_enum_terms[tn].size())
+  {
+    if (d_typ_enum[teIndex].isFinished())
+    {
+      return Node::null();
+    }
+    d_enum_terms[tn].push_back(*d_typ_enum[teIndex]);
+    ++d_typ_enum[teIndex];
+  }
+  return d_enum_terms[tn][index];
+}
+
+bool TermEnumeration::isClosedEnumerableType(TypeNode tn)
+{
+  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
+      d_typ_closed_enum.find(tn);
+  if (it == d_typ_closed_enum.end())
+  {
+    d_typ_closed_enum[tn] = true;
+    bool ret = true;
+    if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
+    {
+      ret = false;
+    }
+    else if (tn.isSet())
+    {
+      ret = isClosedEnumerableType(tn.getSetElementType());
+    }
+    else if (tn.isDatatype())
+    {
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+      {
+        for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
+        {
+          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+          if (tn != ctn && !isClosedEnumerableType(ctn))
+          {
+            ret = false;
+            break;
+          }
+        }
+        if (!ret)
+        {
+          break;
+        }
+      }
+    }
+    
+    // other parametric sorts go here
+    
+    d_typ_closed_enum[tn] = ret;
+    return ret;
+  }
+  else
+  {
+    return it->second;
+  }
+}
+
+// checks whether a type is closed enumerable and is reasonably small enough (<1000)
+// such that all of its domain elements can be enumerated
+bool TermEnumeration::mayComplete(TypeNode tn)
+{
+  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
+      d_may_complete.find(tn);
+  if (it == d_may_complete.end())
+  {
+    bool mc = false;
+    if (isClosedEnumerableType(tn) && tn.getCardinality().isFinite()
+        && !tn.getCardinality().isLargeFinite())
+    {
+      Node card = NodeManager::currentNM()->mkConst(
+          Rational(tn.getCardinality().getFiniteCardinality()));
+      Node oth = NodeManager::currentNM()->mkConst(Rational(1000));
+      Node eq = NodeManager::currentNM()->mkNode(LEQ, card, oth);
+      eq = Rewriter::rewrite(eq);
+      mc = eq.isConst() && eq.getConst<bool>();
+    }
+    d_may_complete[tn] = mc;
+    return mc;
+  }
+  else
+  {
+    return it->second;
+  }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h
new file mode 100644
index 000000000..a96718800
--- /dev/null
+++ b/src/theory/quantifiers/term_enumeration.h
@@ -0,0 +1,83 @@
+/*********************                                                        */
+/*! \file term_enumeration.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 utilities for term enumeration
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#define __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Term enumeration
+ *
+ * This class has utilities for enumerating terms. It stores
+ * a cache of terms enumerated per each type.
+ * It also has various utility functions regarding type
+ * enumeration.
+ */
+class TermEnumeration
+{
+ public:
+  TermEnumeration() {}
+  ~TermEnumeration() {}
+  /** get i^th term for type tn */
+  Node getEnumerateTerm(TypeNode tn, unsigned i);
+  /** is closed enumerable type
+   *
+   * This returns true if this type has an enumerator that produces
+   * constants that are handled by ground theory solvers.
+   * Examples of types that are not closed enumerable are:
+   * (1) uninterpreted sorts,
+   * (2) arrays,
+   * (3) codatatypes,
+   * (4) parametric sorts involving any of the above.
+   */
+  bool isClosedEnumerableType(TypeNode tn);
+  /** may complete type
+   *
+   * Returns true if the type tn is closed 
+   * enumerable, and is small enough
+   * for finite model finding to enumerate it,
+   * by some heuristic (current cardinality < 1000).
+   */
+  bool mayComplete(TypeNode tn);
+
+ private:
+  /** ground terms enumerated for types */
+  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
+      d_enum_terms;
+  /** map from type to the index of its type enumerator in d_typ_enum. */
+  std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
+  /** type enumerators */
+  std::vector<TypeEnumerator> d_typ_enum;
+  /** closed enumerable type cache */
+  std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_typ_closed_enum;
+  /** may complete */
+  std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 346745b1d..471670515 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -16,12 +16,13 @@
 
 #include "expr/datatype.h"
 #include "options/base_options.h"
-#include "options/quantifiers_options.h"
 #include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
 #include "options/uf_options.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -197,7 +198,7 @@ unsigned TermUtil::getNumInstantiationConstants( Node q ) const {
 Node TermUtil::getInstConstantBody( Node q ){
   std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
   if( it==d_inst_const_body.end() ){
-    Node n = getInstConstantNode( q[1], q );
+    Node n = substituteBoundVariablesToInstConstants(q[1], q);
     d_inst_const_body[ q ] = n;
     return n;
   }else{
@@ -225,273 +226,35 @@ Node TermUtil::getCounterexampleLiteral( Node q ){
   return d_ce_lit[ q ];
 }
 
-Node TermUtil::getInstConstantNode( Node n, Node q ){
+Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q)
+{
   registerQuantifier( q );
   return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
 }
 
-Node TermUtil::getVariableNode( Node n, Node q ) {
+Node TermUtil::substituteInstConstantsToBoundVariables(Node n, Node q)
+{
   registerQuantifier( q );
   return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
 }
 
-Node TermUtil::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
+Node TermUtil::substituteBoundVariables(Node n,
+                                        Node q,
+                                        std::vector<Node>& terms)
+{
+  registerQuantifier(q);
   Assert( d_vars[q].size()==terms.size() );
   return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
 }
 
-
-void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
-  TypeNode tspec;
-  if( dt.isParametric() ){
-    tspec = TypeNode::fromType( dc.getSpecializedConstructorType(n.getType().toType()) );
-    Trace("sk-ind-debug") << "Specialized constructor type : " << tspec << std::endl;
-    Assert( tspec.getNumChildren()==dc.getNumArgs() );
-  }
-  Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " << dt.getName() << std::endl;
-  for( unsigned j=0; j<dc.getNumArgs(); j++ ){
-    std::vector< Node > ssc;
-    if( dt.isParametric() ){
-      Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn << std::endl;
-      if( tspec[j]==ntn ){
-        ssc.push_back( n );
-      }
-    }else{
-      TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
-      Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
-      if( tn==ntn ){
-        ssc.push_back( n );
-      }
-    }
-    /* TODO: more than weak structural induction
-    else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
-      visited.push_back( tn );
-      const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
-      std::vector< Node > disj;
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        getSelfSel( dt[i], n, ntn, ssc );
-      }
-      visited.pop_back();
-    }
-    */
-    for( unsigned k=0; k<ssc.size(); k++ ){
-      Node ss = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dc.getSelectorInternal( n.getType().toType(), j ), n );
-      if( std::find( selfSel.begin(), selfSel.end(), ss )==selfSel.end() ){
-        selfSel.push_back( ss );
-      }
-    }
-  }
-}
-
-
-Node TermUtil::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
-                               std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars ) {
-  Assert( sk.empty() || sk.size()==f[0].getNumChildren() );
-  //calculate the variables and substitution
-  std::vector< TNode > ind_vars;
-  std::vector< unsigned > ind_var_indicies;
-  std::vector< TNode > vars;
-  std::vector< unsigned > var_indicies;
-  for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-    if( isInductionTerm( f[0][i] ) ){
-      ind_vars.push_back( f[0][i] );
-      ind_var_indicies.push_back( i );
-    }else{
-      vars.push_back( f[0][i] );
-      var_indicies.push_back( i );
-    }
-    Node s;
-    //make the new function symbol or use existing
-    if( i>=sk.size() ){
-      if( argTypes.empty() ){
-        s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
-      }else{
-        TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
-        Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
-        //DOTHIS: set attribute on op, marking that it should not be selected as trigger
-        std::vector< Node > funcArgs;
-        funcArgs.push_back( op );
-        funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
-        s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
-      }
-      sk.push_back( s );
-    }else{
-      Assert( sk[i].getType()==f[0][i].getType() );
-    }
-  }
-  Node ret;
-  if( vars.empty() ){
-    ret = n;
-  }else{
-    std::vector< Node > var_sk;
-    for( unsigned i=0; i<var_indicies.size(); i++ ){
-      var_sk.push_back( sk[var_indicies[i]] );
-    }
-    Assert( vars.size()==var_sk.size() );
-    ret = n.substitute( vars.begin(), vars.end(), var_sk.begin(), var_sk.end() );
-  }
-  if( !ind_vars.empty() ){
-    Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
-    Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
-    Node n_str_ind;
-    TypeNode tn = ind_vars[0].getType();
-    Node k = sk[ind_var_indicies[0]];
-    Node nret = ret.substitute( ind_vars[0], k );
-    //note : everything is under a negation
-    //the following constructs ~( R( x, k ) => ~P( x ) )
-    if( options::dtStcInduction() && tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      std::vector< Node > disj;
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        std::vector< Node > selfSel;
-        getSelfSel( dt, dt[i], k, tn, selfSel );
-        std::vector< Node > conj;
-        conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
-        for( unsigned j=0; j<selfSel.size(); j++ ){
-          conj.push_back( ret.substitute( ind_vars[0], selfSel[j] ).negate() );
-        }
-        disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) );
-      }
-      Assert( !disj.empty() );
-      n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj );
-    }else if( options::intWfInduction() && tn.isInteger() ){
-      Node icond = NodeManager::currentNM()->mkNode( GEQ, k, NodeManager::currentNM()->mkConst( Rational(0) ) );
-      Node iret = ret.substitute( ind_vars[0], NodeManager::currentNM()->mkNode( MINUS, k, NodeManager::currentNM()->mkConst( Rational(1) ) ) ).negate();
-      n_str_ind = NodeManager::currentNM()->mkNode( OR, icond.negate(), iret );
-      n_str_ind = NodeManager::currentNM()->mkNode( AND, icond, n_str_ind );
-    }else{
-      Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] << ", type = " << tn << std::endl;
-      Assert( false );
-    }
-    Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
-
-    std::vector< Node > rem_ind_vars;
-    rem_ind_vars.insert( rem_ind_vars.end(), ind_vars.begin()+1, ind_vars.end() );
-    if( !rem_ind_vars.empty() ){
-      Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, rem_ind_vars );
-      nret = NodeManager::currentNM()->mkNode( FORALL, bvl, nret );
-      nret = Rewriter::rewrite( nret );
-      sub = nret;
-      sub_vars.insert( sub_vars.end(), ind_var_indicies.begin()+1, ind_var_indicies.end() );
-      n_str_ind = NodeManager::currentNM()->mkNode( FORALL, bvl, n_str_ind.negate() ).negate();
-    }
-    ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
-  }
-  Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
-  //if it has an instantiation level, set the skolemized body to that level
-  if( f.hasAttribute(InstLevelAttribute()) ){
-    theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
-  }
-
-  if( Trace.isOn("quantifiers-sk") ){
-    Trace("quantifiers-sk") << "Skolemize : ";
-    for( unsigned i=0; i<sk.size(); i++ ){
-      Trace("quantifiers-sk") << sk[i] << " ";
-    }
-    Trace("quantifiers-sk") << "for " << std::endl;
-    Trace("quantifiers-sk") << "   " << f << std::endl;
-  }
-
-  return ret;
-}
-
-Node TermUtil::getSkolemizedBody( Node f ){
-  Assert( f.getKind()==FORALL );
-  if( d_skolem_body.find( f )==d_skolem_body.end() ){
-    std::vector< TypeNode > fvTypes;
-    std::vector< TNode > fvs;
-    Node sub;
-    std::vector< unsigned > sub_vars;
-    d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars );
-    //store sub quantifier information
-    if( !sub.isNull() ){
-      //if we are skolemizing one at a time, we already know the skolem constants of the sub-quantified formula, store them
-      Assert( d_skolem_constants[sub].empty() );
-      for( unsigned i=0; i<sub_vars.size(); i++ ){
-        d_skolem_constants[sub].push_back( d_skolem_constants[f][sub_vars[i]] );
-      }
-    }
-    Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
-    if( options::sortInference() ){
-      for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
-        //carry information for sort inference
-        d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
-      }
-    }
-  }
-  return d_skolem_body[ f ];
-}
-
-Node TermUtil::getEnumerateTerm( TypeNode tn, unsigned index ) {
-  Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
-  std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
-  unsigned teIndex;
-  if( it==d_typ_enum_map.end() ){
-    teIndex = (int)d_typ_enum.size();
-    d_typ_enum_map[tn] = teIndex;
-    d_typ_enum.push_back( TypeEnumerator(tn) );
-  }else{
-    teIndex = it->second;
-  }
-  while( index>=d_enum_terms[tn].size() ){
-    if( d_typ_enum[teIndex].isFinished() ){
-      return Node::null();
-    }
-    d_enum_terms[tn].push_back( *d_typ_enum[teIndex] );
-    ++d_typ_enum[teIndex];
-  }
-  return d_enum_terms[tn][index];
-}
-
-bool TermUtil::isClosedEnumerableType( TypeNode tn ) {
-  std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn );
-  if( it==d_typ_closed_enum.end() ){
-    d_typ_closed_enum[tn] = true;
-    bool ret = true;
-    if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){
-      ret = false;
-    }else if( tn.isSet() ){
-      ret = isClosedEnumerableType( tn.getSetElementType() );
-    }else if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-          TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
-          if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
-            ret = false;
-            break;
-          }
-        }
-        if( !ret ){
-          break;
-        }
-      }
-    }
-    //TODO: other parametric sorts go here
-    d_typ_closed_enum[tn] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-}
-
-//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
-bool TermUtil::mayComplete( TypeNode tn ) {
-  std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
-  if( it==d_may_complete.end() ){
-    bool mc = false;
-    if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
-      Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
-      Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
-      Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
-      eq = Rewriter::rewrite( eq );
-      mc = eq==d_true;
-    }
-    d_may_complete[tn] = mc;
-    return mc;
-  }else{
-    return it->second;
-  }
+Node TermUtil::substituteInstConstants(Node n, Node q, std::vector<Node>& terms)
+{
+  registerQuantifier(q);
+  Assert(d_inst_constants[q].size() == terms.size());
+  return n.substitute(d_inst_constants[q].begin(),
+                      d_inst_constants[q].end(),
+                      terms.begin(),
+                      terms.end());
 }
 
 void TermUtil::computeVarContains( Node n, std::vector< Node >& varContains ) {
@@ -1154,12 +917,6 @@ bool TermUtil::isBoolConnectiveTerm( TNode n ) {
          ( n.getKind()!=ITE || n.getType().isBoolean() );
 }
 
-void TermUtil::registerTrigger( theory::inst::Trigger* tr, Node op ){
-  if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
-    d_op_triggers[op].push_back( tr );
-  }
-}
-
 Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn );
   if( ithp==d_ho_type_match_pred.end() ){
@@ -1172,17 +929,6 @@ Node TermUtil::getHoTypeMatchPredicate( TypeNode tn ) {
   }
 }
 
-bool TermUtil::isInductionTerm( Node n ) {
-  TypeNode tn = n.getType();
-  if( options::dtStcInduction() && tn.isDatatype() ){
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    return !dt.isCodatatype();
-  }
-  if( options::intWfInduction() && n.getType().isInteger() ){
-    return true;
-  }
-  return false;
-}
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index f5cfd6df8..bcdf8a2ff 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -46,13 +46,6 @@ typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
 struct ContainsUConstAttributeId {};
 typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
 
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-//                    0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
 //for bounded integers
 struct BoundIntLitAttributeId {};
 typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
@@ -69,7 +62,7 @@ typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
 struct LtePartialInstAttributeId {};
 typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
 
-// attribute for "contains instantiation constants from"
+// attribute for sygus proxy variables
 struct SygusProxyAttributeId {};
 typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
 
@@ -114,7 +107,6 @@ class TermUtil : public QuantifiersUtil
 {
   // TODO : remove these
   friend class ::CVC4::theory::QuantifiersEngine;
-  friend class TermDatabase;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -164,10 +156,14 @@ public:
       return a pattern where the variable are replaced by variable for
       instantiation.
    */
-  Node getInstConstantNode( Node n, Node q );
-  Node getVariableNode( Node n, Node q );
-  /** get substituted node */
-  Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
+  Node substituteBoundVariablesToInstConstants(Node n, Node q);
+  /** substitute { instantiation constants of q -> bound variables of q } in n
+   */
+  Node substituteInstConstantsToBoundVariables(Node n, Node q);
+  /** substitute { variables of q -> terms } in n */
+  Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
+  /** substitute { instantiation constants of q -> terms } in n */
+  Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
 
   static Node getInstConstAttr( Node n );
   static bool hasInstConstAttr( Node n );
@@ -187,51 +183,18 @@ public:
   //quantified simplify (treat free variables in n as quantified and run rewriter)
   static Node getQuantSimplify( Node n );
 
-//for skolem
-private:
-  /** map from universal quantifiers to their skolemized body */
-  std::map< Node, Node > d_skolem_body;
-public:
-  /** map from universal quantifiers to the list of skolem constants */
-  std::map< Node, std::vector< Node > > d_skolem_constants;
-  /** make the skolemized body f[e/x] */
-  static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
-                                std::vector< Node >& sk, Node& sub, std::vector< unsigned >& sub_vars );
-  /** get the skolemized body */
-  Node getSkolemizedBody( Node f);
-  /** is induction variable */
-  static bool isInductionTerm( Node n );
-
-//for ground term enumeration
-private:
-  /** ground terms enumerated for types */
-  std::map< TypeNode, std::vector< Node > > d_enum_terms;
-  //type enumerators
-  std::map< TypeNode, unsigned > d_typ_enum_map;
-  std::vector< TypeEnumerator > d_typ_enum;
-  // closed enumerable type cache
-  std::map< TypeNode, bool > d_typ_closed_enum;
-  /** may complete */
-  std::map< TypeNode, bool > d_may_complete;
-public:
-  //get nth term for type
-  Node getEnumerateTerm( TypeNode tn, unsigned index );
-  //does this type have an enumerator that produces constants that are handled by ground theory solvers
-  bool isClosedEnumerableType( TypeNode tn );
-  // may complete
-  bool mayComplete( TypeNode tn );
-
 //for triggers
 private:
   /** helper function for compute var contains */
   static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
-  /** triggers for each operator */
-  std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
   /** helper for is instance of */
   static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
   /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
   static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
-public:
+  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
+  static int isInstanceOf(Node n1, Node n2);
+
+ public:
   /** compute var contains */
   static void computeVarContains( Node n, std::vector< Node >& varContains );
   /** get var contains for each of the patterns in pats */
@@ -240,12 +203,9 @@ public:
   static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
   /** compute quant contains */
   static void computeQuantContains( Node n, std::vector< Node >& quantContains );
-  /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  static int isInstanceOf( Node n1, Node n2 );
+  // TODO (#1216) : this should be in trigger.h
   /** filter all nodes that have instances */
   static void filterInstances( std::vector< Node >& nodes );
-  /** register trigger (for eager quantifier instantiation) */
-  void registerTrigger( inst::Trigger* tr, Node op );
 
 //for term ordering
 private: