Make quantifier module classes derive from EnvObj (#7132)

diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 8a5ce1c1f9af9a6b05e706b4335c528e666fe529..56eaccd7cbeea42d32273155f63496c7e676cd96 100644 (file)
--- 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 92b7c105d2d94fb3d4a180690a12c352c9e857d5..ae20d49099ac48b3ed442059a6cc22b783d30273 100644 (file)
--- 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 b38de1337b943c7a6689a1a8b19fd3da3ae4c05d..92450b3baba55b80a358c02da5740826cb9bbb20 100644 (file)
--- 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 b6bedfbff1014b7e500e74fc53910b8b8bc1d0da..d5488f0c983746b3f48bbe7be8c091cc544a82a4 100644 (file)
--- 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 a3e306a4ed1569b192c18a0ee9b40c0b3958643a..7358aa55549ed20e46e3229e932cfad1b92b6acb 100644 (file)
--- 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 e3da8c98663879d02791fe393e7060d0609061b3..7257ec4eea798df1d6e0ecf58c8cbe7bae635e64 100644 (file)
--- 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 4cb333849d7d02018570bd450be9b1763e293c03..8272c641807568a1144927aa23de1ff8b5bde15e 100644 (file)
--- 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 d7e0caa5b71e055ac8b745368380b36cf3b6a1b7..8070fe009ed6b48c2d0b7a58c5819d8816a0c90c 100644 (file)
--- 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,