From e5aaebbbc5ea11b0cb3468169e5c80bf38868c82 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 9 Sep 2021 11:37:49 -0700 Subject: Remove `TheoryState::getEnv()` (#7163) --- src/theory/arith/nl/nonlinear_extension.cpp | 10 +++++----- src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 7 ++++--- src/theory/quantifiers/cegqi/inst_strategy_cegqi.h | 4 +++- src/theory/quantifiers/conjecture_generator.cpp | 10 +++++----- src/theory/quantifiers/conjecture_generator.h | 4 +++- .../quantifiers/ematching/instantiation_engine.cpp | 2 +- src/theory/quantifiers/fmf/bounded_integers.cpp | 5 +++-- src/theory/quantifiers/fmf/bounded_integers.h | 7 ++++--- src/theory/quantifiers/fmf/model_engine.cpp | 5 +++-- src/theory/quantifiers/fmf/model_engine.h | 4 +++- src/theory/quantifiers/inst_strategy_enumerative.cpp | 5 +++-- src/theory/quantifiers/inst_strategy_enumerative.h | 4 +++- src/theory/quantifiers/inst_strategy_pool.cpp | 5 +++-- src/theory/quantifiers/inst_strategy_pool.h | 4 +++- src/theory/quantifiers/quant_conflict_find.cpp | 5 +++-- src/theory/quantifiers/quant_conflict_find.h | 3 ++- src/theory/quantifiers/quant_module.cpp | 3 ++- src/theory/quantifiers/quant_module.h | 3 ++- src/theory/quantifiers/quant_split.cpp | 6 ++++-- src/theory/quantifiers/quant_split.h | 4 +++- src/theory/quantifiers/quantifiers_modules.cpp | 18 +++++++++--------- src/theory/quantifiers/sygus/cegis.cpp | 5 +++-- src/theory/quantifiers/sygus/cegis.h | 5 ++++- src/theory/quantifiers/sygus/cegis_core_connective.cpp | 13 ++++++------- src/theory/quantifiers/sygus/cegis_core_connective.h | 4 +++- src/theory/quantifiers/sygus/cegis_unif.cpp | 10 ++++++---- src/theory/quantifiers/sygus/cegis_unif.h | 7 +++++-- src/theory/quantifiers/sygus/sygus_module.cpp | 5 +++-- src/theory/quantifiers/sygus/sygus_module.h | 3 ++- src/theory/quantifiers/sygus/sygus_pbe.cpp | 5 +++-- src/theory/quantifiers/sygus/sygus_pbe.h | 4 +++- src/theory/quantifiers/sygus/synth_conjecture.cpp | 8 ++++---- src/theory/quantifiers/sygus/synth_engine.cpp | 2 +- src/theory/quantifiers/sygus_inst.cpp | 11 ++++++----- src/theory/quantifiers/sygus_inst.h | 4 +++- src/theory/quantifiers/term_registry.cpp | 8 ++++---- src/theory/quantifiers/term_registry.h | 3 ++- src/theory/theory_state.h | 2 -- 38 files changed, 129 insertions(+), 88 deletions(-) diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 742e5ca49..b8170df45 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -49,14 +49,14 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheoryCb(state.getEqualityEngine()), d_extTheory(d_extTheoryCb, context(), userContext(), d_im), d_model(), - d_trSlv(d_im, d_model, d_astate.getEnv()), - d_extState(d_im, d_model, d_astate.getEnv()), + d_trSlv(d_im, d_model, d_env), + d_extState(d_im, d_model, d_env), d_factoringSlv(&d_extState), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_astate.getEnv(), d_im, d_model), + d_cadSlv(d_env, d_im, d_model), d_icpSlv(d_im), d_iandSlv(env, d_im, state, d_model), d_pow2Slv(env, d_im, state, d_model) @@ -72,9 +72,9 @@ NonlinearExtension::NonlinearExtension(Env& env, d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_astate.getEnv().isTheoryProofProducing()) + if (d_env.isTheoryProofProducing()) { - ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker(); + ProofChecker* pc = d_env.getProofNodeManager()->getChecker(); d_proofChecker.registerTo(pc); } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 81366fabd..8334cc248 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -47,11 +47,12 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, return d_parent->rewriteInstantiation(q, terms, inst, doVts); } -InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, +InstStrategyCegqi::InstStrategyCegqi(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), @@ -70,7 +71,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, } if (options::cegqiNestedQE()) { - d_nestedQe.reset(new NestedQe(qs.getEnv())); + d_nestedQe.reset(new NestedQe(d_env)); } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 882f69b85..a568b0b4d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#include "smt/env_obj.h" #include "theory/decision_manager.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" @@ -69,7 +70,8 @@ class InstStrategyCegqi : public QuantifiersModule typedef context::CDHashMap NodeIntMap; public: - InstStrategyCegqi(QuantifiersState& qs, + InstStrategyCegqi(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 17eaad5c6..f9625d7ac 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -86,15 +86,15 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } } -ConjectureGenerator::ConjectureGenerator(QuantifiersState& qs, +ConjectureGenerator::ConjectureGenerator(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_notify(*this), - d_uequalityEngine( - d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false), - d_ee_conjectures(qs.getSatContext()), + d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false), + d_ee_conjectures(context()), d_conj_count(0), d_subs_confirmCount(0), d_subs_unkCount(0), diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index ef60792a6..bc5f3fb13 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -21,6 +21,7 @@ #include "context/cdhashmap.h" #include "expr/node_trie.h" #include "expr/term_canonize.h" +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" #include "theory/type_enumerator.h" @@ -437,7 +438,8 @@ private: //information about ground equivalence classes unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: - ConjectureGenerator(QuantifiersState& qs, + ConjectureGenerator(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index dcfa71f8c..62c5c2440 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -37,7 +37,7 @@ InstantiationEngine::InstantiationEngine(Env& env, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), 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 3fd478c31..b04391db3 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -88,11 +88,12 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() return lem; } -BoundedIntegers::BoundedIntegers(QuantifiersState& qs, +BoundedIntegers::BoundedIntegers(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr) + : QuantifiersModule(env, qs, qim, qr, tr) { } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index d37e71b72..8c468c1de 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -18,13 +18,13 @@ #ifndef CVC5__BOUNDED_INTEGERS_H #define CVC5__BOUNDED_INTEGERS_H -#include "theory/quantifiers/quant_module.h" - #include "context/cdhashmap.h" #include "context/context.h" #include "expr/attribute.h" +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_bound_inference.h" +#include "theory/quantifiers/quant_module.h" namespace cvc5 { namespace theory { @@ -164,7 +164,8 @@ private: std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; public: - BoundedIntegers(QuantifiersState& qs, + BoundedIntegers(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index e58f66d0b..256899580 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -31,12 +31,13 @@ namespace theory { namespace quantifiers { //Model Engine constructor -ModelEngine::ModelEngine(QuantifiersState& qs, +ModelEngine::ModelEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, QModelBuilder* builder) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), 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 f818a6362..b5ab86f20 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H #define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#include "smt/env_obj.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/quant_module.h" #include "theory/theory_model.h" @@ -42,7 +43,8 @@ private: int d_triedLemmas; int d_totalLemmas; public: - ModelEngine(QuantifiersState& qs, + ModelEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index aeff27433..6769d8bc2 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -29,12 +29,13 @@ namespace cvc5 { namespace theory { namespace quantifiers { -InstStrategyEnum::InstStrategyEnum(QuantifiersState& qs, +InstStrategyEnum::InstStrategyEnum(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, RelevantDomain* rd) - : QuantifiersModule(qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(env, qs, qim, qr, tr), 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 a298e3a8a..66315c070 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -18,6 +18,7 @@ #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H #define CVC5__INST_STRATEGY_ENUMERATIVE_H +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5 { @@ -62,7 +63,8 @@ class RelevantDomain; class InstStrategyEnum : public QuantifiersModule { public: - InstStrategyEnum(QuantifiersState& qs, + InstStrategyEnum(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp index 0e32c246e..cadda033b 100644 --- a/src/theory/quantifiers/inst_strategy_pool.cpp +++ b/src/theory/quantifiers/inst_strategy_pool.cpp @@ -30,11 +30,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -InstStrategyPool::InstStrategyPool(QuantifiersState& qs, +InstStrategyPool::InstStrategyPool(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr) + : QuantifiersModule(env, qs, qim, qr, tr) { } diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h index acdc0010b..1f79717af 100644 --- a/src/theory/quantifiers/inst_strategy_pool.h +++ b/src/theory/quantifiers/inst_strategy_pool.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5 { @@ -38,7 +39,8 @@ namespace quantifiers { class InstStrategyPool : public QuantifiersModule { public: - InstStrategyPool(QuantifiersState& qs, + InstStrategyPool(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 8c4d68631..983eee9ae 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1853,11 +1853,12 @@ bool MatchGen::isHandled( TNode n ) { return true; } -QuantConflictFind::QuantConflictFind(QuantifiersState& qs, +QuantConflictFind::QuantConflictFind(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index de521cd07..927a74ff2 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -238,7 +238,8 @@ private: //for equivalence classes bool areMatchDisequal( TNode n1, TNode n2 ); public: - QuantConflictFind(QuantifiersState& qs, + QuantConflictFind(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index d5488f0c9..8fb37c548 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -21,11 +21,12 @@ namespace cvc5 { namespace theory { QuantifiersModule::QuantifiersModule( + Env& env, quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr) - : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) + : EnvObj(env), 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 7358aa555..639f9c2b4 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -60,7 +60,8 @@ class QuantifiersModule : protected EnvObj }; public: - QuantifiersModule(quantifiers::QuantifiersState& qs, + QuantifiersModule(Env& env, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 941b94d23..905424107 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -28,11 +28,13 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QuantDSplit::QuantDSplit(QuantifiersState& qs, +QuantDSplit::QuantDSplit(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), d_added_split(qs.getUserContext()) + : QuantifiersModule(env, qs, qim, qr, tr), + d_added_split(qs.getUserContext()) { } diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 18aeec773..84cc6fea7 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__QUANT_SPLIT_H #include "context/cdo.h" +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5 { @@ -50,7 +51,8 @@ class QuantDSplit : public QuantifiersModule { typedef context::CDHashSet NodeSet; public: - QuantDSplit(QuantifiersState& qs, + QuantDSplit(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 889b6ac26..563951189 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -52,12 +52,12 @@ void QuantifiersModules::initialize(Env& env, // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qs, qim, qr, tr)); + d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qs, qim, qr, tr)); + d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) @@ -67,7 +67,7 @@ void QuantifiersModules::initialize(Env& env, } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qs, qim, qr, tr)); + d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr)); modules.push_back(d_i_cbqi.get()); qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } @@ -80,18 +80,18 @@ void QuantifiersModules::initialize(Env& env, // fmfBound, or if strings are enabled. if (options::fmfBound() || options::stringExp()) { - d_bint.reset(new BoundedIntegers(qs, qim, qr, tr)); + d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound() || options::stringExp()) { - d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder)); + d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qs, qim, qr, tr)); + d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) @@ -102,17 +102,17 @@ void QuantifiersModules::initialize(Env& env, if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr)); - d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get())); + d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::poolInst()) { - d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr)); + d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr)); modules.push_back(d_ipool.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr)); + d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 708bffe80..f5774c761 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -32,11 +32,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersState& qs, +Cegis::Cegis(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p), + : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), d_usingSymCons(false) { diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index d6678a305..d72805950 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -19,6 +19,8 @@ #define CVC5__THEORY__QUANTIFIERS__CEGIS_H #include + +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus_sampler.h" @@ -42,7 +44,8 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersState& qs, + Cegis(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 9a9d8f02d..a42323227 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -68,11 +68,12 @@ bool VariadicTrie::hasSubset(const std::vector& is) const return false; } -CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs, +CegisCoreConnective::CegisCoreConnective(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qs, qim, tds, p) + : Cegis(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -629,9 +630,7 @@ bool CegisCoreConnective::getUnsatCore( Result CegisCoreConnective::checkSat(Node n, std::vector& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; - Env& env = d_qstate.getEnv(); - Result r = - checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo()); + Result r = checkWithSubsolver(n, d_vars, mvs, options(), logicInfo()); Trace("sygus-ccore-debug") << "...got " << r << std::endl; return r; } @@ -739,7 +738,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, addSuccess = false; // try a new core std::unique_ptr checkSol; - initializeSubsolver(checkSol, d_qstate.getEnv()); + initializeSubsolver(checkSol, d_env); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector rasserts = asserts; rasserts.push_back(d_sc); @@ -779,7 +778,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // In terms of Variant #2, this is the check "if S ^ U is unsat" Trace("sygus-ccore") << "----- Check side condition" << std::endl; std::unique_ptr checkSc; - initializeSubsolver(checkSc, d_qstate.getEnv()); + initializeSubsolver(checkSc, d_env); std::vector scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); scasserts.push_back(d_sc); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index e9a73e9bb..80ba6f26e 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_trie.h" +#include "smt/env_obj.h" #include "theory/evaluator.h" #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" @@ -160,7 +161,8 @@ class VariadicTrie class CegisCoreConnective : public Cegis { public: - CegisCoreConnective(QuantifiersState& qs, + CegisCoreConnective(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 797aecdab..871a85fbd 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -30,13 +30,14 @@ namespace cvc5 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersState& qs, +CegisUnif::CegisUnif(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qs, qim, tds, p), - d_sygus_unif(qs.getEnv(), p), - d_u_enum_manager(qs, qim, tds, p) + : Cegis(env, qs, qim, tds, p), + d_sygus_unif(env, p), + d_u_enum_manager(env, qs, qim, tds, p) { } @@ -403,6 +404,7 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, Node lem) } CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( + Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 0cddff9c1..da47aabbe 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -20,6 +20,7 @@ #include #include +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" @@ -49,7 +50,8 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersState& qs, + CegisUnifEnumDecisionStrategy(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* parent); @@ -207,7 +209,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersState& qs, + CegisUnif(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 8272c6418..1840f0eb1 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -21,11 +21,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersState& qs, +SygusModule::SygusModule(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p) + : EnvObj(env), 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 8070fe009..8ee1fc9b4 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -53,7 +53,8 @@ class QuantifiersInferenceManager; class SygusModule : protected EnvObj { public: - SygusModule(QuantifiersState& qs, + SygusModule(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 52bca1586..453ac5c18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -30,11 +30,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersState& qs, +SygusPbe::SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p) + : SygusModule(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 867764617..e55479e18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/sygus_module.h" namespace cvc5 { @@ -86,7 +87,8 @@ class SynthConjecture; class SygusPbe : public SygusModule { public: - SygusPbe(QuantifiersState& qs, + SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 730482073..da021227a 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -66,10 +66,10 @@ SynthConjecture::SynthConjecture(Env& env, d_ceg_gc(new CegGrammarConstructor(d_tds, this)), d_sygus_rconst(new SygusRepairConst(env, d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), - d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)), - d_ceg_cegis(new Cegis(qs, qim, d_tds, this)), - d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)), - d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)), + d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)), + d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)), + d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)), + d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 64227793d..454442351 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -31,7 +31,7 @@ SynthEngine::SynthEngine(Env& env, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv()) + : QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env) { d_conjs.push_back(std::unique_ptr( new SynthConjecture(env, qs, qim, qr, tr, d_statistics))); diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 21852f25a..4da273cd9 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -182,14 +182,15 @@ void addSpecialValues(const TypeNode& tn, } // namespace -SygusInst::SygusInst(QuantifiersState& qs, +SygusInst::SygusInst(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), - d_ce_lemma_added(qs.getUserContext()), - d_global_terms(qs.getUserContext()), - d_notified_assertions(qs.getUserContext()) + : QuantifiersModule(env, qs, qim, qr, tr), + d_ce_lemma_added(userContext()), + d_global_terms(userContext()), + d_notified_assertions(userContext()) { } diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 80c7e809f..060ab7226 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -22,6 +22,7 @@ #include #include "context/cdhashset.h" +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_module.h" @@ -64,7 +65,8 @@ namespace quantifiers { class SygusInst : public QuantifiersModule { public: - SygusInst(QuantifiersState& qs, + SygusInst(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 7ad782fda..98618f3f7 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -32,13 +32,13 @@ namespace quantifiers { TermRegistry::TermRegistry(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) - : d_presolve(qs.getUserContext(), true), + : EnvObj(env), + d_presolve(qs.getUserContext(), true), d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), d_termPools(new TermPools(env, qs)), - d_termDb(qs.getEnv().getLogicInfo().isHigherOrder() - ? new HoTermDb(env, qs, qr) - : new TermDb(env, qs, qr)), + d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr) + : new TermDb(env, qs, qr)), d_sygusTdb(nullptr), d_qmodel(nullptr) { diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index e0ce73286..175d450df 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -22,6 +22,7 @@ #include #include "context/cdhashset.h" +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" @@ -37,7 +38,7 @@ class FirstOrderModel; * Term Registry, which manages notifying modules within quantifiers about * (ground) terms that exist in the current context. */ -class TermRegistry +class TermRegistry : protected EnvObj { using NodeSet = context::CDHashSet; diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 049123b8d..574aa9355 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -46,8 +46,6 @@ class TheoryState : protected EnvObj context::Context* getSatContext() const; /** Get the user context */ context::UserContext* getUserContext() const; - /** Get the environment */ - Env& getEnv() const { return d_env; } //-------------------------------------- equality information /** Is t registered as a term in the equality engine of this class? */ virtual bool hasTerm(TNode a) const; -- cgit v1.2.3