Refactoring finite bounds in Quantifiers Engine (#3261)

1 files changed, 19 insertions, 11 deletions

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index d972a7a84..2ae5e1c4b 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -121,6 +121,22 @@ typedef std::vector< int > RepDomain;
 
 class RepBoundExt;
 
+/**
+ * Representative set iterator enumeration type, which indicates how the
+ * bound on a variable was determined.
+ */
+enum RsiEnumType
+{
+  // the bound on the variable is invalid
+  ENUM_INVALID = 0,
+  // the bound on the variable was determined in the default way, i.e. based
+  // on an enumeration of terms in the model.
+  ENUM_DEFAULT,
+  // The bound on the variable was determined in a custom way, i.e. via a
+  // quantifiers module like the BoundedIntegers module.
+  ENUM_CUSTOM,
+};
+
 /** Rep set iterator.
  *
  * This class is used for iterating over (tuples of) terms
@@ -140,14 +156,6 @@ class RepBoundExt;
  */
 class RepSetIterator {
 public:
- enum RsiEnumType
- {
-   ENUM_INVALID = 0,
-   ENUM_DEFAULT,
-   ENUM_BOUND_INT,
- };
-
-public:
  RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
  ~RepSetIterator() {}
  /** set that this iterator will be iterating over instantiations for a
@@ -264,9 +272,9 @@ class RepBoundExt
    *     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;
+  virtual RsiEnumType setBound(Node owner,
+                               unsigned i,
+                               std::vector<Node>& elements) = 0;
   /** reset index
    *
    * This method initializes iteration for the i^th