(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

1 files changed, 63 insertions, 22 deletions

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);
         }
       }
     }