(Refactor) Decouple rep set iterator and quantifiers (#1339)

* Refactoring rep set iterator, does not modify rep set externally.

* Decouple quantifiers engine and rep set iterator.

* Documentation

* Clang format

* Minor

* Minor

* More

* Format

* Address review.

* Format

* Minor

8 files changed, 550 insertions, 244 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index f3244937d..972b404de 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -739,14 +739,8 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
     Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
     int v = rsi->getVariableOrder( i );
     Assert( q[0][v]==d_set[q][i] );
-    Node t = rsi->getCurrentTerm( v );
+    Node t = rsi->getCurrentTerm(v, true);
     Trace("bound-int-rsi") << "term : " << t << std::endl;
-    Node tt = rsi->d_rep_set->getTermForRepresentative(t);
-    if (!tt.isNull())
-    {
-      t = tt;
-      Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl;
-    }
     vars.push_back( d_set[q][i] );
     subs.push_back( t );
   }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index f4cf1b32a..6749a8c0d 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -16,6 +16,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -26,13 +27,14 @@
 #define USE_INDEX_ORDERING
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::quantifiers::fmcheck;
 
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
 struct sortQuantifierRelevance {
   FirstOrderModel * d_fm;
   bool operator() (Node i, Node j) {
@@ -46,6 +48,83 @@ struct sortQuantifierRelevance {
   }
 };
 
+RepSetIterator::RsiEnumType QRepBoundExt::setBound(Node owner,
+                                                   unsigned i,
+                                                   std::vector<Node>& elements)
+{
+  // builtin: check if it is bound by bounded integer module
+  if (owner.getKind() == FORALL && d_qe->getBoundedIntegers())
+  {
+    if (d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i]))
+    {
+      unsigned bvt =
+          d_qe->getBoundedIntegers()->getBoundVarType(owner, owner[0][i]);
+      if (bvt != BoundedIntegers::BOUND_FINITE)
+      {
+        d_bound_int[i] = true;
+        return RepSetIterator::ENUM_BOUND_INT;
+      }
+      else
+      {
+        // indicates the variable is finitely bound due to
+        // the (small) cardinality of its type,
+        // will treat in default way
+      }
+    }
+  }
+  return RepSetIterator::ENUM_INVALID;
+}
+
+bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
+                              Node owner,
+                              unsigned i,
+                              bool initial,
+                              std::vector<Node>& elements)
+{
+  if (d_bound_int.find(i) != d_bound_int.end())
+  {
+    Assert(owner.getKind() == FORALL);
+    Assert(d_qe->getBoundedIntegers() != nullptr);
+    if (!d_qe->getBoundedIntegers()->getBoundElements(
+            rsi, initial, owner, owner[0][i], elements))
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
+{
+  return d_qe->getModel()->initializeRepresentativesForType(tn);
+}
+
+bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
+{
+  // must set a variable index order based on bounded integers
+  if (owner.getKind() == FORALL && d_qe->getBoundedIntegers())
+  {
+    Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
+    for (unsigned i = 0; i < d_qe->getBoundedIntegers()->getNumBoundVars(owner);
+         i++)
+    {
+      Node v = d_qe->getBoundedIntegers()->getBoundVar(owner, i);
+      Trace("bound-int-rsi") << "  bound var #" << i << " is " << v
+                             << std::endl;
+      varOrder.push_back(d_qe->getTermUtil()->getVariableNum(owner, v));
+    }
+    for (unsigned i = 0; i < owner[0].getNumChildren(); i++)
+    {
+      if (!d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i]))
+      {
+        varOrder.push_back(i);
+      }
+    }
+    return true;
+  }
+  return false;
+}
+
 FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
 TheoryModel( c, name, true ),
 d_qe( qe ), d_forall_asserts( c ){
@@ -104,18 +183,51 @@ void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& vi
 
 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;
+  if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0)
+  {
+    Trace("fm-debug") << "Must create domain element for " << tn << "..."
+                      << std::endl;
     Node mbt = getModelBasisTerm(tn);
-    Trace("fmc-model-debug") << "Add to representative set..." << std::endl;
+    Trace("fm-debug") << "Add to representative set..." << std::endl;
     d_rep_set.add(tn, mbt);
-  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
-    Message() << "empty reps" << std::endl;
-    exit(0);
   }
   return d_rep_set.d_type_reps[tn][0];
 }
 
+bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
+{
+  if (tn.isSort())
+  {
+    // must ensure uninterpreted type is non-empty.
+    if (!d_rep_set.hasType(tn))
+    {
+      // terms in rep_set are now constants which mapped to terms through
+      // TheoryModel. Thus, should introduce a constant and a term.
+      // For now, we just add an arbitrary term.
+      Node var = d_qe->getModel()->getSomeDomainElement(tn);
+      Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
+                     << std::endl;
+      d_rep_set.add(tn, var);
+    }
+    return true;
+  }
+  else
+  {
+    // can we complete it?
+    if (d_qe->getTermEnumeration()->mayComplete(tn))
+    {
+      Trace("fm-debug") << "  do complete, since cardinality is small ("
+                        << tn.getCardinality() << ")..." << std::endl;
+      d_rep_set.complete(tn);
+      // must have succeeded
+      Assert(d_rep_set.hasType(tn));
+      return true;
+    }
+    Trace("fm-debug") << "  variable cannot be bounded." << std::endl;
+    return false;
+  }
+}
+
 /** needs check */
 bool FirstOrderModel::checkNeeded() {
   return d_forall_asserts.size()>0;
@@ -1022,3 +1134,7 @@ void FirstOrderModelAbs::processInitializeQuantifier( Node q ) {
 Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) {
   return q[0][d_var_order[q][i]];
 }
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 6305a3807..57582a856 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -54,6 +54,40 @@ class FirstOrderModelAbs;
 struct IsStarAttributeId {};
 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 
+/** Quantifiers representative bound
+ *
+ * This class is used for computing (finite)
+ * bounds for the domain of a quantifier
+ * in the context of a RepSetIterator
+ * (see theory/rep_set.h).
+ */
+class QRepBoundExt : public RepBoundExt
+{
+ public:
+  QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
+  virtual ~QRepBoundExt() {}
+  /** set bound */
+  virtual RepSetIterator::RsiEnumType setBound(
+      Node owner, unsigned i, std::vector<Node>& elements) override;
+  /** reset index */
+  virtual bool resetIndex(RepSetIterator* rsi,
+                          Node owner,
+                          unsigned i,
+                          bool initial,
+                          std::vector<Node>& elements) override;
+  /** initialize representative set for type */
+  virtual bool initializeRepresentativesForType(TypeNode tn) override;
+  /** get variable order */
+  virtual bool getVariableOrder(Node owner,
+                                std::vector<unsigned>& varOrder) override;
+
+ private:
+  /** quantifiers engine associated with this bound */
+  QuantifiersEngine* d_qe;
+  /** indices that are bound integer enumeration */
+  std::map<unsigned, bool> d_bound_int;
+};
+
 // TODO (#1301) : document and refactor this class
 class FirstOrderModel : public TheoryModel
 {
@@ -109,6 +143,22 @@ class FirstOrderModel : public TheoryModel
   unsigned getModelBasisArg(Node n);
   /** get some domain element */
   Node getSomeDomainElement(TypeNode tn);
+  /** initialize representative set for type
+   *
+   * This ensures that TheoryModel::d_rep_set
+   * is initialized for type tn. In particular:
+   * (1) If tn is an uninitialized (unconstrained)
+   * uninterpreted sort, then we interpret it
+   * as a set of size one,
+   * (2) If tn is a "small" enumerable finite type,
+   * then we ensure that all its values are in
+   * TheoryModel::d_rep_set.
+   *
+   * Returns true if the initialization was complete,
+   * in that the set for tn in TheoryModel::d_rep_set
+   * has all representatives of type tn.
+   */
+  bool initializeRepresentativesForType(TypeNode tn);
 
  protected:
   /** quant engine */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 5847449cf..4277ab366 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -747,36 +747,76 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
   }
 }
 
