Pass term registry to quantifiers modules (#6216)

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 9a952601dac49a1a5cc02d98a029c54631828847..f553e27f27b39f75db4ee3166c13ec1685b80381 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -32,6 +32,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index d3bc788cdcd4b81334a75aee63796d37a61f0a27..ca9599ba37cbc7a5ba0f1517f80689d9c4a9d387 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -26,7 +26,7 @@
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 2c0fba7a62f71f2d2b3191b859b8946674fe07c3..99df6cf13756494c0f4be24bff37a1c28f8bd941 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
@@ -52,8 +53,9 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
 InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
                                      QuantifiersState& qs,
                                      QuantifiersInferenceManager& qim,
-                                     QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe),
+                                     QuantifiersRegistry& qr,
+                                     TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe),
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
@@ -84,10 +86,10 @@ bool InstStrategyCegqi::needsCheck(Theory::Effort e)
 
 QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e)
 {
-  size_t nquant = d_quantEngine->getModel()->getNumAssertedQuantifiers();
+  size_t nquant = d_treg.getModel()->getNumAssertedQuantifiers();
   for (size_t i = 0; i < nquant; i++)
   {
-    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    Node q = d_treg.getModel()->getAssertedQuantifier(i);
     if (doCbqi(q))
     {
       return QEFFORT_STANDARD;
@@ -193,11 +195,15 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
   d_incomplete_check = false;
   d_active_quant.clear();
   //check if any cbqi lemma has not been added yet
-  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  FirstOrderModel* fm = d_treg.getModel();
+  size_t nquant = fm->getNumAssertedQuantifiers();
+  for (size_t i = 0; i < nquant; i++)
+  {
+    Node q = fm->getAssertedQuantifier(i);
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
-      if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      if (fm->isQuantifierActive(q))
+      {
         d_active_quant[q] = true;
         Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
         Node cel = getCounterexampleLiteral(q);
@@ -211,7 +217,7 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
               Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
             }else{
               Trace("cegqi") << "Inactive : " << q << std::endl;
-              d_quantEngine->getModel()->setQuantifierActive( q, false );
+              fm->setQuantifierActive(q, false);
               d_cbqi_set_quant_inactive = true;
               d_active_quant.erase( q );
             }

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 92b9506e7851dc314860ca572b5bafc16d5514b2..6db7552463442b87c16afea7d1e9033387a4f74f 100644 (file)
--- 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
   InstStrategyCegqi(QuantifiersEngine* qe,
                     QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
-                    QuantifiersRegistry& qr);
+                    QuantifiersRegistry& qr,
+                    TermRegistry& tr);
   ~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 04ab464f8e8fca4c1ebf7b55c06622b6665c892d..d253fce23052e7e8ddc57214ad11a921d156169c 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
@@ -89,8 +88,9 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
 ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
                                          QuantifiersState& qs,
                                          QuantifiersInferenceManager& qim,
-                                         QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe),
+                                         QuantifiersRegistry& qr,
+                                         TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe),
       d_notify(*this),
       d_uequalityEngine(
           d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
@@ -318,7 +318,7 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
 }
 
 bool ConjectureGenerator::isHandledTerm( TNode n ){
-  return d_quantEngine->getTermDatabase()->isTermActive(n)
+  return getTermDatabase()->isTermActive(n)
          && inst::TriggerTermInfo::isAtomicTrigger(n)
          && (n.getKind() != APPLY_UF || n.getOperator().getKind() != SKOLEM);
 }
@@ -537,7 +537,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
       d_ue_canon.clear();
       d_thm_index.clear();
       std::vector< Node > provenConj;
-      quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
+      quantifiers::FirstOrderModel* m = d_treg.getModel();
       for( unsigned i=0; i<m->getNumAssertedQuantifiers(); i++ ){
         Node q = m->getAssertedQuantifier( i );
         Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
@@ -570,7 +570,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
                   {
                     isSubsume = true;
                     //set inactive (will be ignored by other modules)
-                    d_quantEngine->getModel()->setQuantifierActive( q, false );
+                    m->setQuantifierActive(q, false);
                   }
                   else
                   {
@@ -1103,7 +1103,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
   if( n.getNumChildren()>0 ){
     Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num
                               << ")" << std::endl;
-    TermEnumeration* te = d_quantEngine->getTermRegistry().getTermEnumeration();
+    TermEnumeration* te = d_treg.getTermEnumeration();
     // below, we do a fair enumeration of vectors vec of indices whose sum is
     // 1,2,3, ...
     std::vector< int > vec;

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index eaf7ff172bbe1046db0d3961a2f48d4a20818e11..6b4df3df8345c23875b2a9c28f52fa838d1f9ea7 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -439,7 +439,8 @@ private:  //information about ground equivalence classes
   ConjectureGenerator(QuantifiersEngine* qe,
                       QuantifiersState& qs,
                       QuantifiersInferenceManager& qim,
-                      QuantifiersRegistry& qr);
+                      QuantifiersRegistry& qr,
+                      TermRegistry& tr);
   ~ConjectureGenerator();
 
   /* needs check */

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 9153d928067a45425a0f0e5aeaea98a7f8bef46a..2298eb2531252c658d46acfdd955137686cd1f86 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -37,7 +37,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
                                          QuantifiersInferenceManager& qim,
                                          QuantifiersRegistry& qr,
                                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, qe),
+    : QuantifiersModule(qs, qim, qr, tr, qe),
       d_instStrategies(),
       d_isup(),
       d_i_ag(),

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 0a035a6911bfa6986766cd33615f71d92895262e..3c871014a8e0fd39f75f18817c3dd2f0c0874cf8 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -26,7 +26,6 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4;
@@ -90,8 +89,9 @@ BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
                                  QuantifiersRegistry& qr,
+                                 TermRegistry& tr,
                                  DecisionManager* dm)
-    : QuantifiersModule(qs, qim, qr, qe), d_dm(dm)
+    : QuantifiersModule(qs, qim, qr, tr, qe), d_dm(dm)
 {
 }
 
@@ -573,10 +573,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
   getBounds( f, v, rsi, l, u );
   Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
   if( !l.isNull() ){
-    l = d_quantEngine->getModel()->getValue( l );
+    l = d_treg.getModel()->getValue(l);
   }
   if( !u.isNull() ){
-    u = d_quantEngine->getModel()->getValue( u );
+    u = d_treg.getModel()->getValue(u);
   }
   Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
   return;
@@ -631,7 +631,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
   Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
   Assert(!expr::hasFreeVar(sr));
   Node sro = sr;
-  sr = d_quantEngine->getModel()->getValue(sr);
+  sr = d_treg.getModel()->getValue(sr);
   // if non-constant, then sr does not occur in the model, we fail
   if (!sr.isConst())
   {

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index fd32b35551aacb914c66a95ce0dfda49d5d51136..cb64978bbe89256240d8198f5616935fe60e16b7 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -24,6 +24,7 @@
 #include "context/context.h"
 #include "expr/attribute.h"
 #include "theory/decision_strategy.h"
+#include "theory/quantifiers/quant_bound_inference.h"
 
 namespace CVC4 {
 namespace theory {
@@ -167,6 +168,7 @@ private:
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
+                  TermRegistry& tr,
                   DecisionManager* dm);
   virtual ~BoundedIntegers();
 

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index b05f25b5e568c7a518bca034d97102fca9ec1c0b..85a2622b70ffaed5edaf3628885aa2152c3fc3a9 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -34,8 +34,9 @@ namespace quantifiers {
 ModelEngine::ModelEngine(QuantifiersEngine* qe,
                          QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
-                         QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe),
+                         QuantifiersRegistry& qr,
+                         TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe),
       d_incomplete_check(true),
       d_addedLemmas(0),
       d_triedLemmas(0),

diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index d0c0da4dd7347958d654ffbb58d635e246a690c7..0188de06f1044152d68926569c5964e884d71c32 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -46,7 +46,8 @@ public:
  ModelEngine(QuantifiersEngine* qe,
              QuantifiersState& qs,
              QuantifiersInferenceManager& qim,
-             QuantifiersRegistry& qr);
+             QuantifiersRegistry& qr,
+             TermRegistry& tr);
  virtual ~ModelEngine();
 
 public:

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index f2a41975f121ad8a2f9dab7690c1346042c95bbf..007c37b20f5b9fa761b98eee1d9c59a28b5f01b1 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -33,8 +33,9 @@ InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
                                    QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
                                    QuantifiersRegistry& qr,
+                                   TermRegistry& tr,
                                    RelevantDomain* rd)
-    : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1)
+    : QuantifiersModule(qs, qim, qr, tr, qe), d_rd(rd), d_fullSaturateLimit(-1)
 {
 }
 void InstStrategyEnum::presolve()

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 92e5ec71b88612649822dd435f419008b246529c..c97d8d1f45b7349b72a9e0a7940380c7847af03e 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -65,6 +65,7 @@ class InstStrategyEnum : public QuantifiersModule
                    QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
+                   TermRegistry& tr,
                    RelevantDomain* rd);
   ~InstStrategyEnum() {}
   /** Presolve */

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 52096a8ec6f9375bbbdbdd603dd85bfde89ae19b..ba1c3ddabe3146bcfae2763acf20acbb140a082f 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1857,8 +1857,9 @@ bool MatchGen::isHandled( TNode n ) {
 QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
                                      QuantifiersState& qs,
                                      QuantifiersInferenceManager& qim,
-                                     QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe),
+                                     QuantifiersRegistry& qr,
+                                     TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe),
       d_conflict(qs.getSatContext(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 5b54f8055c8e651fdd1cb825777e702571699801..818b99ea79449b17fd6b9b291f4a2870e49d7d82 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -239,7 +239,8 @@ private:  //for equivalence classes
   QuantConflictFind(QuantifiersEngine* qe,
                     QuantifiersState& qs,
                     QuantifiersInferenceManager& qim,
-                    QuantifiersRegistry& qr);
+                    QuantifiersRegistry& qr,
+                    TermRegistry& tr);
 
   /** register quantifier */
   void registerQuantifier(Node q) override;

diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index c694d9c2288df9f8ebb28558949d07b8bc20d183..a3256ee3184df481b8d0c1129bfabbe4060c573f 100644 (file)
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -13,10 +13,6 @@
  **/
 
 #include "theory/quantifiers/quant_module.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
@@ -27,8 +23,9 @@ QuantifiersModule::QuantifiersModule(
     quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersInferenceManager& qim,
     quantifiers::QuantifiersRegistry& qr,
+    quantifiers::TermRegistry& tr,
     QuantifiersEngine* qe)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
 {
 }
 
@@ -64,7 +61,7 @@ QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
 
 quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
 {
-  return d_quantEngine->getTermDatabase();
+  return d_treg.getTermDatabase();
 }
 
 quantifiers::QuantifiersState& QuantifiersModule::getState()

diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 948f144078475ef2043cbd9911b4a87819e79cd3..d0c2d024e17cdaf52cd89013724f99d83d8acd64 100644 (file)
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -63,6 +64,7 @@ class QuantifiersModule
   QuantifiersModule(quantifiers::QuantifiersState& qs,
                     quantifiers::QuantifiersInferenceManager& qim,
                     quantifiers::QuantifiersRegistry& qr,
+                    quantifiers::TermRegistry& tr,
                     QuantifiersEngine* qe);
   virtual ~QuantifiersModule() {}
   /** Presolve.
@@ -169,12 +171,14 @@ class QuantifiersModule
  protected:
   /** pointer to the quantifiers engine that owns this module */
   QuantifiersEngine* d_quantEngine;
-  /** The state of the quantifiers engine */
+  /** Reference to the state of the quantifiers engine */
   quantifiers::QuantifiersState& d_qstate;
-  /** The quantifiers inference manager */
+  /** Reference to the quantifiers inference manager */
   quantifiers::QuantifiersInferenceManager& d_qim;
-  /** The quantifiers registry */
+  /** Reference to the quantifiers registry */
   quantifiers::QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  quantifiers::TermRegistry& d_treg;
 }; /* class QuantifiersModule */
 
 }  // namespace theory

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 55f3469d2f150163a35ea2913036781ce3e1ab1a..23087286bb7b748eee3a15e3eb1d6009bbaf39a4 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -31,8 +31,9 @@ using namespace CVC4::theory::quantifiers;
 QuantDSplit::QuantDSplit(QuantifiersEngine* qe,
                          QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
-                         QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe), d_added_split(qs.getUserContext())
+                         QuantifiersRegistry& qr,
+                         TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe), d_added_split(qs.getUserContext())
 {
 }
 

diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index d91b0014630642ba795ea91369de43d9608e0c5c..13af881ee80fb64af6acbf1e721ca180b8f3ccf9 100644 (file)
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -52,7 +52,8 @@ class QuantDSplit : public QuantifiersModule {
   QuantDSplit(QuantifiersEngine* qe,
               QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
-              QuantifiersRegistry& qr);
+              QuantifiersRegistry& qr,
+              TermRegistry& tr);
   /** 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/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 1a7697608ec4365b59c78901d7bf39fb24934e99..f9467f7d897e5cc67dfd12962d3f07ac5b58d00a 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -51,12 +51,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   // add quantifiers modules
   if (options::quantConflictFind())
   {
-    d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr));
+    d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr, tr));
     modules.push_back(d_qcf.get());
   }
   if (options::conjectureGen())
   {
-    d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr));
+    d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr, tr));
     modules.push_back(d_sg_gen.get());
   }
   if (!options::finiteModelFind() || options::fmfInstEngine())
@@ -66,24 +66,24 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   }
   if (options::cegqi())
   {
-    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
+    d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr, tr));
     modules.push_back(d_i_cbqi.get());
     qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
   }
   if (options::sygus())
   {
-    d_synth_e.reset(new SynthEngine(qe, qs, qim, qr));
+    d_synth_e.reset(new SynthEngine(qe, qs, qim, qr, tr));
     modules.push_back(d_synth_e.get());
   }
   // finite model finding
   if (options::fmfBound())
   {
-    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm));
+    d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, tr, dm));
     modules.push_back(d_bint.get());
   }
   if (options::finiteModelFind() || options::fmfBound())
   {
-    d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
+    d_model_engine.reset(new ModelEngine(qe, qs, qim, qr, tr));
     modules.push_back(d_model_engine.get());
     Trace("quant-init-debug")
         << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
@@ -102,7 +102,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
   {
-    d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr));
+    d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr, tr));
     modules.push_back(d_qsplit.get());
   }
   if (options::quantAlphaEquiv())
@@ -113,12 +113,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe,
   if (options::fullSaturateQuant() || options::fullSaturateInterleave())
   {
     d_rel_dom.reset(new RelevantDomain(qe, qr));
-    d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
+    d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get()));
     modules.push_back(d_fs.get());
   }
   if (options::sygusInst())
   {
-    d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr));
+    d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr, tr));
     modules.push_back(d_sygus_inst.get());
   }
 }

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 98475911cf60d9387b1a74c54c5d14a190b81e22..d77a42a14bc8a14074f450b6a536e6978b418ecf 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -20,7 +20,6 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -32,9 +31,10 @@ namespace quantifiers {
 SynthEngine::SynthEngine(QuantifiersEngine* qe,
                          QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
-                         QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe),
-      d_tds(qe->getTermDatabaseSygus()),
+                         QuantifiersRegistry& qr,
+                         TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe),
+      d_tds(tr.getTermDatabaseSygus()),
       d_conj(nullptr),
       d_sqp(qe)
 {

diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index dcc5dd085755fc3df37c1db473ee0bf25e8de183..a4bed1737a55f9caa17850133385d52d715a294a 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -36,7 +36,8 @@ class SynthEngine : public QuantifiersModule
   SynthEngine(QuantifiersEngine* qe,
               QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
-              QuantifiersRegistry& qr);
+              QuantifiersRegistry& qr,
+              TermRegistry& tr);
   ~SynthEngine();
   /** presolve
    *

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 52a2787f7d462e18a5d1f4938ed07714942cfe21..c5f9b44b0a63e5fc588ee910f6bda232bc38e71a 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -186,8 +186,9 @@ void addSpecialValues(
 SygusInst::SygusInst(QuantifiersEngine* qe,
                      QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
-                     QuantifiersRegistry& qr)
-    : QuantifiersModule(qs, qim, qr, qe),
+                     QuantifiersRegistry& qr,
+                     TermRegistry& tr)
+    : QuantifiersModule(qs, qim, qr, tr, qe),
       d_ce_lemma_added(qs.getUserContext()),
       d_global_terms(qs.getUserContext()),
       d_notified_assertions(qs.getUserContext())
@@ -209,7 +210,7 @@ void SygusInst::reset_round(Theory::Effort e)
   d_active_quant.clear();
   d_inactive_quant.clear();
 
-  FirstOrderModel* model = d_quantEngine->getModel();
+  FirstOrderModel* model = d_treg.getModel();
   uint32_t nasserted = model->getNumAssertedQuantifiers();
 
   for (uint32_t i = 0; i < nasserted; ++i)
@@ -245,9 +246,9 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
 
   if (quant_e != QEFFORT_STANDARD) return;
 
-  FirstOrderModel* model = d_quantEngine->getModel();
+  FirstOrderModel* model = d_treg.getModel();
   Instantiate* inst = d_qim.getInstantiate();
-  TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
+  TermDbSygus* db = d_treg.getTermDatabaseSygus();
   SygusExplain syexplain(db);
   NodeManager* nm = NodeManager::currentNM();
   options::SygusInstMode mode = options::sygusInstMode();
@@ -480,7 +481,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
 
   /* Generate counterexample lemma for 'q'. */
   NodeManager* nm = NodeManager::currentNM();
-  TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
+  TermDbSygus* db = d_treg.getTermDatabaseSygus();
 
   /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
    * instantiation constant ic_i with type types[i] and wrap each ic_i in

diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 413c9f3a76ca462bdab4ab98d88cb7b978a36e84..dc8bc9c10aca52acf2bbd111f6f4cd7ac6a3db5e 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -66,7 +66,8 @@ class SygusInst : public QuantifiersModule
   SygusInst(QuantifiersEngine* qe,
             QuantifiersState& qs,
             QuantifiersInferenceManager& qim,
-            QuantifiersRegistry& qr);
+            QuantifiersRegistry& qr,
+            TermRegistry& tr);
   ~SygusInst() = default;
 
   bool needsCheck(Theory::Effort e) override;