(Move only) Move enumerative instantiation strategy to its own file and document (#1290)

* Move, document, and rename enumerative instantiation.

* Clang format.

6 files changed, 432 insertions, 228 deletions

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 105f8f5e2..0b248056c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -15,18 +15,22 @@
 #include "theory/quantifiers/inst_strategy_e_matching.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace theory {
+
+using namespace inst;
+
+namespace quantifiers {
 
 //priority levels :
 //1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
@@ -600,198 +604,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
   }
 }
 */
-FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe ){
-
-}
-
-bool FullSaturation::needsCheck( Theory::Effort e ){
-  if( options::fullSaturateInterleave() ){
-    if( d_quantEngine->getInstWhenNeedsCheck( e ) ){
-      return true;
-    }
-  }
-  if( options::fullSaturateQuant() ){
-    if( e>=Theory::EFFORT_LAST_CALL ){
-      return true;
-    }
-  }
-  return false;
-}
-
-void FullSaturation::reset_round( Theory::Effort e ) {
-
-}
-
-void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
-  bool doCheck = false;
-  bool fullEffort = false;
-  if( options::fullSaturateInterleave() ){
-    //we only add when interleaved with other strategies
-    doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
-  }
-  if( options::fullSaturateQuant() && !doCheck ){
-    doCheck = quant_e==QuantifiersEngine::QEFFORT_LAST_CALL;
-    fullEffort = !d_quantEngine->hasAddedLemma();
-  }
-  if( doCheck ){
-    double clSet = 0;
-    if( Trace.isOn("fs-engine") ){
-      clSet = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl;
-    }
-    int addedLemmas = 0;
-    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
-      if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-        if( process( q, fullEffort ) ){
-          //added lemma
-          addedLemmas++;
-          if( d_quantEngine->inConflict() ){
-            break;
-          }
-        }
-      }
-    }
-    if( Trace.isOn("fs-engine") ){
-      Trace("fs-engine") << "Added lemmas = " << addedLemmas  << std::endl;
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("fs-engine") << "Finished full saturation engine, time = " << (clSet2-clSet) << std::endl;
-    }
-  }
-}
 
