From 962c83047eed6f471f2c40f664df631ebd1350ae Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 3 Sep 2021 12:09:57 -0500 Subject: Make quantifier module classes derive from EnvObj (#7132) --- src/theory/quantifiers/expr_miner.h | 7 +++---- src/theory/quantifiers/expr_miner_manager.cpp | 2 +- src/theory/quantifiers/expr_miner_manager.h | 5 ++--- src/theory/quantifiers/quant_module.cpp | 2 +- src/theory/quantifiers/quant_module.h | 3 ++- src/theory/quantifiers/solution_filter.h | 2 +- src/theory/quantifiers/sygus/sygus_module.cpp | 4 +++- src/theory/quantifiers/sygus/sygus_module.h | 3 ++- 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 #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 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 #include +#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& 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 #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, -- cgit v1.2.3