Introduce quantifiers registry utility (#5829)

This is a simple module for determining which quantifiers module has ownership of quantified formulas.

This is work towards eliminating dependencies of quantifiers modules.

Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.

4 files changed, 16 insertions, 9 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 9144bca2a..a6862f513 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -86,8 +86,9 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
 
 BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
-                                 QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe)
+                                 QuantifiersInferenceManager& qim,
+                                 QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe)
 {
 }
 
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 685c07d82..74ff8a19b 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -163,7 +163,8 @@ private:
  public:
   BoundedIntegers(QuantifiersEngine* qe,
                   QuantifiersState& qs,
-                  QuantifiersInferenceManager& qim);
+                  QuantifiersInferenceManager& qim,
+                  QuantifiersRegistry& qr);
   virtual ~BoundedIntegers();
 
   void presolve() override;
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 715002f7b..618a72047 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -35,8 +35,9 @@ using namespace CVC4::theory::inst;
 //Model Engine constructor
 ModelEngine::ModelEngine(QuantifiersEngine* qe,
                          QuantifiersState& qs,
-                         QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                         QuantifiersInferenceManager& qim,
+                         QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_incomplete_check(true),
       d_addedLemmas(0),
       d_triedLemmas(0),
@@ -187,7 +188,8 @@ int ModelEngine::checkModel(){
   if( Trace.isOn("model-engine") ){
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
-      if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){
+      if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this))
+      {
         int totalInst = 1;
         for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
           TypeNode tn = f[0][j].getType();
@@ -213,7 +215,8 @@ int ModelEngine::checkModel(){
       Node q = fm->getAssertedQuantifier( i, true );
       Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
-      if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){
+      if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this))
+      {
         exhaustiveInstantiate( q, e );
         if (d_qstate.isInConflict())
         {
@@ -318,7 +321,8 @@ void ModelEngine::debugPrint( const char* c ){
   Trace( c ) << "Quantifiers: " << std::endl;
   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-    if( d_quantEngine->hasOwnership( q, this ) ){
+    if (d_qreg.hasOwnership(q, this))
+    {
       Trace( c ) << "   ";
       if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){
         Trace( c ) << "*Inactive* ";
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 3e212b319..1cb780dd0 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -45,7 +45,8 @@ private:
 public:
  ModelEngine(QuantifiersEngine* qe,
              QuantifiersState& qs,
-             QuantifiersInferenceManager& qim);
+             QuantifiersInferenceManager& qim,
+             QuantifiersRegistry& qr);
  virtual ~ModelEngine();
 
 public: