1 files changed, 55 insertions, 25 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 8e6738e9e..d668c6f02 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -30,28 +30,23 @@ class RepSetIterator;
 
 namespace quantifiers {
 
-
 class BoundedIntegers : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashMap<int, bool> IntBoolMap;
-public:
-  enum {
-    BOUND_FINITE,
-    BOUND_INT_RANGE,
-    BOUND_SET_MEMBER,
-    BOUND_FIXED_SET,
-    BOUND_NONE
-  };
 private:
   //for determining bounds
-  bool isBound( Node f, Node v );
   bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited );
   bool hasNonBoundVar( Node f, Node b );
-  //bound type
-  std::map< Node, std::map< Node, unsigned > > d_bound_type;
+  /** The bound type for each quantified formula, variable pair */
+  std::map<Node, std::map<Node, BoundVarType>> d_bound_type;
+  /**
+   * The ordered list of variables that are finitely bound, for each quantified
+   * formulas. Variables that occur later in this list may depend on having
+   * finite bounds for variables earlier in this list.
+   */
   std::map< Node, std::vector< Node > > d_set;
   std::map< Node, std::map< Node, int > > d_set_nums;
   std::map< Node, std::map< Node, Node > > d_range;
@@ -152,9 +147,6 @@ private:
     }
   };
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
-private:
-  
-  void setBoundedVar( Node f, Node v, unsigned bound_type );
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
   virtual ~BoundedIntegers();
@@ -163,11 +155,54 @@ public:
   bool needsCheck(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
   void checkOwnership(Node q) override;
-  bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
-  unsigned getBoundVarType( Node q, Node v );
-  unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
-  Node getBoundVar( Node q, int i ) { return d_set[q][i]; }
-private:
+  /**
+   * Is v a variable of quantified formula q that this class has inferred to
+   * have a finite bound?
+   */
+  bool isBound(Node q, Node v) const;
+  /**
+   * Get the type of bound that was inferred for variable v of quantified
+   * formula q, or BOUND_NONE if no bound was inferred.
+   */
+  BoundVarType getBoundVarType(Node q, Node v) const;
+  /**
+   * Get the indices of bound variables, in the order they should be processed
+   * in a RepSetIterator. For example, for q:
+   *   forall xyz. 0 <= x < 5 ^ 0 <= z <= x+7 => P(x,y,z)
+   * this would add {1,3} to the vector indices, indicating that x has a finite
+   * bound, z has a finite bound assuming x has a finite bound, and y does not
+   * have a finite bound.
+   */
+  void getBoundVarIndices(Node q, std::vector<unsigned>& indices) const;
+  /**
+   * Get bound elements
+   *
+   * This gets the (finite) enumeration of the range of variable v of quantified
+   * formula q and adds it into the vector elements in the context of the
+   * iteration being performed by rsi. It returns true if it could successfully
+   * determine this range.
+   *
+   * This method determines the range of a variable depending on the current
+   * state of the iterator rsi and flag initial (which is true when rsi is
+   * being initialized). For example, if q is:
+   *   forall xy. 0 <= x < 5 ^ 0 <= y <= x+7 => P(x,y)
+   * v is y, and rsi currently maps x to 4, then we add the elements 0...11 to
+   * the vector elements.
+   */
+  bool getBoundElements(RepSetIterator* rsi,
+                        bool initial,
+                        Node q,
+                        Node v,
+                        std::vector<Node>& elements);
+  /** Identify this module */
+  std::string identify() const override { return "BoundedIntegers"; }
+
+ private:
+  /**
+   * Set that variable v of quantified formula q has a finite bound, where
+   * bound_type indicates how that bound was inferred.
+   */
+  void setBoundedVar(Node f, Node v, BoundVarType bound_type);
   //for integer range
   Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
   Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
@@ -180,11 +215,6 @@ private:
   Node matchBoundVar( Node v, Node t, Node e );
   
   bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
-public:
-  bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements );
-
-  /** Identify this module */
-  std::string identify() const override { return "BoundedIntegers"; }
 };
 
 }