Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.

8 files changed, 29 insertions, 16 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 4588e8952..42e7e2f13 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -29,8 +29,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p)
-    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
+CegisUnif::CegisUnif(QuantifiersEngine* qe,
+                     QuantifiersState& qs,
+                     SynthConjecture* p)
+    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p)
 {
 }
 
@@ -398,8 +400,8 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
 }
 
 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
-    QuantifiersEngine* qe, SynthConjecture* parent)
-    : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
+    QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent)
+    : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()),
       d_qe(qe),
       d_parent(parent)
 {
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index aca85a691..ee9ae0132 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -47,7 +47,9 @@ namespace quantifiers {
 class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 {
  public:
-  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, SynthConjecture* parent);
+  CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
+                                QuantifiersState& qs,
+                                SynthConjecture* parent);
   /** Make the n^th literal of this strategy (G_uq_n).
    *
    * This call may add new lemmas of the form described above
@@ -202,7 +204,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersEngine* qe, SynthConjecture* p);
+  CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p);
   ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ad125a70f..b007f8716 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -43,8 +43,10 @@ namespace theory {
 namespace quantifiers {
 
 SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
+                                 QuantifiersState& qs,
                                  SygusStatistics& s)
     : d_qe(qe),
+      d_qstate(qs),
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
@@ -56,7 +58,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_exampleInfer(new ExampleInfer(d_tds)),
       d_ceg_pbe(new SygusPbe(qe, this)),
       d_ceg_cegis(new Cegis(qe, this)),
-      d_ceg_cegisUnif(new CegisUnif(qe, this)),
+      d_ceg_cegisUnif(new CegisUnif(qe, qs, this)),
       d_sygus_ccore(new CegisCoreConnective(qe, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
@@ -235,7 +237,7 @@ void SynthConjecture::assign(Node q)
   d_feasible_strategy.reset(
       new DecisionStrategySingleton("sygus_feasible",
                                     d_feasible_guard,
-                                    d_qe->getSatContext(),
+                                    d_qstate.getSatContext(),
                                     d_qe->getValuation()));
   d_qe->getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 7786f57ad..1d43e30ff 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -82,7 +82,9 @@ class EnumValGenerator
 class SynthConjecture
 {
  public:
-  SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s);
+  SynthConjecture(QuantifiersEngine* qe,
+                  QuantifiersState& qs,
+                  SygusStatistics& s);
   ~SynthConjecture();
   /** presolve */
   void presolve();
@@ -199,6 +201,8 @@ class SynthConjecture
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
   /** term database sygus of d_qe */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f49cc962f..09a6add1c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -30,14 +30,14 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
-    : QuantifiersModule(qe),
+SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs)
+    : QuantifiersModule(qs, qe),
       d_tds(qe->getTermDatabaseSygus()),
       d_conj(nullptr),
       d_sqp(qe)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-      new SynthConjecture(d_quantEngine, d_statistics)));
+      new SynthConjecture(d_quantEngine, qs, d_statistics)));
   d_conj = d_conjs.back().get();
 }
 
@@ -159,7 +159,7 @@ void SynthEngine::assignConjecture(Node q)
   if (d_conjs.back()->isAssigned())
   {
     d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-        new SynthConjecture(d_quantEngine, d_statistics)));
+        new SynthConjecture(d_quantEngine, d_qstate, d_statistics)));
   }
   d_conjs.back()->assign(q);
 }
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 25981748e..e3cf2e47b 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -33,7 +33,7 @@ class SynthEngine : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
  public:
-  SynthEngine(QuantifiersEngine* qe, context::Context* c);
+  SynthEngine(QuantifiersEngine* qe, QuantifiersState& qs);
   ~SynthEngine();
   /** presolve
    *
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index ccc23f109..210ebb921 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -46,8 +46,9 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
   return os;
 }
 
-TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
+TermDbSygus::TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs)
     : d_quantEngine(qe),
+      d_qstate(qs),
       d_syexp(new SygusExplain(this)),
       d_ext_rw(new ExtendedRewriter(true)),
       d_eval(new Evaluator),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index e082cf15b..1bf6b6ca7 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -54,7 +54,7 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
 // TODO :issue #1235 split and document this class
 class TermDbSygus {
  public:
-  TermDbSygus(context::Context* c, QuantifiersEngine* qe);
+  TermDbSygus(QuantifiersEngine* qe, QuantifiersState& qs);
   ~TermDbSygus() {}
   /** Reset this utility */
   bool reset(Theory::Effort e);
@@ -316,6 +316,8 @@ class TermDbSygus {
  private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
 
   //------------------------------utilities
   /** sygus explanation */