Refactoring finite bounds in Quantifiers Engine (#3261)

14 files changed, 394 insertions, 184 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index becc0be88..d6376fb8d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -521,6 +521,8 @@ libcvc4_add_sources(
   theory/quantifiers/quant_epr.h
   theory/quantifiers/quant_relevance.cpp
   theory/quantifiers/quant_relevance.h
+  theory/quantifiers/quant_rep_bound_ext.cpp
+  theory/quantifiers/quant_rep_bound_ext.h
   theory/quantifiers/quant_split.cpp
   theory/quantifiers/quant_split.h
   theory/quantifiers/quant_util.cpp
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index b2b4c967b..4b8b65697 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -33,83 +33,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-RepSetIterator::RsiEnumType QRepBoundExt::setBound(Node owner,
-                                                   unsigned i,
-                                                   std::vector<Node>& elements)
-{
-  // builtin: check if it is bound by bounded integer module
-  if (owner.getKind() == FORALL && d_qe->getBoundedIntegers())
-  {
-    if (d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i]))
-    {
-      unsigned bvt =
-          d_qe->getBoundedIntegers()->getBoundVarType(owner, owner[0][i]);
-      if (bvt != BoundedIntegers::BOUND_FINITE)
-      {
-        d_bound_int[i] = true;
-        return RepSetIterator::ENUM_BOUND_INT;
-      }
-      else
-      {
-        // indicates the variable is finitely bound due to
-        // the (small) cardinality of its type,
-        // will treat in default way
-      }
-    }
-  }
-  return RepSetIterator::ENUM_INVALID;
-}
-
-bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
-                              Node owner,
-                              unsigned i,
-                              bool initial,
-                              std::vector<Node>& elements)
-{
-  if (d_bound_int.find(i) != d_bound_int.end())
-  {
-    Assert(owner.getKind() == FORALL);
-    Assert(d_qe->getBoundedIntegers() != nullptr);
-    if (!d_qe->getBoundedIntegers()->getBoundElements(
-            rsi, initial, owner, owner[0][i], elements))
-    {
-      return false;
-    }
-  }
-  return true;
-}
-
-bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
-{
-  return d_qe->getModel()->initializeRepresentativesForType(tn);
-}
-
-bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
-{
-  // must set a variable index order based on bounded integers
-  if (owner.getKind() == FORALL && d_qe->getBoundedIntegers())
-  {
-    Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
-    for (unsigned i = 0; i < d_qe->getBoundedIntegers()->getNumBoundVars(owner);
-         i++)
-    {
-      Node v = d_qe->getBoundedIntegers()->getBoundVar(owner, i);
-      Trace("bound-int-rsi") << "  bound var #" << i << " is " << v
-                             << std::endl;
-      varOrder.push_back(d_qe->getTermUtil()->getVariableNum(owner, v));
-    }
-    for (unsigned i = 0; i < owner[0].getNumChildren(); i++)
-    {
-      if (!d_qe->getBoundedIntegers()->isBoundVar(owner, owner[0][i]))
-      {
-        varOrder.push_back(i);
-      }
-    }
-    return true;
-  }
-  return false;
-}
-
 FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
                                  context::Context* c,
                                  std::string name)
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 51b40f589..a113d1b1b 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -49,40 +49,6 @@ namespace fmcheck {
 struct IsStarAttributeId {};
 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
 
-/** Quantifiers representative bound
- *
- * This class is used for computing (finite)
- * bounds for the domain of a quantifier
- * in the context of a RepSetIterator
- * (see theory/rep_set.h).
- */
-class QRepBoundExt : public RepBoundExt
-{
- public:
-  QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
-  virtual ~QRepBoundExt() {}
-  /** set bound */
-  RepSetIterator::RsiEnumType setBound(Node owner,
-                                       unsigned i,
-                                       std::vector<Node>& elements) override;
-  /** reset index */
-  bool resetIndex(RepSetIterator* rsi,
-                  Node owner,
-                  unsigned i,
-                  bool initial,
-                  std::vector<Node>& elements) override;
-  /** initialize representative set for type */
-  bool initializeRepresentativesForType(TypeNode tn) override;
-  /** get variable order */
-  bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
-
- private:
-  /** quantifiers engine associated with this bound */
-  QuantifiersEngine* d_qe;
-  /** indices that are bound integer enumeration */
-  std::map<unsigned, bool> d_bound_int;
-};
-
 // TODO (#1301) : document and refactor this class
 class FirstOrderModel : public TheoryModel
 {
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 879771903..87f0b1ffe 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -94,10 +94,6 @@ void BoundedIntegers::presolve() {
   d_bnd_it.clear();
 }
 
-bool BoundedIntegers::isBound( Node f, Node v ) {
-  return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
-}
-
 bool BoundedIntegers::hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ) {
   if( visited.find( b )==visited.end() ){
     visited[b] = true;
@@ -300,11 +296,13 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e)
   }
   Trace("bint-engine") << "   addedLemma = " << addedLemma << std::endl;
 }
-void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
+void BoundedIntegers::setBoundedVar(Node q, Node v, BoundVarType bound_type)
+{
   d_bound_type[q][v] = bound_type;
   d_set_nums[q][v] = d_set[q].size();
   d_set[q].push_back( v );
-  Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
+  Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v
+                         << std::endl;
 }
 
 void BoundedIntegers::checkOwnership(Node f)
@@ -506,12 +504,43 @@ void BoundedIntegers::checkOwnership(Node f)
   }
 }
 
-unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) {
-  std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v );
-  if( it==d_bound_type[q].end() ){
+bool BoundedIntegers::isBound(Node q, Node v) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator its = d_set.find(q);
+  if (its == d_set.end())
+  {
+    return false;
+  }
+  return std::find(its->second.begin(), its->second.end(), v)
+         != its->second.end();
+}
+
+BoundVarType BoundedIntegers::getBoundVarType(Node q, Node v) const
+{
+  std::map<Node, std::map<Node, BoundVarType> >::const_iterator itb =
+      d_bound_type.find(q);
+  if (itb == d_bound_type.end())
+  {
     return BOUND_NONE;
-  }else{
-    return it->second;
+  }
+  std::map<Node, BoundVarType>::const_iterator it = itb->second.find(v);
+  if (it == itb->second.end())
+  {
+    return BOUND_NONE;
+  }
+  return it->second;
+}
+
+void BoundedIntegers::getBoundVarIndices(Node q,
+                                         std::vector<unsigned>& indices) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it = d_set.find(q);
+  if (it != d_set.end())
+  {
+    for (const Node& v : it->second)
+    {
+      indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v));
+    }
   }
 }
 
@@ -547,7 +576,7 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
 
 bool BoundedIntegers::isGroundRange(Node q, Node v)
 {
-  if (isBoundVar(q, v))
+  if (isBound(q, v))
   {
     if (d_bound_type[q][v] == BOUND_INT_RANGE)
     {
@@ -728,7 +757,7 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
 bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) {
   if( initial || !isGroundRange( q, v ) ){
     elements.clear();
-    unsigned bvt = getBoundVarType( q, v );
+    BoundVarType bvt = getBoundVarType(q, v);
     if( bvt==BOUND_INT_RANGE ){
       Node l, u;
       getBoundValues( q, v, rsi, l, u );
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"; }
 };
 
 }
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 0f06cef74..2306a0565 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -19,6 +19,7 @@
 #include "options/uf_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -746,14 +747,15 @@ class RepBoundFmcEntry : public QRepBoundExt
   }
   ~RepBoundFmcEntry() {}
   /** set bound */
-  virtual RepSetIterator::RsiEnumType setBound(
-      Node owner, unsigned i, std::vector<Node>& elements) override
+  virtual RsiEnumType setBound(Node owner,
+                               unsigned i,
+                               std::vector<Node>& elements) override
   {
     if (!d_fm->isStar(d_entry[i]))
     {
       // only need to consider the single point
       elements.push_back(d_entry[i]);
-      return RepSetIterator::ENUM_DEFAULT;
+      return ENUM_DEFAULT;
     }
     return QRepBoundExt::setBound(owner, i, elements);
   }
@@ -820,8 +822,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       int index = riter.increment();
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
       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;
+        if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0
+            && riter.d_enum_type[index] == ENUM_CUSTOM)
+        {
+          Trace("fmc-exh-debug")
+              << "Since this is a custom enumeration, skip to the next..."
+              << std::endl;
           riter.incrementAtIndex(index - 1);
         }
       }
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index cdbc5e391..63f004448 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index f34dc1b85..35d1f82fd 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_rep_bound_ext.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp
new file mode 100644
index 000000000..8b3aaf589
--- /dev/null
+++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp
@@ -0,0 +1,85 @@
+/*********************                                                        */
+/*! \file quant_rep_bound_ext.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of quantifiers representative bound utility
+ **/
+
+#include "theory/quantifiers/quant_rep_bound_ext.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QRepBoundExt::QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
+
+RsiEnumType QRepBoundExt::setBound(Node owner,
+                                   unsigned i,
+                                   std::vector<Node>& elements)
+{
+  // builtin: check if it is bound by bounded integer module
+  if (owner.getKind() == FORALL)
+  {
+    BoundVarType bvt = d_qe->getBoundVarType(owner, owner[0][i]);
+    if (bvt != BOUND_FINITE)
+    {
+      d_bound_int[i] = true;
+      return ENUM_CUSTOM;
+    }
+    // indicates the variable is finitely bound due to
+    // the (small) cardinality of its type,
+    // will treat in default way
+  }
+  return ENUM_INVALID;
+}
+
+bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
+                              Node owner,
+                              unsigned i,
+                              bool initial,
+                              std::vector<Node>& elements)
+{
+  if (d_bound_int.find(i) == d_bound_int.end())
+  {
+    // not bound
+    return true;
+  }
+  Assert(owner.getKind() == FORALL);
+  if (!d_qe->getBoundElements(rsi, initial, owner, owner[0][i], elements))
+  {
+    return false;
+  }
+  return true;
+}
+
+bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
+{
+  return d_qe->getModel()->initializeRepresentativesForType(tn);
+}
+
+bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
+{
+  // must set a variable index order based on bounded integers
+  if (owner.getKind() != FORALL)
+  {
+    return false;
+  }
+  Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
+  d_qe->getBoundVarIndices(owner, varOrder);
+  return true;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h
new file mode 100644
index 000000000..1e54786a3
--- /dev/null
+++ b/src/theory/quantifiers/quant_rep_bound_ext.h
@@ -0,0 +1,71 @@
+/*********************                                                        */
+/*! \file quant_rep_bound_ext.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Quantifiers representative bound utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+#define CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/rep_set.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+/** Quantifiers representative bound
+ *
+ * This class is used for computing (finite) bounds for the domain of a
+ * quantifier in the context of a RepSetIterator (see theory/rep_set.h)
+ * based on modules from the quantifiers engine.
+ */
+class QRepBoundExt : public RepBoundExt
+{
+ public:
+  QRepBoundExt(QuantifiersEngine* qe);
+  virtual ~QRepBoundExt() {}
+  /** set bound */
+  RsiEnumType setBound(Node owner,
+                       unsigned i,
+                       std::vector<Node>& elements) override;
+  /** reset index */
+  bool resetIndex(RepSetIterator* rsi,
+                  Node owner,
+                  unsigned i,
+                  bool initial,
+                  std::vector<Node>& elements) override;
+  /** initialize representative set for type */
+  bool initializeRepresentativesForType(TypeNode tn) override;
+  /** get variable order */
+  bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
+
+ private:
+  /** Quantifiers engine associated with this bound */
+  QuantifiersEngine* d_qe;
+  /** indices that are bound integer enumeration */
+  std::map<unsigned, bool> d_bound_int;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 43861d6e9..640a62780 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -234,6 +234,24 @@ public:
   virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
 };/* class EqualityQuery */
 
+/** Types of bounds that can be inferred for quantified formulas */
+enum BoundVarType
+{
+  // a variable has a finite bound because it has finite cardinality
+  BOUND_FINITE,
+  // a variable has a finite bound because it is in an integer range, e.g.
+  //   forall x. u <= x <= l => P(x)
+  BOUND_INT_RANGE,
+  // a variable has a finite bound because it is a member of a set, e.g.
+  //   forall x. x in S => P(x)
+  BOUND_SET_MEMBER,
+  // a variable has a finite bound because only a fixed set of terms are
+  // relevant for it in the domain of the quantified formula, e.g.
+  //   forall x. ( x = t1 OR ... OR x = tn ) => P(x)
+  BOUND_FIXED_SET,
+  // a bound has not been inferred for the variable
+  BOUND_NONE
+};
 }
 }
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index def1f969c..a03596060 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/anti_skolem.h"
 #include "theory/quantifiers/conjecture_generator.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/inst_propagator.h"
