(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

6 files changed, 253 insertions, 47 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;