(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, 185 insertions, 81 deletions

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 */