Move utilities for inferred bounds on quantifers to own class (#6159)

This also moves some methods from TermEnumeration to QuantifiersBoundInference.

This is required for breaking several cyclic dependencies within quantifiers.

20 files changed, 360 insertions, 205 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e8dd5d0aa..5ceb44615 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -735,6 +735,8 @@ libcvc4_add_sources(
   theory/quantifiers/lazy_trie.h
   theory/quantifiers/proof_checker.cpp
   theory/quantifiers/proof_checker.h
+  theory/quantifiers/quant_bound_inference.cpp
+  theory/quantifiers/quant_bound_inference.h
   theory/quantifiers/quant_conflict_find.cpp
   theory/quantifiers/quant_conflict_find.h
   theory/quantifiers/quant_relevance.cpp
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 98f440894..44c42b305 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -129,7 +129,7 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
   else
   {
     // can we complete it?
-    if (d_qe->getTermEnumeration()->mayComplete(tn))
+    if (d_qreg.getQuantifiersBoundInference().mayComplete(tn))
     {
       Trace("fm-debug") << "  do complete, since cardinality is small ("
                         << tn.getCardinality() << ")..." << std::endl;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 99aca6408..0a035a691 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -416,7 +416,7 @@ void BoundedIntegers::checkOwnership(Node f)
         if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
           TypeNode tn = f[0][i].getType();
           if ((tn.isSort() && tn.isInterpretedFinite())
-              || d_quantEngine->getTermEnumeration()->mayComplete(tn))
+              || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
           {
             success = true;
             setBoundedVar( f, f[0][i], BOUND_FINITE );
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 46c27df3d..abcd5a794 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -18,8 +18,11 @@
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_rep_bound_ext.h"
+#include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -281,8 +284,10 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
   }
 }
 
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs)
-    : QModelBuilder(qe, qs)
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe,
+                                   QuantifiersState& qs,
+                                   QuantifiersRegistry& qr)
+    : QModelBuilder(qe, qs, qr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -785,8 +790,10 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
 class RepBoundFmcEntry : public QRepBoundExt
 {
  public:
-  RepBoundFmcEntry(QuantifiersEngine* qe, Node e, FirstOrderModelFmc* f)
-      : QRepBoundExt(qe), d_entry(e), d_fm(f)
+  RepBoundFmcEntry(QuantifiersBoundInference& qbi,
+                   Node e,
+                   FirstOrderModelFmc* f)
+      : QRepBoundExt(qbi, f), d_entry(e), d_fm(f)
   {
   }
   ~RepBoundFmcEntry() {}
@@ -818,8 +825,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
   Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
-  RepBoundFmcEntry rbfe(d_qe, c, fm);
-  RepSetIterator riter(d_qe->getModel()->getRepSet(), &rbfe);
+  QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
+  RepBoundFmcEntry rbfe(qbi, c, fm);
+  RepSetIterator riter(fm->getRepSet(), &rbfe);
   Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
   //initialize
   if (riter.setQuantifier(f))
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 6cad3fff5..b3c55ee7a 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -154,7 +154,9 @@ protected:
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 
  public:
-  FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs);
+  FullModelChecker(QuantifiersEngine* qe,
+                   QuantifiersState& qs,
+                   QuantifiersRegistry& qr);
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 878b4ddd3..89e4fa29d 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,12 +30,15 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs)
+QModelBuilder::QModelBuilder(QuantifiersEngine* qe,
+                             QuantifiersState& qs,
+                             QuantifiersRegistry& qr)
     : TheoryEngineModelBuilder(),
       d_qe(qe),
       d_addedLemmas(0),
       d_triedLemmas(0),
-      d_qstate(qs)
+      d_qstate(qs),
+      d_qreg(qr)
 {
 }
 
@@ -94,14 +97,15 @@ void QModelBuilder::debugModel( TheoryModel* m ){
     Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
+    QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
       std::vector< Node > vars;
       for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
         vars.push_back( f[0][j] );
       }
-      QRepBoundExt qrbe(d_qe);
-      RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
+      QRepBoundExt qrbe(qbi, fm);
+      RepSetIterator riter(fm->getRepSet(), &qrbe);
       if( riter.setQuantifier( f ) ){
         while( !riter.isFinished() ){
           tests++;
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 578554d79..534226a7c 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -27,6 +27,7 @@ namespace quantifiers {
 
 class FirstOrderModel;
 class QuantifiersState;
+class QuantifiersRegistry;
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {
@@ -41,7 +42,9 @@ class QModelBuilder : public TheoryEngineModelBuilder
   unsigned d_triedLemmas;
 
  public:
-  QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs);
+  QModelBuilder(QuantifiersEngine* qe,
+                QuantifiersState& qs,
+                QuantifiersRegistry& qr);
 
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
@@ -61,6 +64,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
  protected:
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
+  /** Reference to the quantifiers registry */
+  QuantifiersRegistry& d_qreg;
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 6cfb31c53..257926737 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -251,7 +251,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
   unsigned prev_alem = mb->getNumAddedLemmas();
   unsigned prev_tlem = mb->getNumTriedLemmas();
-  int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
+  FirstOrderModel* fm = d_quantEngine->getModel();
+  int retEi = mb->doExhaustiveInstantiation(fm, f, effort);
   if( retEi!=0 ){
     if( retEi<0 ){
       Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
@@ -270,9 +271,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       }
       Trace("fmf-exh-inst-debug") << std::endl;
     }
+    QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
-    QRepBoundExt qrbe(d_quantEngine);
-    RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe);
+    QRepBoundExt qrbe(qbi, fm);
+    RepSetIterator riter(fm->getRepSet(), &qrbe);
     if( riter.setQuantifier( f ) ){
       Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
       if( !riter.isIncomplete() ){
diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp
new file mode 100644
index 000000000..45c2b5e42
--- /dev/null
+++ b/src/theory/quantifiers/quant_bound_inference.cpp
@@ -0,0 +1,130 @@
+/*********************                                                        */
+/*! \file quant_bound_inference.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 bound inference
+ **/
+
+#include "theory/quantifiers/quant_bound_inference.h"
+
+#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
+                                                     bool isFmf)
+    : d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
+{
+}
+
+void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }
+
+bool QuantifiersBoundInference::mayComplete(TypeNode tn)
+{
+  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
+      d_may_complete.find(tn);
+  if (it == d_may_complete.end())
+  {
+    // cache
+    bool mc = mayComplete(tn, d_cardMax);
+    d_may_complete[tn] = mc;
+    return mc;
+  }
+  return it->second;
+}
+
+bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
+{
+  bool mc = false;
+  if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
+  {
+    Cardinality c = tn.getCardinality();
+    if (!c.isLargeFinite())
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+      // check if less than fixed upper bound
+      Node oth = nm->mkConst(Rational(maxCard));
+      Node eq = nm->mkNode(LEQ, card, oth);
+      eq = Rewriter::rewrite(eq);
+      mc = eq.isConst() && eq.getConst<bool>();
+    }
+  }
+  return mc;
+}
+
+bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
+{
+  if (d_bint && d_bint->isBound(q, v))
+  {
+    return true;
+  }
+  TypeNode tn = v.getType();
+  if (tn.isSort() && d_isFmf)
+  {
+    return true;
+  }
+  else if (mayComplete(tn))
+  {
+    return true;
+  }
+  return false;
+}
+
+BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
+{
+  if (d_bint)
+  {
+    return d_bint->getBoundVarType(q, v);
+  }
+  return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
+}
+
+void QuantifiersBoundInference::getBoundVarIndices(
+    Node q, std::vector<unsigned>& indices) const
+{
+  Assert(indices.empty());
+  // we take the bounded variables first
+  if (d_bint)
+  {
+    d_bint->getBoundVarIndices(q, indices);
+  }
+  // then get the remaining ones
+  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+  {
+    if (std::find(indices.begin(), indices.end(), i) == indices.end())
+    {
+      indices.push_back(i);
+    }
+  }
+}
+
+bool QuantifiersBoundInference::getBoundElements(
+    RepSetIterator* rsi,
+    bool initial,
+    Node q,
+    Node v,
+    std::vector<Node>& elements) const
+{
+  if (d_bint)
+  {
+    return d_bint->getBoundElements(rsi, initial, q, v, elements);
+  }
+  return false;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h
new file mode 100644
index 000000000..58b4e3db9
--- /dev/null
+++ b/src/theory/quantifiers/quant_bound_inference.h
@@ -0,0 +1,127 @@
+/*********************                                                        */
+/*! \file quant_bound_inference.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 bound inference
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+class RepSetIterator;
+
+namespace quantifiers {
+
+class BoundedIntegers;
+
+/** 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
+};
+
+/**
+ * This class is the central utility for determining if the domain of a
+ * quantified formula is finite, or whether its domain can be restricted to
+ * a finite subdomain based on one of the above types.
+ */
+class QuantifiersBoundInference
+{
+ public:
+  /**
+   * @param cardMax The maximum cardinality we consider to be small enough
+   * to "complete" below.
+   * @param isFmf Whether finite model finding (for uninterpreted sorts) is
+   * enabled.
+   */
+  QuantifiersBoundInference(unsigned cardMax, bool isFmf = false);
+  /** finish initialize */
+  void finishInit(BoundedIntegers* b);
+  /** may complete type
+   *
+   * Returns true if the type tn is closed enumerable, is interpreted as a
+   * finite type, and has cardinality less than some reasonable value
+   * (currently < 1000). This method caches the results of whether each type
+   * may be completed.
+   */
+  bool mayComplete(TypeNode tn);
+  /**
+   * Static version of the above method where maximum cardinality is
+   * configurable.
+   */
+  static bool mayComplete(TypeNode tn, unsigned cardMax);
+  /** does variable v of quantified formula q have a finite bound? */
+  bool isFiniteBound(Node q, Node v);
+  /** 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);
+  /**
+   * 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;
+
+ private:
+  /** The maximum cardinality for which we complete */
+  unsigned d_cardMax;
+  /** Whether finite model finding is enabled */
+  bool d_isFmf;
+  /** may complete */
+  std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
+  /** The bounded integers module, which may help infer bounds */
+  BoundedIntegers* d_bint;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp
index 70ac2ddfa..b26a5bfa2 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.cpp
+++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp
@@ -14,8 +14,9 @@
 
 #include "theory/quantifiers/quant_rep_bound_ext.h"
 
-#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quant_bound_inference.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
@@ -23,7 +24,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-QRepBoundExt::QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
+QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m)
+    : d_qbi(qbi), d_model(m)
+{
+}
 
 RsiEnumType QRepBoundExt::setBound(Node owner,
                                    unsigned i,
@@ -32,7 +36,7 @@ RsiEnumType QRepBoundExt::setBound(Node owner,
   // builtin: check if it is bound by bounded integer module
   if (owner.getKind() == FORALL)
   {
-    BoundVarType bvt = d_qe->getBoundVarType(owner, owner[0][i]);
+    BoundVarType bvt = d_qbi.getBoundVarType(owner, owner[0][i]);
     if (bvt != BOUND_FINITE)
     {
       d_bound_int[i] = true;
@@ -57,7 +61,7 @@ bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
     return true;
   }
   Assert(owner.getKind() == FORALL);
-  if (!d_qe->getBoundElements(rsi, initial, owner, owner[0][i], elements))
+  if (!d_qbi.getBoundElements(rsi, initial, owner, owner[0][i], elements))
   {
     return false;
   }
@@ -66,7 +70,7 @@ bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
 
 bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
 {
-  return d_qe->getModel()->initializeRepresentativesForType(tn);
+  return d_model->initializeRepresentativesForType(tn);
 }
 
 bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
@@ -77,7 +81,7 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
     return false;
   }
   Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
-  d_qe->getBoundVarIndices(owner, varOrder);
+  d_qbi.getBoundVarIndices(owner, varOrder);
   return true;
 }
 
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h
index ed636c1b2..30dbd520b 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.h
+++ b/src/theory/quantifiers/quant_rep_bound_ext.h
@@ -20,17 +20,16 @@
 #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 {
 
+class QuantifiersBoundInference;
+class FirstOrderModel;
+
 /** Quantifiers representative bound
  *
  * This class is used for computing (finite) bounds for the domain of a
@@ -40,7 +39,7 @@ namespace quantifiers {
 class QRepBoundExt : public RepBoundExt
 {
  public:
-  QRepBoundExt(QuantifiersEngine* qe);
+  QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m);
   virtual ~QRepBoundExt() {}
   /** set bound */
   RsiEnumType setBound(Node owner,
@@ -58,8 +57,10 @@ class QRepBoundExt : public RepBoundExt
   bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
 
  private:
-  /** Quantifiers engine associated with this bound */
-  QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers bound inference */
+  QuantifiersBoundInference& d_qbi;
+  /** Pointer to the quantifiers model */
+  FirstOrderModel* d_model;
   /** indices that are bound integer enumeration */
   std::map<unsigned, bool> d_bound_int;
 };
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 269a51625..55f3469d2 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,6 +48,7 @@ void QuantDSplit::checkOwnership(Node q)
   }
   bool takeOwnership = false;
   bool doSplit = false;
+  QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
   Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
@@ -67,7 +68,7 @@ void QuantDSplit::checkOwnership(Node q)
         else if (options::quantDynamicSplit()
                  == options::QuantDSplitMode::DEFAULT)
         {
-          if (!d_quantEngine->isFiniteBound(q, q[0][i]))
+          if (!qbi.isFiniteBound(q, q[0][i]))
           {
             if (dt.isInterpretedFinite(tn))
             {
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 714a0f467..d536fa84d 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -77,24 +77,6 @@ public:
   static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 };
 
-/** 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/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index 76e2b3078..daaaea0ad 100644
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/quantifiers_registry.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/term_util.h"
 
@@ -21,7 +22,12 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-QuantifiersRegistry::QuantifiersRegistry() : d_quantAttr() {}
+QuantifiersRegistry::QuantifiersRegistry()
+    : d_quantAttr(),
+      d_quantBoundInf(options::fmfTypeCompletionThresh(),
+                      options::finiteModelFind())
+{
+}
 
 void QuantifiersRegistry::registerQuantifier(Node q)
 {
@@ -177,6 +183,12 @@ QuantAttributes& QuantifiersRegistry::getQuantAttributes()
 {
   return d_quantAttr;
 }
+
+QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
+{
+  return d_quantBoundInf;
+}
+
 Node QuantifiersRegistry::getNameForQuant(Node q) const
 {
   Node name = d_quantAttr.getQuantName(q);
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index fb1643765..f2d3f085e 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
 
 #include "expr/node.h"
+#include "theory/quantifiers/quant_bound_inference.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 
@@ -87,6 +88,8 @@ class QuantifiersRegistry : public QuantifiersUtil
   //----------------------------- end instantiation constants
   /** Get quantifiers attributes utility class */
   QuantAttributes& getQuantAttributes();
+  /** Get quantifiers bound inference utility */
+  QuantifiersBoundInference& getQuantifiersBoundInference();
   /**
    * Get quantifiers name, which returns a variable corresponding to the name of
    * quantified formula q if q has a name, or otherwise returns q itself.
@@ -120,6 +123,8 @@ class QuantifiersRegistry : public QuantifiersUtil
   std::map<Node, std::vector<Node> > d_inst_constants;
   /** The quantifiers attributes class */
   QuantAttributes d_quantAttr;
+  /** The quantifiers bound inference class */
+  QuantifiersBoundInference d_quantBoundInf;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
index 1a066a886..0b1b1cdae 100644
--- a/src/theory/quantifiers/term_enumeration.cpp
+++ b/src/theory/quantifiers/term_enumeration.cpp
@@ -14,9 +14,7 @@
 
 #include "theory/quantifiers/term_enumeration.h"
 
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
+#include "theory/quantifiers/quant_bound_inference.h"
 
 using namespace CVC4::kind;
 
@@ -24,6 +22,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+TermEnumeration::TermEnumeration(QuantifiersBoundInference* qbi) : d_qbi(qbi) {}
+
 Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
 {
   Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
@@ -53,43 +53,9 @@ Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
   return d_enum_terms[tn][index];
 }
 
-bool TermEnumeration::mayComplete(TypeNode tn)
-{
-  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
-      d_may_complete.find(tn);
-  if (it == d_may_complete.end())
-  {
-    // cache
-    bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
-    d_may_complete[tn] = mc;
-    return mc;
-  }
-  return it->second;
-}
-
-bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
-{
-  bool mc = false;
-  if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
-  {
-    Cardinality c = tn.getCardinality();
-    if (!c.isLargeFinite())
-    {
-      NodeManager* nm = NodeManager::currentNM();
-      Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
-      // check if less than fixed upper bound
-      Node oth = nm->mkConst(Rational(maxCard));
-      Node eq = nm->mkNode(LEQ, card, oth);
-      eq = Rewriter::rewrite(eq);
-      mc = eq.isConst() && eq.getConst<bool>();
-    }
-  }
-  return mc;
-}
-
 bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom)
 {
-  if (!mayComplete(tn))
+  if (!d_qbi || !d_qbi->mayComplete(tn))
   {
     return false;
   }
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h
index fcad50f05..9cd57bfd0 100644
--- a/src/theory/quantifiers/term_enumeration.h
+++ b/src/theory/quantifiers/term_enumeration.h
@@ -28,6 +28,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class QuantifiersBoundInference;
+
 /** Term enumeration
  *
  * This class has utilities for enumerating terms. It stores
@@ -38,33 +40,26 @@ namespace quantifiers {
 class TermEnumeration
 {
  public:
-  TermEnumeration() {}
+  TermEnumeration(QuantifiersBoundInference* qbi = nullptr);
   ~TermEnumeration() {}
   /** get i^th term for type tn */
   Node getEnumerateTerm(TypeNode tn, unsigned i);
-  /** may complete type
-   *
-   * Returns true if the type tn is closed enumerable, is interpreted as a
-   * finite type, and has cardinality less than some reasonable value
-   * (currently < 1000). This method caches the results of whether each type
-   * may be completed.
-   */
-  bool mayComplete(TypeNode tn);
-  /**
-   * Static version of the above method where maximum cardinality is
-   * configurable.
-   */
-  static bool mayComplete(TypeNode tn, unsigned cardMax);
 
   /** get domain
    *
-   * If tn is a type such that mayComplete(tn) returns true, this method
+   * If tn is a type such that d_qbi.mayComplete(tn) returns true, this method
    * adds all domain elements of tn to dom and returns true. Otherwise, this
    * method returns false.
    */
   bool getDomain(TypeNode tn, std::vector<Node>& dom);
 
  private:
+  /**
+   * Reference to quantifiers bound inference, which determines when it is
+   * possible to enumerate the entire domain of a type. If this is not provided,
+   * getDomain above always returns false.
+   */
+  QuantifiersBoundInference* d_qbi;
   /** ground terms enumerated for types */
   std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
       d_enum_terms;
@@ -72,10 +67,6 @@ class TermEnumeration
   std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
   /** type enumerators */
   std::vector<TypeEnumerator> d_typ_enum;
-  /** closed enumerable type cache */
-  std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_typ_closed_enum;
-  /** may complete */
-  std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c41fa36e6..1784b976e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -93,13 +93,14 @@ QuantifiersEngine::QuantifiersEngine(
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
-          this, qstate, d_qreg, "FirstOrderModelFmc"));
-      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
+          this, qstate, qr, "FirstOrderModelFmc"));
+      d_builder.reset(
+          new quantifiers::fmcheck::FullModelChecker(this, qstate, qr));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_model.reset(new quantifiers::FirstOrderModel(
-          this, qstate, d_qreg, "FirstOrderModel"));
-      d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
+          this, qstate, qr, "FirstOrderModel"));
+      d_builder.reset(new quantifiers::QModelBuilder(this, qstate, qr));
     }
   }else{
     d_model.reset(new quantifiers::FirstOrderModel(
@@ -123,6 +124,12 @@ void QuantifiersEngine::finishInit(TheoryEngine* te, DecisionManager* dm)
   {
     d_util.push_back(d_qmodules->d_rel_dom.get());
   }
+
+  // handle any circular dependencies
+
+  // quantifiers bound inference needs to be informed of the bounded integers
+  // module, which has information about which quantifiers have finite bounds
+  d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
 }
 
 DecisionManager* QuantifiersEngine::getDecisionManager()
@@ -178,69 +185,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
   return d_tr_trie.get();
 }
 
-bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
-{
-  quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
-  if (bi && bi->isBound(q, v))
-  {
-    return true;
-  }
-  TypeNode tn = v.getType();
-  if (tn.isSort() && options::finiteModelFind())
-  {
-    return true;
-  }
-  else if (d_treg.getTermEnumeration()->mayComplete(tn))
-  {
-    return true;
-  }
-  return false;
-}
-
-BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
-{
-  quantifiers::BoundedIntegers* bi = d_qmodules->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_qmodules->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())
-    {
-      indices.push_back(i);
-    }
-  }
-}
-
-bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
-                                         bool initial,
-                                         Node q,
-                                         Node v,
-                                         std::vector<Node>& elements) const
-{
-  quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
-  if (bi)
-  {
-    return bi->getBoundElements(rsi, initial, q, v, elements);
-  }
-  return false;
-}
-
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
   d_qim.clearPending();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index c7c716105..92b90c375 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -111,37 +111,6 @@ class QuantifiersEngine {
    */
   void finishInit(TheoryEngine* te, DecisionManager* dm);
   //---------------------- end private initialization
- 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 */