1 files changed, 32 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 458ba07bc..36b58fd60 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -28,7 +28,6 @@
 #include "theory/quantifiers/equality_infer.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_epr.h"
@@ -114,8 +113,6 @@ public:
   quantifiers::RelevantDomain* getRelevantDomain() const;
   //---------------------- end utilities
   //---------------------- modules (TODO remove these #1163)
-  /** get bounded integers utility */
-  quantifiers::BoundedIntegers* getBoundedIntegers() const;
   /** ceg instantiation */
   quantifiers::SynthEngine* getSynthEngine() const;
   //---------------------- end modules
@@ -144,9 +141,38 @@ public:
   void setOwner(Node q, quantifiers::QAttributes& qa);
   /** considers */
   bool hasOwnership( Node q, QuantifiersModule * m = NULL );
-  /** is finite bound */
-  bool isFiniteBound( Node q, Node v );
-public:
+  /** does variable v of quantified formula q have a finite bound? */
+  bool isFiniteBound(Node q, Node v) const;
+  /** get bound var type
+   *
+   * This returns the type of bound that was inferred for variable v of
+   * quantified formula q.
+   */
+  BoundVarType getBoundVarType(Node q, Node v) const;
+  /**
+   * Get the indices of bound variables, in the order they should be processed
+   * in a RepSetIterator.
+   *
+   * For details, see BoundedIntegers::getBoundVarIndices.
+   */
+  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.
+   *
+   * For details, see BoundedIntegers::getBoundElements.
+   */
+  bool getBoundElements(RepSetIterator* rsi,
+                        bool initial,
+                        Node q,
+                        Node v,
+                        std::vector<Node>& elements) const;
+
+ public:
   /** presolve */
   void presolve();
   /** notify preprocessed assertion */