-class RepBoundFmcEntry : public RepBoundExt {
-public:
-  Node d_entry;
-  FirstOrderModelFmc * d_fm;
-  bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) {
-    if( d_fm->isInterval(d_entry[i]) ){
-      //explicitly add the interval TODO?
-    }else if( d_fm->isStar(d_entry[i]) ){
-      //add the full range
-      return false;
-    }else{
-      //only need to consider the single point
-      elements.push_back( d_entry[i] );
-      return true;
+/** Representative bound fmc entry
+ *
+ * This bound information corresponds to one
+ * entry in a term definition (see terminology in
+ * Chapter 5 of Finite Model Finding for
+ * Satisfiability Modulo Theories thesis).
+ * For example, a term definition for the body
+ * of a quantified formula:
+ *   forall xyz. P( x, y, z )
+ * may be:
+ *   ( 0, 0, 0 ) -> false
+ *   ( *, 1, 2 ) -> false
+ *   ( *, *, * ) -> true
+ * Indicating that the quantified formula evaluates
+ * to false in the current model for x=0, y=0, z=0,
+ * or y=1, z=2 for any x, and evaluates to true
+ * otherwise.
+ * This class is used if we wish
+ * to iterate over all values corresponding to one
+ * of these entries. For example, for the second entry:
+ *   (*, 1, 2 )
+ * we iterate over all values of x, but only {1}
+ * for y and {2} for z.
+ */
+class RepBoundFmcEntry : public QRepBoundExt
+{
+ public:
+  RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f)
+      : QRepBoundExt(qe), d_entry(e), d_fm(f)
+  {
+  }
+  ~RepBoundFmcEntry() {}
+  /** set bound */
+  virtual RepSetIterator::RsiEnumType setBound(
+      Node owner, unsigned i, std::vector<Node>& elements) override
+  {
+    if (d_fm->isInterval(d_entry[i]))
+    {
+      // explicitly add the interval?
     }
-    return false;
+    else if (d_fm->isStar(d_entry[i]))
+    {
+      // must add the full range
+    }
+    else
+    {
+      // only need to consider the single point
+      elements.push_back(d_entry[i]);
+      return RepSetIterator::ENUM_DEFAULT;
+    }
+    return QRepBoundExt::setBound(owner, i, elements);
   }
+
+ private:
+  /** the entry for this bound */
+  Node d_entry;
+  /** the model builder associated with this bound */
+  FirstOrderModelFmc* d_fm;
 };
 
 bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
-  RepSetIterator riter( d_qe, &(fm->d_rep_set) );
   Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
-  RepBoundFmcEntry rbfe;
-  rbfe.d_entry = c;
-  rbfe.d_fm = fm;
+  RepBoundFmcEntry rbfe(d_qe, c, fm);
+  RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe);
   Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
   //initialize
