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.

6 files changed, 37 insertions, 16 deletions

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() ){