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.

28 files changed, 233 insertions, 64 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index c539bfdb0..037cb74d7 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -49,8 +49,9 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
 
 InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
                                      QuantifiersState& qs,
-                                     QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                                     QuantifiersInferenceManager& qim,
+                                     QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
@@ -309,11 +310,12 @@ bool InstStrategyCegqi::checkCompleteFor(Node q)
 
 void InstStrategyCegqi::checkOwnership(Node q)
 {
-  if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
+  if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
+  {
     if (d_do_cbqi[q] == CEG_HANDLED)
     {
       //take full ownership of the quantified formula
-      d_quantEngine->setOwner( q, this );
+      d_qreg.setOwner(q, this);
     }
   }
 }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index d4b78d306..a6a3c36cd 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -71,7 +71,8 @@ class InstStrategyCegqi : public QuantifiersModule
  public:
   InstStrategyCegqi(QuantifiersEngine* qe,
                     QuantifiersState& qs,
-                    QuantifiersInferenceManager& qim);
+                    QuantifiersInferenceManager& qim,
+                    QuantifiersRegistry& qr);
   ~InstStrategyCegqi();
 
   /** whether to do counterexample-guided instantiation for quantifier q */
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index db8bc90d1..83a102633 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -86,8 +86,9 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
 
 ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
                                          QuantifiersState& qs,
-                                         QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                                         QuantifiersInferenceManager& qim,
+                                         QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_notify(*this),
       d_uequalityEngine(
           d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index c73abd19b..644461da2 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -438,7 +438,8 @@ private:  //information about ground equivalence classes
  public:
   ConjectureGenerator(QuantifiersEngine* qe,
                       QuantifiersState& qs,
-                      QuantifiersInferenceManager& qim);
+                      QuantifiersInferenceManager& qim,
+                      QuantifiersRegistry& qr);
   ~ConjectureGenerator();
 
   /* needs check */
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 69c33d329..96b3bd0b0 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -35,8 +35,9 @@ namespace quantifiers {
 
 InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
                                          QuantifiersState& qs,
-                                         QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                                         QuantifiersInferenceManager& qim,
+                                         QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),
@@ -210,7 +211,7 @@ void InstantiationEngine::checkOwnership(Node q)
       }
     }
     if( hasPat ){
-      d_quantEngine->setOwner( q, this, 1 );
+      d_qreg.setOwner(q, this, 1);
     }
   }
 }
@@ -260,7 +261,7 @@ void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
 
 bool InstantiationEngine::shouldProcess(Node q)
 {
-  if (!d_quantEngine->hasOwnership(q, this))
+  if (!d_qreg.hasOwnership(q, this))
   {
     return false;
   }
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index f5b999cea..016784152 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -50,7 +50,8 @@ class InstantiationEngine : public QuantifiersModule {
  public:
   InstantiationEngine(QuantifiersEngine* qe,
                       QuantifiersState& qs,
-                      QuantifiersInferenceManager& qim);
+                      QuantifiersInferenceManager& qim,
+                      QuantifiersRegistry& qr);
   ~InstantiationEngine();
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
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:
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index c0f294528..f22e67815 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -35,8 +35,9 @@ namespace quantifiers {
 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
                                    QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
+                                   QuantifiersRegistry& qr,
                                    RelevantDomain* rd)
-    : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1)
+    : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
 void InstStrategyEnum::presolve()