-  if( riter.setQuantifier( f, &rbfe ) ){
+  if (riter.setQuantifier(f))
+  {
     Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
     int addedLemmas = 0;
     //now do full iteration
@@ -785,7 +825,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       Trace("fmc-exh-debug") << "Inst : ";
       std::vector< Node > ev_inst;
       std::vector< Node > inst;
-      for( int i=0; i<riter.getNumTerms(); i++ ){
+      for (unsigned i = 0; i < riter.getNumTerms(); i++)
+      {
         Node rr = riter.getCurrentTerm( i );
         Node r = rr;
         //if( r.getType().isSort() ){
@@ -822,7 +863,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       if( !riter.isFinished() ){
         if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) {
           Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
-          riter.increment2( index-1 );
+          riter.incrementAtIndex(index - 1);
         }
       }
     }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index a72293ea1..358838b11 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -108,12 +108,14 @@ void QModelBuilder::debugModel( TheoryModel* m ){
       for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
         vars.push_back( f[0][j] );
       }
-      RepSetIterator riter(d_qe, fm->getRepSetPtr());
+      QRepBoundExt qrbe(d_qe);
+      RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
       if( riter.setQuantifier( f ) ){
         while( !riter.isFinished() ){
           tests++;
           std::vector< Node > terms;
-          for( int k=0; k<riter.getNumTerms(); k++ ){
+          for (unsigned k = 0; k < riter.getNumTerms(); k++)
+          {
             terms.push_back( riter.getCurrentTerm( k ) );
           }
           Node n = d_qe->getInstantiation( f, vars, terms );
@@ -419,7 +421,8 @@ QModelBuilderIG::Statistics::~Statistics(){
 //do exhaustive instantiation
 int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
-    RepSetIterator riter(d_qe, d_qe->getModel()->getRepSetPtr());
+    QRepBoundExt qrbe(d_qe);
+    RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
     if( riter.setQuantifier( f ) ){
       FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
       Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
@@ -452,11 +455,12 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
         }
         if( eval==1 ){
           //instantiation is already true -> skip
-          riter.increment2( depIndex );
+          riter.incrementAtIndex(depIndex);
         }else{
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
-          for( int i=0; i<riter.getNumTerms(); i++ ){
+          for (unsigned i = 0; i < riter.getNumTerms(); i++)
+          {
             m.set( d_qe, i, riter.getCurrentTerm( i ) );
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
@@ -468,7 +472,7 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
             }
             //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
             if( eval==-1 ){
-              riter.increment2( depIndex );
+              riter.incrementAtIndex(depIndex);
             }else{
               riter.increment();
             }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 88b16bfd3..c4a0b5c5d 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -277,8 +277,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       Trace("fmf-exh-inst-debug") << std::endl;
     }
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
-    RepSetIterator riter(d_quantEngine,
-                         d_quantEngine->getModel()->getRepSetPtr());
+    QRepBoundExt qrbe(d_quantEngine);
+    RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe);
     if( riter.setQuantifier( f ) ){
       Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
       if( !riter.isIncomplete() ){
@@ -287,7 +287,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
-          for( int i=0; i<riter.getNumTerms(); i++ ){
+          for (unsigned i = 0; i < riter.getNumTerms(); i++)
+          {
             m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 5c02b631c..bff5e36cd 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -14,18 +14,14 @@
 
 #include <unordered_set>
 
-#include "theory/quantifiers/bounded_integers.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/rep_set.h"
 #include "theory/type_enumerator.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace theory {
 
 void RepSet::clear(){
   d_type_reps.clear();
@@ -64,6 +60,14 @@ Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
   return it->second[i];
 }
 
+void RepSet::getRepresentatives(TypeNode tn, std::vector<Node>& reps) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_reps.find(tn);
+  Assert(it != d_type_reps.end());
+  reps.insert(reps.end(), it->second.begin(), it->second.end());
+}
+
 bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
 {
   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
@@ -184,43 +188,44 @@ void RepSet::toStream(std::ostream& out){
   }
 }
 
-
-RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
-  d_incomplete = false;
+RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext)
+    : d_rs(rs), d_rext(rext), d_incomplete(false)
+{
 }
 
-int RepSetIterator::domainSize( int i ) {
-  Assert(i>=0);
-  int v = d_var_order[i];
+unsigned RepSetIterator::domainSize(unsigned i)
+{
+  unsigned v = d_var_order[i];
   return d_domain_elements[v].size();
 }
 
-bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){
-  Trace("rsi") << "Make rsi for " << f << std::endl;
+bool RepSetIterator::setQuantifier(Node q)
+{
+  Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
   Assert( d_types.empty() );
   //store indicies
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    d_types.push_back( f[0][i].getType() );
+  for (size_t i = 0; i < q[0].getNumChildren(); i++)
+  {
+    d_types.push_back(q[0][i].getType());
   }
-  d_owner = f;
-  return initialize( rext );
+  d_owner = q;
+  return initialize();
 }
 
-bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){
-  Trace("rsi") << "Make rsi for " << op << std::endl;
+bool RepSetIterator::setFunctionDomain(Node op)
+{
+  Trace("rsi") << "Make rsi for function " << op << std::endl;
   Assert( d_types.empty() );
   TypeNode tn = op.getType();
   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
     d_types.push_back( tn[i] );
   }
   d_owner = op;
-  return initialize( rext );
+  return initialize();
 }
 
-// TODO : as part of #1199, the portions of this
-// function which modify d_rep_set should be
-// moved to TheoryModel.
-bool RepSetIterator::initialize( RepBoundExt* rext ){
+bool RepSetIterator::initialize()
+{
   Trace("rsi") << "Initialize rep set iterator..." << std::endl;
   for( unsigned v=0; v<d_types.size(); v++ ){
     d_index.push_back( 0 );
@@ -232,103 +237,81 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){
     d_domain_elements.push_back( std::vector< Node >() );
     TypeNode tn = d_types[v];
     Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
-    if( tn.isSort() ){
-      //must ensure uninterpreted type is non-empty.
-      if( !d_rep_set->hasType( tn ) ){
-        //FIXME:
-        // terms in rep_set are now constants which mapped to terms through TheoryModel
-        // thus, should introduce a constant and a term.  for now, just a term.
-
-        //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
-        Node var = d_qe->getModel()->getSomeDomainElement( tn );
-        Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
-        d_rep_set->add( tn, var );
-      }
-    }
     bool inc = true;
+    bool setEnum = false;
     //check if it is externally bound
-    if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){
-      d_enum_type.push_back( ENUM_DEFAULT );
-      inc = false;
-    //builtin: check if it is bound by bounded integer module
-    }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
-      if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){
-        unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] );
-        if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){
-          d_enum_type.push_back( ENUM_BOUND_INT );
-          inc = false;
-        }else{
-          //will treat in default way
-        }
+    if (d_rext)
+    {
+      inc = !d_rext->initializeRepresentativesForType(tn);
+      RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]);
+      if (rsiet != ENUM_INVALID)
+      {
+        d_enum_type.push_back(rsiet);
+        inc = false;
+        setEnum = true;
       }
     }
-    if( !tn.isSort() ){
-      if( inc ){
-        if (d_qe->getTermEnumeration()->mayComplete(tn))
-        {
-          Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
-          d_rep_set->complete( tn );
-          //must have succeeded
-          Assert( d_rep_set->hasType( tn ) );
-        }else{
-          Trace("rsi") << "  variable cannot be bounded." << std::endl;
-          Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
-          d_incomplete = true;
-        }
-      }
+    if (inc)
+    {
+      Trace("fmf-incomplete") << "Incomplete because of quantification of type "
+                              << tn << std::endl;
+      d_incomplete = true;
     }
 
     //if we have yet to determine the type of enumeration
-    if( d_enum_type.size()<=v ){
-      if( d_rep_set->hasType( tn ) ){
+    if (!setEnum)
+    {
+      if (d_rs->hasType(tn))
+      {
         d_enum_type.push_back( ENUM_DEFAULT );
-        for( unsigned j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
-          //d_domain[v].push_back( j );
-          d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] );
-        }
+        d_rs->getRepresentatives(tn, d_domain_elements[v]);
       }else{
         Assert( d_incomplete );
         return false;
       }
     }
   }
-  //must set a variable index order based on bounded integers
-  if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
-    Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
-    std::vector< int > varOrder;
-    for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){
-      Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i );
-      Trace("bound-int-rsi") << "  bound var #" << i << " is " << v << std::endl;
-      varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) );
-    }
-    for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
-      if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
-        varOrder.push_back(i);
+
+  if (d_rext)
+  {
+    std::vector<unsigned> varOrder;
+    if (d_rext->getVariableOrder(d_owner, varOrder))
+    {
+      if (Trace.isOn("bound-int-rsi"))
+      {
+        Trace("bound-int-rsi") << "Variable order : ";
+        for (unsigned i = 0; i < varOrder.size(); i++)
+        {
+          Trace("bound-int-rsi") << varOrder[i] << " ";
+        }
+        Trace("bound-int-rsi") << std::endl;
       }
+      std::vector<unsigned> indexOrder;
+      indexOrder.resize(varOrder.size());
+      for (unsigned i = 0; i < varOrder.size(); i++)
+      {
+        Assert(varOrder[i] < indexOrder.size());
+        indexOrder[varOrder[i]] = i;
+      }
+      if (Trace.isOn("bound-int-rsi"))
+      {
+        Trace("bound-int-rsi") << "Will use index order : ";
+        for (unsigned i = 0; i < indexOrder.size(); i++)
+        {
+          Trace("bound-int-rsi") << indexOrder[i] << " ";
+        }
+        Trace("bound-int-rsi") << std::endl;
+      }
+      setIndexOrder(indexOrder);
     }
-    Trace("bound-int-rsi") << "Variable order : ";
-    for( unsigned i=0; i<varOrder.size(); i++) {
-      Trace("bound-int-rsi") << varOrder[i] << " ";
-    }
-    Trace("bound-int-rsi") << std::endl;
-    std::vector< int > indexOrder;
-    indexOrder.resize(varOrder.size());
-    for( unsigned i=0; i<varOrder.size(); i++){
-      indexOrder[varOrder[i]] = i;
-    }
-    Trace("bound-int-rsi") << "Will use index order : ";
-    for( unsigned i=0; i<indexOrder.size(); i++) {
-      Trace("bound-int-rsi") << indexOrder[i] << " ";
-    }
-    Trace("bound-int-rsi") << std::endl;
-    setIndexOrder( indexOrder );
   }
   //now reset the indices
   do_reset_increment( -1, true );
   return true;
 }
 