-bool FullSaturation::process( Node f, bool fullEffort ){
-  // ignore if constant true (rare case of non-standard quantifier whose body is rewritten to true)
-  if( f[1].isConst() && f[1].getConst<bool>() ){
-    return false;
-  }
-  //first, try from relevant domain
-  RelevantDomain * rd = d_quantEngine->getRelevantDomain();
-  unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
-  unsigned rend = fullEffort ? 1 : rstart;
-  for( unsigned r=rstart; r<=rend; r++ ){
-    if( rd || r>0 ){
-      if( r==0 ){
-        Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
-      }else{
-        Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
-      }
-      Assert( rd!=NULL );
-      Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
-      rd->compute();
-      Trace("inst-alg-debug") << "...finished" << std::endl;
-      unsigned final_max_i = 0;
-      std::vector< unsigned > maxs;
-      std::vector< bool > max_zero;
-      bool has_zero = false;
-      std::map< TypeNode, std::vector< Node > > term_db_list;
-      std::vector< TypeNode > ftypes;
-      // iterate over substitutions for variables
-      for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
-        TypeNode tn = f[0][i].getType();
-        ftypes.push_back( tn );
-        unsigned ts;
-        if( r==0 ){
-          ts = rd->getRDomain( f, i )->d_terms.size();
-        }else{
-          ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( tn );
-          std::map< TypeNode, std::vector< Node > >::iterator ittd = term_db_list.find( tn );
-          if( ittd==term_db_list.end() ){
-            std::map< Node, Node > reps_found;
-            for( unsigned j=0; j<ts; j++ ){
-              Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], j );
-              if( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr( gt ) ){
-                Node r = d_quantEngine->getEqualityQuery()->getRepresentative( gt );
-                if( reps_found.find( r )==reps_found.end() ){
-                  reps_found[r] = gt;
-                  term_db_list[tn].push_back( gt );
-                }
-              } 
-            }
-            ts = term_db_list[tn].size();
-          }else{
-            ts = ittd->second.size();
-          }
-        }
-        // consider a default value if at full effort
-        max_zero.push_back( fullEffort && ts==0 );
-        ts = ( fullEffort && ts==0 ) ? 1 : ts;
-        Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
-        if( ts==0 ){
-          has_zero = true;
-          break;
-        }else{
-          maxs.push_back( ts );
-          if( ts>final_max_i ){
-            final_max_i = ts;
-          }
-        }
-      }
-      if( !has_zero ){
-        Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
-        unsigned max_i = 0;
-        bool success;
-        while( max_i<=final_max_i ){
-          Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
-          std::vector< unsigned > childIndex;
-          int index = 0;
-          do {
-            while( index>=0 && index<(int)f[0].getNumChildren() ){
-              if( index==(int)childIndex.size() ){
-                childIndex.push_back( -1 );
-              }else{
-                Assert( index==(int)(childIndex.size())-1 );
-                unsigned nv = childIndex[index]+1;
-                if( nv<maxs[index] && nv<=max_i ){
-                  childIndex[index] = nv;
-                  index++;
-                }else{
-                  childIndex.pop_back();
-                  index--;
-                }
-              }
-            }
-            success = index>=0;
-            if( success ){
-              Trace("inst-alg-rd") << "Try instantiation { ";
-              for( unsigned j=0; j<childIndex.size(); j++ ){
-                Trace("inst-alg-rd") << childIndex[j] << " ";
-              }
-              Trace("inst-alg-rd") << "}" << std::endl;
-              //try instantiation
-              std::vector< Node > terms;
-              for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-                if( max_zero[i] ){
-                  //no terms available, will report incomplete instantiation
-                  terms.push_back( Node::null() );
-                  Trace("inst-alg-rd") << "  null" << std::endl;
-                }else if( r==0 ){
-                  terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
-                  Trace("inst-alg-rd") << "  " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl;
-                }else{
-                  Assert( childIndex[i]<term_db_list[ftypes[i]].size() );
-                  terms.push_back( term_db_list[ftypes[i]][childIndex[i]] );
-                  Trace("inst-alg-rd") << "  " << term_db_list[ftypes[i]][childIndex[i]] << std::endl;
-                }
-              }
-              if( d_quantEngine->addInstantiation( f, terms ) ){
-                Trace("inst-alg-rd") << "Success!" << std::endl;
-                ++(d_quantEngine->d_statistics.d_instantiations_guess);
-                return true;
-              }else{
-                index--;
-              }
-            }
-          }while( success );
-          max_i++;
-        }
-      }
-    }
-  }
-  //TODO : term enumerator?
-  return false;
-}
-
-void FullSaturation::registerQuantifier( Node q ) {
-
-}
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 5a4f8e499..1a0ec9b44 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -111,23 +111,6 @@ public:
   void addUserNoPattern( Node q, Node pat );
 };/* class InstStrategyAutoGenTriggers */
 
-class FullSaturation : public QuantifiersModule {
-private:
-  /** guessed instantiations */
-  std::map< Node, bool > d_guessed;
-  /** process functions */
-  bool process( Node q, bool fullEffort );
-public:
-  FullSaturation( QuantifiersEngine* qe );
-  ~FullSaturation(){}
-  bool needsCheck( Theory::Effort e );
-  void reset_round( Theory::Effort e );
-  void check( Theory::Effort e, unsigned quant_e );
-  void registerQuantifier( Node q );
-  /** identify */
-  std::string identify() const { return std::string("FullSaturation"); }
-};/* class FullSaturation */
-
 
 }
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
new file mode 100644
index 000000000..8b825d50d
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -0,0 +1,302 @@
+/*********************                                                        */
+/*! \file inst_strategy_enumerative.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 an enumerative instantiation strategy.
+ **/
+
+#include "theory/quantifiers/inst_strategy_enumerative.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace theory {
+
+using namespace inst;
+
+namespace quantifiers {
+
+InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe)
+    : QuantifiersModule(qe)
+{
+}
+
+bool InstStrategyEnum::needsCheck(Theory::Effort e)
+{
+  if (options::fullSaturateInterleave())
+  {
+    if (d_quantEngine->getInstWhenNeedsCheck(e))
+    {
+      return true;
+    }
+  }
+  if (options::fullSaturateQuant())
+  {
+    if (e >= Theory::EFFORT_LAST_CALL)
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+void InstStrategyEnum::reset_round(Theory::Effort e) {}
+void InstStrategyEnum::check(Theory::Effort e, unsigned quant_e)
+{
+  bool doCheck = false;
+  bool fullEffort = false;
+  if (options::fullSaturateInterleave())
+  {
+    // we only add when interleaved with other strategies
+    doCheck = quant_e == QuantifiersEngine::QEFFORT_STANDARD
+              && d_quantEngine->hasAddedLemma();
+  }
+  if (options::fullSaturateQuant() && !doCheck)
+  {
+    doCheck = quant_e == QuantifiersEngine::QEFFORT_LAST_CALL;
+    fullEffort = !d_quantEngine->hasAddedLemma();
+  }
+  if (doCheck)
+  {
+    double clSet = 0;
+    if (Trace.isOn("fs-engine"))
+    {
+      clSet = double(clock()) / double(CLOCKS_PER_SEC);
+      Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
+                         << std::endl;
+    }
+    int addedLemmas = 0;
+    for (unsigned i = 0;
+         i < d_quantEngine->getModel()->getNumAssertedQuantifiers();
+         i++)
+    {
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
+      if (d_quantEngine->hasOwnership(q, this)
+          && d_quantEngine->getModel()->isQuantifierActive(q))
+      {
+        if (process(q, fullEffort))
+        {
+          // added lemma
+          addedLemmas++;
+          if (d_quantEngine->inConflict())
+          {
+            break;
+          }
+        }
+      }
+    }
+    if (Trace.isOn("fs-engine"))
+    {
+      Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl;
+      double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
+      Trace("fs-engine") << "Finished full saturation engine, time = "
+                         << (clSet2 - clSet) << std::endl;
+    }
+  }
+}
+
+bool InstStrategyEnum::process(Node f, bool fullEffort)
+{
+  // ignore if constant true (rare case of non-standard quantifier whose body is
+  // rewritten to true)
+  if (f[1].isConst() && f[1].getConst<bool>())
+  {
+    return false;
+  }
+  // first, try from relevant domain
+  RelevantDomain* rd = d_quantEngine->getRelevantDomain();
+  unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
+  unsigned rend = fullEffort ? 1 : rstart;
+  for (unsigned r = rstart; r <= rend; r++)
+  {
+    if (rd || r > 0)
+    {
+      if (r == 0)
+      {
+        Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..."
+                          << std::endl;
+      }
+      else
+      {
+        Trace("inst-alg") << "-> Ground term instantiate " << f << "..."
+                          << std::endl;
+      }
+      Assert(rd != NULL);
+      Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
+      rd->compute();
+      Trace("inst-alg-debug") << "...finished" << std::endl;
+      unsigned final_max_i = 0;
+      std::vector<unsigned> maxs;
+      std::vector<bool> max_zero;
+      bool has_zero = false;
+      std::map<TypeNode, std::vector<Node> > term_db_list;
+      std::vector<TypeNode> ftypes;
+      // iterate over substitutions for variables
+      for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+      {
+        TypeNode tn = f[0][i].getType();
+        ftypes.push_back(tn);
+        unsigned ts;
+        if (r == 0)
+        {
+          ts = rd->getRDomain(f, i)->d_terms.size();
+        }
+        else
+        {
+          ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms(tn);
+          std::map<TypeNode, std::vector<Node> >::iterator ittd =
+              term_db_list.find(tn);
+          if (ittd == term_db_list.end())
+          {
+            std::map<Node, Node> reps_found;
+            for (unsigned j = 0; j < ts; j++)
+            {
+              Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm(
+                  ftypes[i], j);
+              if (!options::cbqi()
+                  || !quantifiers::TermUtil::hasInstConstAttr(gt))
+              {
+                Node r =
+                    d_quantEngine->getEqualityQuery()->getRepresentative(gt);
+                if (reps_found.find(r) == reps_found.end())
+                {
+                  reps_found[r] = gt;
+                  term_db_list[tn].push_back(gt);
+                }
+              }
+            }
+            ts = term_db_list[tn].size();
+          }
+          else
+          {
+            ts = ittd->second.size();
+          }
+        }
+        // consider a default value if at full effort
+        max_zero.push_back(fullEffort && ts == 0);
+        ts = (fullEffort && ts == 0) ? 1 : ts;
+        Trace("inst-alg-rd") << "Variable " << i << " has " << ts
+                             << " in relevant domain." << std::endl;
+        if (ts == 0)
+        {
+          has_zero = true;
+          break;
+        }
+        else
+        {
+          maxs.push_back(ts);
+          if (ts > final_max_i)
+          {
+            final_max_i = ts;
+          }
+        }
+      }
+      if (!has_zero)
+      {
+        Trace("inst-alg-rd") << "Will do " << final_max_i
+                             << " stages of instantiation." << std::endl;
+        unsigned max_i = 0;
+        bool success;
+        while (max_i <= final_max_i)
+        {
+          Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+          std::vector<unsigned> childIndex;
+          int index = 0;
+          do
+          {
+            while (index >= 0 && index < (int)f[0].getNumChildren())
+            {
+              if (index == (int)childIndex.size())
+              {
+                childIndex.push_back(-1);
+              }
+              else
+              {
+                Assert(index == (int)(childIndex.size()) - 1);
+                unsigned nv = childIndex[index] + 1;
+                if (nv < maxs[index] && nv <= max_i)
+                {
+                  childIndex[index] = nv;
+                  index++;
+                }
+                else
+                {
+                  childIndex.pop_back();
+                  index--;
+                }
+              }
+            }
+            success = index >= 0;
+            if (success)
+            {
+              Trace("inst-alg-rd") << "Try instantiation { ";
+              for (unsigned j = 0; j < childIndex.size(); j++)
+              {
+                Trace("inst-alg-rd") << childIndex[j] << " ";
+              }
+              Trace("inst-alg-rd") << "}" << std::endl;
+              // try instantiation
+              std::vector<Node> terms;
+              for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+              {
+                if (max_zero[i])
+                {
+                  // no terms available, will report incomplete instantiation
+                  terms.push_back(Node::null());
+                  Trace("inst-alg-rd") << "  null" << std::endl;
+                }
+                else if (r == 0)
+                {
+                  terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]);
+                  Trace("inst-alg-rd")
+                      << "  " << rd->getRDomain(f, i)->d_terms[childIndex[i]]
+                      << std::endl;
+                }
+                else
+                {
+                  Assert(childIndex[i] < term_db_list[ftypes[i]].size());
+                  terms.push_back(term_db_list[ftypes[i]][childIndex[i]]);
+                  Trace("inst-alg-rd") << "  "
+                                       << term_db_list[ftypes[i]][childIndex[i]]
+                                       << std::endl;
+                }
+              }
+              if (d_quantEngine->addInstantiation(f, terms))
+              {
+                Trace("inst-alg-rd") << "Success!" << std::endl;
+                ++(d_quantEngine->d_statistics.d_instantiations_guess);
+                return true;
+              }
+              else
+              {
+                index--;
+              }
+            }
+          } while (success);
+          max_i++;
+        }
+      }
+    }
+  }
+  // TODO : term enumerator instantiation?
+  return false;
+}
+
+void InstStrategyEnum::registerQuantifier(Node q) {}
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
new file mode 100644
index 000000000..d79917eda
--- /dev/null
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file inst_strategy_enumerative.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 Enumerative instantiation
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGY_ENUMERATIVE_H
+#define __CVC4__INST_STRATEGY_ENUMERATIVE_H
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Enumerative instantiation
+ *
+ * This class implements enumerative instantiation described
+ * in Reynolds et al., "Revisiting Enumerative Instantiation".
+ *
+ * It is an instance of QuantifiersModule, whose main
+ * task is to make calls to QuantifiersEngine during
+ * calls to QuantifiersModule::check(...).
+ *
+ * This class adds instantiations based on enumerating
+ * well-typed terms that occur in the current context
+ * based on a heuristically determined ordering on
+ * tuples of terms. This ordering incorporates
+ * reasoning about the relevant domain of quantified
+ * formulas (see theory/quantifiers/relevant_domain.h).
+ * We consider only ground terms that occur in the
+ * context due to Theorem 1 of "Revisiting Enumerative
+ * Instantiation". Notice this theorem holds only for theories
+ * with compactness. For theories such as arithmetic,
+ * this class may introduce "default" terms that are
+ * used in instantiations, say 0 for arithmetic, even
+ * when the term 0 does not occur in the context.
+ *
+ * This strategy is not enabled by default, and
+ * is enabled by the option:
+ *   --full-saturate-quant
+ *
+ * It is generally called with lower priority than
+ * other instantiation strategies, although this
+ * option interleaves it with other strategies
+ * during quantifier effort level QEFFORT_STANDARD:
+ *   --fs-interleave
+ */
+class InstStrategyEnum : public QuantifiersModule
+{
+ public:
+  InstStrategyEnum(QuantifiersEngine* qe);
+  ~InstStrategyEnum() {}
+  /** Needs check. */
+  bool needsCheck(Theory::Effort e) override;
+  /** Reset round. */
+  void reset_round(Theory::Effort e) override;
+  /** Check.
+   * Adds instantiations for all currently asserted
+   * quantified formulas via calls to process(...)
+   */
+  void check(Theory::Effort e, unsigned quant_e) override;
+  /** Register quantifier. */
+  void registerQuantifier(Node q) override;
+  /** Identify. */
+  std::string identify() const override
+  {
+    return std::string("InstStrategyEnum");
+  }
+
+ private:
+  /** process quantified formula
+   *
+   * q is the quantified formula we are constructing instances for.
+   * fullEffort is whether we are called at full effort.
+   *
+   * If this function returns true, then one instantiation
+   * (determined by an enumeration) was added via a successful
+   * call to QuantifiersEngine::addInstantiation(...).
+   *
+   * If fullEffort is true, then we may introduce a "default"
+   * well-typed term *not* occurring in the current context.
+   * This handles corner cases where there are no well-typed
+   * ground terms in the current context to instantiate with.
+   */
+  bool process(Node q, bool fullEffort);
+}; /* class InstStrategyEnum */
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fdb70c85b..2d5f48a5c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -19,25 +19,29 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/datatypes/theory_datatypes.h"
-#include "theory/sep/theory_sep.h"
 #include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/anti_skolem.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/ceg_t_instantiator.h"
 #include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/equality_infer.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/fun_def_engine.h"
+#include "theory/quantifiers/inst_propagator.h"
 #include "theory/quantifiers/inst_strategy_cbqi.h"
 #include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_enumerative.h"
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/quantifiers/local_theory_ext.h"
 #include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_equality_engine.h"
+#include "theory/quantifiers/quant_split.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/rewrite_engine.h"
@@ -45,10 +49,7 @@
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/quant_split.h"
-#include "theory/quantifiers/anti_skolem.h"
-#include "theory/quantifiers/equality_infer.h"
-#include "theory/quantifiers/inst_propagator.h"
+#include "theory/sep/theory_sep.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -298,7 +299,7 @@ void QuantifiersEngine::finishInit(){
   }
   //full saturation : instantiate from relevant domain, then arbitrary terms
   if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
-    d_fs = new quantifiers::FullSaturation( this );
+    d_fs = new quantifiers::InstStrategyEnum(this);
     d_modules.push_back( d_fs );
     needsRelDom = true;
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0bb5b10e5..be0c4cd43 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -74,7 +74,7 @@ namespace quantifiers {
   class AlphaEquivalence;
   class FunDefEngine;
   class QuantEqualityEngine;
-  class FullSaturation;
+  class InstStrategyEnum;
   class InstStrategyCbqi;
   class InstStrategyCegqi;
   class QuantDSplit;
@@ -155,7 +155,7 @@ private:
   /** quantifiers equality engine */
   quantifiers::QuantEqualityEngine * d_uee;
   /** full saturation */
-  quantifiers::FullSaturation * d_fs;
+  quantifiers::InstStrategyEnum* d_fs;
   /** counterexample-based quantifier instantiation */
   quantifiers::InstStrategyCbqi * d_i_cbqi;
   /** quantifiers splitting */
@@ -275,7 +275,7 @@ public:  //modules
   /** quantifiers equality engine */
   quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
   /** get full saturation */
-  quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
+  quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; }
   /** get inst strategy cbqi */
   quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
   /** get quantifiers splitting */