@@ -130,7 +131,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
       for (unsigned i = 0; i < nquant; i++)
       {
         Node q = fm->getAssertedQuantifier(i, true);
-        bool doProcess = d_quantEngine->hasOwnership(q, this)
+        bool doProcess = d_qreg.hasOwnership(q, this)
                          && fm->isQuantifierActive(q)
                          && alreadyProc.find(q) == alreadyProc.end();
         if (doProcess)
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 5687624db..35c43d740 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -65,6 +65,7 @@ class InstStrategyEnum : public QuantifiersModule
   InstStrategyEnum(QuantifiersEngine* qe,
                    QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
+                   QuantifiersRegistry& qr,
                    RelevantDomain* rd);
   ~InstStrategyEnum() {}
   /** Presolve */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c025dc29e..433de2f85 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1840,8 +1840,9 @@ bool MatchGen::isHandled( TNode n ) {
 
 QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
                                      QuantifiersState& qs,
-                                     QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                                     QuantifiersInferenceManager& qim,
+                                     QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_conflict(qs.getSatContext(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
@@ -1852,7 +1853,8 @@ QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
 //-------------------------------------------------- registration
 
 void QuantConflictFind::registerQuantifier( Node q ) {
-  if( d_quantEngine->hasOwnership( q, this ) ){
+  if (d_qreg.hasOwnership(q, this))
+  {
     d_quants.push_back( q );
     d_quant_id[q] = d_quants.size();
     if( Trace.isOn("qcf-qregister") ){
@@ -2022,7 +2024,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
     for (unsigned i = 0; i < nquant; i++)
     {
       Node q = fm->getAssertedQuantifier(i, true);
-      if (d_quantEngine->hasOwnership(q, this)
+      if (d_qreg.hasOwnership(q, this)
           && d_irr_quant.find(q) == d_irr_quant.end()
           && fm->isQuantifierActive(q))
       {
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 15b3d119a..5ffe4426a 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -234,7 +234,8 @@ private:  //for equivalence classes
  public:
   QuantConflictFind(QuantifiersEngine* qe,
                     QuantifiersState& qs,
-                    QuantifiersInferenceManager& qim);
+                    QuantifiersInferenceManager& qim,
+                    QuantifiersRegistry& qr);
 
   /** register quantifier */
   void registerQuantifier(Node q) override;
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index ad65c06cd..a1dc5acf3 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -27,8 +27,9 @@ using namespace CVC4::theory::quantifiers;
 
 QuantDSplit::QuantDSplit(QuantifiersEngine* qe,
                          QuantifiersState& qs,
-                         QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe), d_added_split(qs.getUserContext())
+                         QuantifiersInferenceManager& qim,
+                         QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe), d_added_split(qs.getUserContext())
 {
 }
 
@@ -100,7 +101,7 @@ void QuantDSplit::checkOwnership(Node q)
   if (takeOwnership)
   {
     Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
-    d_quantEngine->setOwner( q, this );
+    d_qreg.setOwner(q, this);
   }
   // Notice we may not take ownership in some cases, meaning that both the
   // original quantified formula and the split one are generated. This may
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 76ac1a974..8fb9b4eb6 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -51,7 +51,8 @@ class QuantDSplit : public QuantifiersModule {
  public:
   QuantDSplit(QuantifiersEngine* qe,
               QuantifiersState& qs,
-              QuantifiersInferenceManager& qim);
+              QuantifiersInferenceManager& qim,
+              QuantifiersRegistry& qr);
   /** determine whether this quantified formula will be reduced */
   void checkOwnership(Node q) override;
   /* whether this module needs to check this round */
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 6ce46ad99..db643d96b 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -26,8 +26,9 @@ namespace theory {
 QuantifiersModule::QuantifiersModule(
     quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersInferenceManager& qim,
+    quantifiers::QuantifiersRegistry& qr,
     QuantifiersEngine* qe)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
 {
 }
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 417e6820d..9037e94fa 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -61,6 +62,7 @@ class QuantifiersModule {
  public:
   QuantifiersModule(quantifiers::QuantifiersState& qs,
                     quantifiers::QuantifiersInferenceManager& qim,
+                    quantifiers::QuantifiersRegistry& qr,
                     QuantifiersEngine* qe);
   virtual ~QuantifiersModule(){}
   /** Presolve.
@@ -168,6 +170,8 @@ class QuantifiersModule {
   quantifiers::QuantifiersState& d_qstate;
   /** The quantifiers inference manager */
   quantifiers::QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry& d_qreg;
 };/* class QuantifiersModule */
 
 /** Quantifiers utility
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 15715152b..ad5d5dba7 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -18,7 +18,6 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -34,11 +33,8 @@ bool QAttributes::isStandard() const
          && !d_isInternal;
 }
 
-QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : 
-d_quantEngine(qe) {
+QuantAttributes::QuantAttributes() {}
 
-}  
-  
 void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
   Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
   if (attr == "fun-def")
@@ -182,8 +178,6 @@ void QuantAttributes::computeAttributes( Node q ) {
     }
     d_fun_defs[f] = true;
   }
-  // set ownership of quantified formula q based on the computed attributes
-  d_quantEngine->setOwner(q, qa);
 }
 
 void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 91a0d504f..740588b84 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -25,8 +25,6 @@
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-
 /** Attribute true for function definition quantifiers */
 struct FunDefAttributeId {};
 typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
@@ -176,8 +174,8 @@ struct QAttributes
 */
 class QuantAttributes
 {
-public:
-  QuantAttributes( QuantifiersEngine * qe );
+ public:
+  QuantAttributes();
   ~QuantAttributes(){}
   /** set user attribute
   * This function applies an attribute
@@ -238,8 +236,6 @@ public:
   static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
 
  private:
-  /** pointer to quantifiers engine */
-  QuantifiersEngine * d_quantEngine;
   /** cache of attributes */
   std::map< Node, QAttributes > d_qattr;
   /** function definitions */
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 573824b80..f1a05f401 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -40,49 +40,50 @@ QuantifiersModules::~QuantifiersModules() {}
 void QuantifiersModules::initialize(QuantifiersEngine* qe,
                                     QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
+                                    QuantifiersRegistry& qr,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
   if (options::quantConflictFind())
   {
-    d_qcf.reset(new QuantConflictFind(qe, qs, qim));
+    d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr));
     modules.push_back(d_qcf.get());
   }
   if (options::conjectureGen())
   {
-    d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim));
+    d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr));
     modules.push_back(d_sg_gen.get());
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
   {
-    d_inst_engine.reset(new InstantiationEngine(qe, qs, qim));
+    d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr));
     modules.push_back(d_inst_engine.get());
   }
   if (options::cegqi())
   {
-    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim));
+    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
     modules.push_back(d_i_cbqi.get());
     qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
   if (options::sygus())
   {
-    d_synth_e.reset(new SynthEngine(qe, qs, qim));
+    d_synth_e.reset(new SynthEngine(qe, qs, qim, qr));
     modules.push_back(d_synth_e.get());
   }
   // finite model finding
   if (options::fmfBound())
   {
-    d_bint.reset(new BoundedIntegers(qe, qs, qim));
+    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr));
     modules.push_back(d_bint.get());
   }
   if (options::finiteModelFind() || options::fmfBound())
   {
-    d_model_engine.reset(new ModelEngine(qe, qs, qim));
+    d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
-    d_qsplit.reset(new QuantDSplit(qe, qs, qim));
+    d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr));
     modules.push_back(d_qsplit.get());
   }
   if (options::quantAlphaEquiv())
@@ -93,12 +94,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
     d_rel_dom.reset(new RelevantDomain(qe));
-    d_fs.reset(new InstStrategyEnum(qe, qs, qim, d_rel_dom.get()));
+    d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
   if (options::sygusInst())
   {
-    d_sygus_inst.reset(new SygusInst(qe, qs, qim));
+    d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr));
     modules.push_back(d_sygus_inst.get());
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index ba48cc68b..08266c8fe 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -54,6 +54,7 @@ class QuantifiersModules
   void initialize(QuantifiersEngine* qe,
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
+                  QuantifiersRegistry& qr,
                   std::vector<QuantifiersModule*>& modules);
 
  private:
diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
new file mode 100644
index 000000000..1633382c8
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file quantifiers_registry.cpp
+ ** \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 The quantifiers registry
+ **/
+
+#include "theory/quantifiers/quantifiers_registry.h"
+
+#include "theory/quantifiers/quant_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
+{
+  std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
+  if (it == d_owner.end())
+  {
+    return nullptr;
+  }
+  return it->second;
+}
+
+void QuantifiersRegistry::setOwner(Node q,
+                                   QuantifiersModule* m,
+                                   int32_t priority)
+{
+  QuantifiersModule* mo = getOwner(q);
+  if (mo == m)
+  {
+    return;
+  }
+  if (mo != nullptr)
+  {
+    if (priority <= d_owner_priority[q])
+    {
+      Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
+                          << (m ? m->identify() : "null")
+                          << ", but already has owner " << mo->identify()
+                          << " with higher priority!" << std::endl;
+      return;
+    }
+  }
+  d_owner[q] = m;
+  d_owner_priority[q] = priority;
+}
+
+bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
+{
+  QuantifiersModule* mo = getOwner(q);
+  return mo == m || mo == nullptr;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
new file mode 100644
index 000000000..59db1dfe2
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file quantifiers_registry.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 The quantifiers registry
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersModule;
+
+namespace quantifiers {
+
+/**
+ * The quantifiers registry, which manages basic information about which
+ * quantifiers modules have ownership of quantified formulas.
+ */
+class QuantifiersRegistry
+{
+ public:
+  QuantifiersRegistry() {}
+  ~QuantifiersRegistry() {}
+  /** get the owner of quantified formula q */
+  QuantifiersModule* getOwner(Node q) const;
+  /**
+   * Set owner of quantified formula q to module m with given priority. If
+   * the quantified formula has previously been assigned an owner with
+   * lower priority, that owner is overwritten.
+   */
+  void setOwner(Node q, QuantifiersModule* m, int32_t priority = 0);
+  /**
+   * Return true if module q has no owner registered or if its registered owner is m.
+   */
+  bool hasOwnership(Node q, QuantifiersModule* m) const;
+
+ private:
+  /**
+   * Maps quantified formulas to the module that owns them, if any module has
+   * specifically taken ownership of it.
+   */
+  std::map<Node, QuantifiersModule*> d_owner;
+  /**
+   * The priority value associated with the ownership of quantified formulas
+   * in the domain of the above map, where higher values take higher
+   * precendence.
+   */
+  std::map<Node, int32_t> d_owner_priority;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 4b35bc545..869d22737 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -31,8 +31,9 @@ namespace quantifiers {
 
 SynthEngine::SynthEngine(QuantifiersEngine* qe,
                          QuantifiersState& qs,
-                         QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                         QuantifiersInferenceManager& qim,
+                         QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_tds(qe->getTermDatabaseSygus()),
       d_conj(nullptr),
       d_sqp(qe)
@@ -164,11 +165,22 @@ void SynthEngine::assignConjecture(Node q)
   d_conjs.back()->assign(q);
 }
 
+void SynthEngine::checkOwnership(Node q)
+{
+  // take ownership of quantified formulas with sygus attribute, and function
+  // definitions when options::sygusRecFun is true.
+  QuantAttributes* qa = d_quantEngine->getQuantAttributes();
+  if (qa->isSygus(q) || (options::sygusRecFun() && qa->isFunDef(q)))
+  {
+    d_qreg.setOwner(q, this, 2);
+  }
+}
+
 void SynthEngine::registerQuantifier(Node q)
 {
   Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
                        << std::endl;
-  if (d_quantEngine->getOwner(q) != this)
+  if (d_qreg.getOwner(q) != this)
   {
     return;
   }
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 63175cf0c..4cb73d450 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -35,7 +35,8 @@ class SynthEngine : public QuantifiersModule
  public:
   SynthEngine(QuantifiersEngine* qe,
               QuantifiersState& qs,
-              QuantifiersInferenceManager& qim);
+              QuantifiersInferenceManager& qim,
+              QuantifiersRegistry& qr);
   ~SynthEngine();
   /** presolve
    *
@@ -49,6 +50,8 @@ class SynthEngine : public QuantifiersModule
   QEffort needsModel(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
+  /** check ownership */
+  void checkOwnership(Node q) override;
   /* Called for new quantifiers */
   void registerQuantifier(Node q) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 66c9cbf79..69836feba 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -181,8 +181,9 @@ void addSpecialValues(
 
 SygusInst::SygusInst(QuantifiersEngine* qe,
                      QuantifiersState& qs,
-                     QuantifiersInferenceManager& qim)
-    : QuantifiersModule(qs, qim, qe),
+                     QuantifiersInferenceManager& qim,
+                     QuantifiersRegistry& qr)
+    : QuantifiersModule(qs, qim, qr, qe),
       d_ce_lemma_added(qs.getUserContext()),
       d_global_terms(qs.getUserContext()),
       d_notified_assertions(qs.getUserContext())
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 4820398be..123ec1f5e 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -64,7 +64,8 @@ class SygusInst : public QuantifiersModule
  public:
   SygusInst(QuantifiersEngine* qe,
             QuantifiersState& qs,
-            QuantifiersInferenceManager& qim);
+            QuantifiersInferenceManager& qim,
+            QuantifiersRegistry& qr);
   ~SygusInst() = default;
 
   bool needsCheck(Theory::Effort e) override;