@@ -384,10 +385,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
   return d_tr_trie.get();
 }
 
-quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
-{
-  return d_private->d_bint.get();
-}
 quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const
 {
   return d_private->d_synth_e.get();
@@ -445,19 +442,66 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
   return mo==m || mo==NULL;
 }
 
-bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
-  if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){
+bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
+{
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi && bi->isBound(q, v))
+  {
     return true;
-  }else{
-    TypeNode tn = v.getType();
-    if( tn.isSort() && options::finiteModelFind() ){
-      return true;
-    }
-    else if (d_term_enum->mayComplete(tn))
+  }
+  TypeNode tn = v.getType();
+  if (tn.isSort() && options::finiteModelFind())
+  {
+    return true;
+  }
+  else if (d_term_enum->mayComplete(tn))
+  {
+    return true;
+  }
+  return false;
+}
+
+BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
+{
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi)
+  {
+    return bi->getBoundVarType(q, v);
+  }
+  return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
+}
+
+void QuantifiersEngine::getBoundVarIndices(Node q,
+                                           std::vector<unsigned>& indices) const
+{
+  Assert(indices.empty());
+  // we take the bounded variables first
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi)
+  {
+    bi->getBoundVarIndices(q, indices);
+  }
+  // then get the remaining ones
+  for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+  {
+    if (std::find(indices.begin(), indices.end(), i) == indices.end())
     {
-      return true;
+      indices.push_back(i);
     }
   }
+}
+
+bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
+                                         bool initial,
+                                         Node q,
+                                         Node v,
+                                         std::vector<Node>& elements) const
+{
+  quantifiers::BoundedIntegers* bi = d_private->d_bint.get();
+  if (bi)
+  {
+    return bi->getBoundElements(rsi, initial, q, v, elements);
+  }
   return false;
 }
 
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 */
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