-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
+void RepSetIterator::setIndexOrder(std::vector<unsigned>& indexOrder)
+{
   d_index_order.clear();
   d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
   //make the d_var_order mapping
@@ -337,20 +320,23 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
   }
 }
 
-int RepSetIterator::resetIndex( int i, bool initial ) {
+int RepSetIterator::resetIndex(unsigned i, bool initial)
+{
   d_index[i] = 0;
-  int v = d_var_order[i];
+  unsigned v = d_var_order[i];
   Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl;
-  if( d_enum_type[v]==ENUM_BOUND_INT ){
-    Assert( d_owner.getKind()==FORALL );
-    if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){
+  if (d_rext)
+  {
+    if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v]))
+    {
       return -1;
     }
   }
   return d_domain_elements[v].empty() ? 0 : 1;
 }
 
-int RepSetIterator::increment2( int i ){
+int RepSetIterator::incrementAtIndex(int i)
+{
   Assert( !isFinished() );
 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
   i = (int)d_index.size()-1;
@@ -402,23 +388,31 @@ int RepSetIterator::do_reset_increment( int i, bool initial ) {
 
 int RepSetIterator::increment(){
   if( !isFinished() ){
-    return increment2( (int)d_index.size()-1 );
+    return incrementAtIndex(d_index.size() - 1);
   }else{
     return -1;
   }
 }
 
-bool RepSetIterator::isFinished(){
-  return d_index.empty();
-}
+bool RepSetIterator::isFinished() const { return d_index.empty(); }
 
-Node RepSetIterator::getCurrentTerm( int v ){
-  int ii = d_index_order[v];
-  int curr = d_index[ii];
+Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm)
+{
+  unsigned ii = d_index_order[v];
+  unsigned curr = d_index[ii];
   Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl;
   Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl;
-  Assert( 0<=curr && curr<(int)d_domain_elements[v].size() );
-  return d_domain_elements[v][curr];
+  Assert(0 <= curr && curr < d_domain_elements[v].size());
+  Node t = d_domain_elements[v][curr];
+  if (valTerm)
+  {
+    Node tt = d_rs->getTermForRepresentative(t);
+    if (!tt.isNull())
+    {
+      return tt;
+    }
+  }
+  return t;
 }
 
 void RepSetIterator::debugPrint( const char* c ){
@@ -435,3 +429,5 @@ void RepSetIterator::debugPrintSmall( const char* c ){
   Debug( c ) << std::endl;
 }
 
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index a20e56184..5b75fa943 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -74,6 +74,8 @@ public:
   unsigned getNumRepresentatives(TypeNode tn) const;
   /** get representative at index */
   Node getRepresentative(TypeNode tn, unsigned i) const;
+  /** get representatives of type tn, appends them to reps */
+  void getRepresentatives(TypeNode tn, std::vector<Node>& reps) const;
   /** add representative n for type tn, where n has type tn */
   void add( TypeNode tn, Node n );
   /** returns index in d_type_reps for node n */
@@ -113,93 +115,195 @@ public:
 //representative domain
 typedef std::vector< int > RepDomain;
 
+class RepBoundExt;
 
-class RepBoundExt {
- public:
-  virtual ~RepBoundExt() {}
-  virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
-};
-
-/** this class iterates over a RepSet */
+/** Rep set iterator.
+ *
+ * This class is used for iterating over (tuples of) terms
+ * in the domain(s) of a RepSet.
+ *
+ * To use it, first it must
+ * be initialized with a call to:
+ * - setQuantifier or setFunctionDomain
+ * which initializes the d_owner field and sets up
+ * initial information.
+ *
+ * Then, we increment over the tuples of terms in the
+ * domains of the owner of this iterator using:
+ * - increment and incrementAtIndex
+ *
+ * TODO (#1199): this class needs further documentation.
+ */
 class RepSetIterator {
 public:
-  enum {
-    ENUM_DEFAULT,
-    ENUM_BOUND_INT,
-  };
-private:
-  QuantifiersEngine * d_qe;
-  //initialize function
-  bool initialize( RepBoundExt* rext = NULL );
-  //for int ranges
-  std::map< int, Node > d_lower_bounds;
-  //for set ranges
-  std::map< int, std::vector< Node > > d_setm_bounds;
-  //domain size
-  int domainSize( int i );
-  //node this is rep set iterator is for
-  Node d_owner;
-  //reset index, 1:success, 0:empty, -1:fail
-  int resetIndex( int i, bool initial = false );
-  /** set index order */
-  void setIndexOrder( std::vector< int >& indexOrder );
-  /** do reset increment the iterator at index=counter */
-  int do_reset_increment( int counter, bool initial = false );
-  //ordering for variables we are indexing over
-  //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
-  //    then we consider instantiations in this order:
-  //      a/x a/y a/z
-  //      a/x b/y a/z
-  //      b/x a/y a/z
-  //      b/x b/y a/z
-  //      ...
-  std::vector< int > d_index_order;
-  //variables to index they are considered at
-  //  for example, if d_index_order = { 2, 0, 1 }
-  //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
-  std::map< int, int > d_var_order;  
-  //are we only considering a strict subset of the domain of the quantifier?
-  bool d_incomplete;
-public:
-  RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
-  ~RepSetIterator(){}
-  //set that this iterator will be iterating over instantiations for a quantifier
-  bool setQuantifier( Node f, RepBoundExt* rext = NULL );
-  //set that this iterator will be iterating over the domain of a function
-  bool setFunctionDomain( Node op, RepBoundExt* rext = NULL );
-public:
-  //pointer to model
-  RepSet* d_rep_set;
-  //enumeration type?
-  std::vector< int > d_enum_type;
-  //current tuple we are considering
-  std::vector< int > d_index;
-  //types we are considering
-  std::vector< TypeNode > d_types;
-  //domain we are considering
-  std::vector< std::vector< Node > > d_domain_elements;
+ enum RsiEnumType
+ {
+   ENUM_INVALID = 0,
+   ENUM_DEFAULT,
+   ENUM_BOUND_INT,
+ };
+
 public:
-  /** increment the iterator at index=counter */
-  int increment2( int i );
-  /** increment the iterator */
-  int increment();
-  /** is the iterator finished? */
-  bool isFinished();
-  /** get the i_th term we are considering */
-  Node getCurrentTerm( int v );
-  /** get the number of terms we are considering */
-  int getNumTerms() { return (int)d_index_order.size(); }
-  /** debug print */
-  void debugPrint( const char* c );
-  void debugPrintSmall( const char* c );
-  //get index order, returns var #
-  int getIndexOrder( int v ) { return d_index_order[v]; }
-  //get variable order, returns index #
-  int getVariableOrder( int i ) { return d_var_order[i]; }
-  //is incomplete
-  bool isIncomplete() { return d_incomplete; }
+ RepSetIterator(const RepSet* rs, RepBoundExt* rext);
+ ~RepSetIterator() {}
+ /** set that this iterator will be iterating over instantiations for a
+  * quantifier */
+ bool setQuantifier(Node q);
+ /** set that this iterator will be iterating over the domain of a function */
+ bool setFunctionDomain(Node op);
+ /** increment the iterator */
+ int increment();
+ /** increment the iterator at index
+  * This increments the i^th field of the
+  * iterator, for examples, see operator next_i
+  * in Figure 2 of Reynolds et al. CADE 2013.
+  */
+ int incrementAtIndex(int i);
+ /** is the iterator finished? */
+ bool isFinished() const;
+ /** get domain size of the i^th field of this iterator */
+ unsigned domainSize(unsigned i);
+ /** get the i^th term in the tuple we are considering */
+ Node getCurrentTerm(unsigned v, bool valTerm = false);
+ /** get the number of terms in the tuple we are considering */
+ unsigned getNumTerms() { return d_index_order.size(); }
+ /** get index order, returns var # */
+ unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
+ /** get variable order, returns index # */
+ unsigned getVariableOrder(unsigned i) { return d_var_order[i]; }
+ /** is incomplete
+  * Returns true if we are iterating over a strict subset of
+  * the domain of the quantified formula or function.
+  */
+ bool isIncomplete() { return d_incomplete; }
+ /** debug print methods */
+ void debugPrint(const char* c);
+ void debugPrintSmall(const char* c);
+ // TODO (#1199): these should be private
+ /** enumeration type for each field */
+ std::vector<RsiEnumType> d_enum_type;
+ /** the current tuple we are considering */
+ std::vector<int> d_index;
+
+private:
+ /** rep set associated with this iterator */
+ const RepSet* d_rs;
+ /** rep set external bound information for this iterator */
+ RepBoundExt* d_rext;
+ /** types we are considering */
+ std::vector<TypeNode> d_types;
+ /** for each argument, the domain we are iterating over */
+ std::vector<std::vector<Node> > d_domain_elements;
+ /** initialize
+  * This is called when the owner of this iterator is set.
+  * It initializes the typing information for the types
+  * that are involved in this iterator, initializes the
+  * domain elements we are iterating over, and variable
+  * and index orderings we are considering.
+  */
+ bool initialize();
+ /** owner
+  * This is the term that we are iterating for, which may either be:
+  * (1) a quantified formula, or
+  * (2) a function.
+  */
+ Node d_owner;
+ /** reset index, 1:success, 0:empty, -1:fail */
+ int resetIndex(unsigned i, bool initial = false);
+ /** set index order (see below) */
+ void setIndexOrder(std::vector<unsigned>& indexOrder);
+ /** do reset increment the iterator at index=counter */
+ int do_reset_increment(int counter, bool initial = false);
+ /** ordering for variables we are iterating over
+ *  For example, given reps = { a, b } and quantifier
+ *    forall( x, y, z ) P( x, y, z )
+ *  with d_index_order = { 2, 0, 1 },
+ *    then we consider instantiations in this order:
+ *      a/x a/y a/z
+ *      a/x b/y a/z
+ *      b/x a/y a/z
+ *      b/x b/y a/z
+ *      ...
+ */
+ std::vector<unsigned> d_index_order;
+ /** Map from variables to the index they are considered at
+ * For example, if d_index_order = { 2, 0, 1 }
+ *    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
+ */
+ std::map<unsigned, unsigned> d_var_order;
+ /** incomplete flag */
+ bool d_incomplete;
 };/* class RepSetIterator */
 
+/** Representative bound external
+ *
+ * This class manages bound information
+ * for an instance of a RepSetIterator.
+ * Its main functionalities are to set
+ * bounds on the domain of the iterator
+ * over quantifiers and function arguments.
+ */
+class RepBoundExt
+{
+ public:
+  virtual ~RepBoundExt() {}
+  /** set bound
+   *
+   * This method initializes the vector "elements"
+   * with list of terms to iterate over for the i^th
+   * field of owner, where owner may be :
+   * (1) A function, in which case we are iterating
+   *     over domain elements of its argument type,
+   * (2) A quantified formula, in which case we are
+   *     iterating over domain elements of the type
+   *     of its i^th bound variable.
+   */
+  virtual RepSetIterator::RsiEnumType setBound(Node owner,
+                                               unsigned i,
+                                               std::vector<Node>& elements) = 0;
+  /** reset index
+   *
+   * This method initializes iteration for the i^th
+   * field of owner, based on the current state of
+   * the iterator rsi. It initializes the vector
+   * "elements" with all appropriate terms to
+   * iterate over in this context.
+   * initial is whether this is the first call
+   * to this function for this iterator.
+   *
+   * This method returns false if we were unable
+   * to establish (finite) bounds for the current
+   * field we are considering, which indicates that
+   * the iterator will terminate with a failure.
+   */
+  virtual bool resetIndex(RepSetIterator* rsi,
+                          Node owner,
+                          unsigned i,
+                          bool initial,
+                          std::vector<Node>& elements)
+  {
+    return true;
+  }
+  /** initialize representative set for type
+   *
+   * Returns true if the representative set associated
+   * with this bound has been given a complete interpretation
+   * for type tn.
+   */
+  virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
+  /** get variable order
+   * If this method returns true, then varOrder is the order
+   * in which we want to consider variables for the iterator.
+   * If this method returns false, then varOrder is unchanged
+   * and the RepSetIterator is free to choose a default
+   * variable order.
+   */
+  virtual bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
+  {
+    return false;
+  }
+};
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */