Make quantifier module classes derive from EnvObj (#7132)

8 files changed, 15 insertions, 13 deletions

diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 8a5ce1c1f..56eaccd7c 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/smt_engine_subsolver.h"
 
@@ -40,10 +41,10 @@ namespace quantifiers {
  * from (enumerated) expressions. This includes:
  * - candidate rewrite rules (--sygus-rr-synth)
  */
-class ExprMiner
+class ExprMiner : protected EnvObj
 {
  public:
-  ExprMiner(Env& env) : d_env(env), d_sampler(nullptr) {}
+  ExprMiner(Env& env) : EnvObj(env), d_sampler(nullptr) {}
   virtual ~ExprMiner() {}
   /** initialize
    *
@@ -64,8 +65,6 @@ class ExprMiner
   virtual bool addTerm(Node n, std::ostream& out) = 0;
 
  protected:
-  /** Reference to the env */
-  Env& d_env;
   /** the set of variables used by this class */
   std::vector<Node> d_vars;
   /**
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index 92b7c105d..ae20d4909 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -22,7 +22,7 @@ namespace theory {
 namespace quantifiers {
 
 ExpressionMinerManager::ExpressionMinerManager(Env& env)
-    : d_env(env),
+    : EnvObj(env),
       d_doRewSynth(false),
       d_doQueryGen(false),
       d_doFilterLogicalStrength(false),
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index b38de1337..92450b3ba 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/quantifiers/query_generator.h"
@@ -39,7 +40,7 @@ namespace quantifiers {
  * coordination, possibly sharing information and utilities like a common
  * sampling object.
  */
-class ExpressionMinerManager
+class ExpressionMinerManager : protected EnvObj
 {
  public:
   ExpressionMinerManager(Env& env);
@@ -93,8 +94,6 @@ class ExpressionMinerManager
   bool addTerm(Node sol, std::ostream& out, bool& rew_print);
 
  private:
-  /** Reference to the env */
-  Env& d_env;
   /** whether we are doing rewrite synthesis */
   bool d_doRewSynth;
   /** whether we are doing query generation */
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index b6bedfbff..d5488f0c9 100644
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -25,7 +25,7 @@ QuantifiersModule::QuantifiersModule(
     quantifiers::QuantifiersInferenceManager& qim,
     quantifiers::QuantifiersRegistry& qr,
     quantifiers::TermRegistry& tr)
-    : d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+    : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
 {
 }
 
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index a3e306a4e..7358aa555 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -22,6 +22,7 @@
 #include <map>
 #include <vector>
 
+#include "smt/env_obj.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -40,7 +41,7 @@ class TermDb;
  * This is the virtual class for defining subsolvers of the quantifiers theory.
  * It has a similar interface to a Theory object.
  */
-class QuantifiersModule
+class QuantifiersModule : protected EnvObj
 {
  public:
   /** effort levels for quantifiers modules check */
diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h
index e3da8c986..7257ec4ee 100644
--- a/src/theory/quantifiers/solution_filter.h
+++ b/src/theory/quantifiers/solution_filter.h
@@ -40,7 +40,7 @@ namespace quantifiers {
 class SolutionFilterStrength : public ExprMiner
 {
  public:
-  SolutionFilterStrength(Env& d_env);
+  SolutionFilterStrength(Env& env);
   ~SolutionFilterStrength() {}
   /** initialize */
   void initialize(const std::vector<Node>& vars,
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 4cb333849..8272c6418 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/quantifiers/sygus/sygus_module.h"
 
+#include "theory/quantifiers/quantifiers_state.h"
+
 namespace cvc5 {
 namespace theory {
 namespace quantifiers {
@@ -23,7 +25,7 @@ SygusModule::SygusModule(QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          TermDbSygus* tds,
                          SynthConjecture* p)
-    : d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
+    : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
 {
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index d7e0caa5b..8070fe009 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -49,7 +50,7 @@ class QuantifiersInferenceManager;
  * Modules implement an initialize function, which determines whether the module
  * will take responsibility for the given conjecture.
  */
-class SygusModule
+class SygusModule : protected EnvObj
 {
  public:
   SygusModule(QuantifiersState& qs,