diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-13 16:14:54 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-13 18:14:54 -0500 |
commit | a37f486c6e10b882a81474418e1d3f4ffdbd583c (patch) | |
tree | 6b73a761684a5caba5745c7e5fbc37102beccebd /src/theory/quantifiers | |
parent | 09cbf1c5746c69854a7578263240101e2430173e (diff) |
Remove context getters from `TheoryState` (#7174)
This removes TheoryState::getSatContext() and
TheoryState::getUserContext().
Diffstat (limited to 'src/theory/quantifiers')
20 files changed, 67 insertions, 67 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 8334cc248..1ccfd8ede 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env, d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), - d_added_cbqi_lemma(qs.getUserContext()), + d_added_cbqi_lemma(userContext()), d_vtsCache(new VtsTermCache(qim)), d_bv_invert(nullptr), d_small_const_multiplier( @@ -168,10 +168,8 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) DecisionStrategy* dlds = nullptr; if (itds == d_dstrat.end()) { - d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral", - ceLit, - d_qstate.getSatContext(), - d_qstate.getValuation())); + d_dstrat[q].reset(new DecisionStrategySingleton( + d_env, "CexLiteral", ceLit, d_qstate.getValuation())); dlds = d_dstrat[q].get(); } else diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index f9625d7ac..da8727c12 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -167,7 +167,7 @@ ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bo if( eqc_i!=d_eqc_info.end() ){ return eqc_i->second; }else if( doMake ){ - EqcInfo* ei = new EqcInfo(d_qstate.getSatContext()); + EqcInfo* ei = new EqcInfo(context()); d_eqc_info[n] = ei; return ei; }else{ diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 92ec1e452..30d223b2a 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -33,7 +33,7 @@ EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m) : QuantifiersUtil(env), d_qstate(qs), d_model(m), - d_eqi_counter(qs.getSatContext()), + d_eqi_counter(context()), d_reset_count(0) { } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 841177a7f..cfd903646 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -46,11 +46,12 @@ FirstOrderModel::FirstOrderModel(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr) - : d_model(nullptr), + : EnvObj(env), + d_model(nullptr), d_qreg(qr), d_treg(tr), d_eq_query(env, qs, this), - d_forall_asserts(qs.getSatContext()), + d_forall_asserts(context()), d_forallRlvComputed(false) { } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 05bdcbee6..526bbe10b 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,6 +19,7 @@ #define CVC5__FIRST_ORDER_MODEL_H #include "context/cdlist.h" +#include "smt/env_obj.h" #include "theory/quantifiers/equality_query.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" @@ -36,7 +37,7 @@ class TermRegistry; class QuantifiersRegistry; // TODO (#1301) : document and refactor this class -class FirstOrderModel +class FirstOrderModel : protected EnvObj { public: FirstOrderModel(Env& env, diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b04391db3..4a3e13dd0 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -37,12 +37,10 @@ using namespace cvc5::theory::quantifiers; using namespace cvc5::kind; BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( - Node r, - context::Context* c, - context::Context* u, - Valuation valuation, - bool isProxy) - : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u) + Env& env, Node r, Valuation valuation, bool isProxy) + : DecisionStrategyFmf(env, valuation), + d_range(r), + d_ranges_proxied(userContext()) { if( options::fmfBoundLazy() ){ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); @@ -514,12 +512,8 @@ void BoundedIntegers::checkOwnership(Node f) { Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl; d_ranges.push_back( r ); - d_rms[r].reset( - new IntRangeDecisionHeuristic(r, - d_qstate.getSatContext(), - d_qstate.getUserContext(), - d_qstate.getValuation(), - isProxy)); + d_rms[r].reset(new IntRangeDecisionHeuristic( + d_env, r, d_qstate.getValuation(), isProxy)); dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE, d_rms[r].get()); } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 8c468c1de..2c3a86fc7 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -100,9 +100,8 @@ private: class IntRangeDecisionHeuristic : public DecisionStrategyFmf { public: - IntRangeDecisionHeuristic(Node r, - context::Context* c, - context::Context* u, + IntRangeDecisionHeuristic(Env& env, + Node r, Valuation valuation, bool isProxy); /** make the n^th literal of this strategy */ diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index ba9ea9152..a4107564e 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -189,16 +189,18 @@ CDInstMatchTrie::~CDInstMatchTrie() d_data.clear(); } -bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs, +bool CDInstMatchTrie::existsInstMatch(context::Context* context, + quantifiers::QuantifiersState& qs, Node q, const std::vector<Node>& m, bool modEq, unsigned index) { - return !addInstMatch(qs, q, m, modEq, index, true); + return !addInstMatch(context, qs, q, m, modEq, index, true); } -bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, +bool CDInstMatchTrie::addInstMatch(context::Context* context, + quantifiers::QuantifiersState& qs, Node f, const std::vector<Node>& m, bool modEq, @@ -226,7 +228,8 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n); if (it != d_data.end()) { - bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist); + bool ret = + it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist); if (!onlyExist || !ret) { return reset || ret; @@ -246,7 +249,8 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en); if (itc != d_data.end()) { - if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true)) + if (itc->second->addInstMatch( + context, qs, f, m, modEq, index + 1, true)) { return false; } @@ -259,10 +263,10 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, if (!onlyExist) { - CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext()); + CDInstMatchTrie* imt = new CDInstMatchTrie(context); Assert(d_data.find(n) == d_data.end()); d_data[n] = imt; - imt->addInstMatch(qs, f, m, modEq, index + 1, false); + imt->addInstMatch(context, qs, f, m, modEq, index + 1, false); } return true; } diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 83bd8d3b1..5ddc299af 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -23,6 +23,7 @@ #include "context/cdlist.h" #include "context/cdo.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -131,7 +132,8 @@ class CDInstMatchTrie * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ - bool existsInstMatch(QuantifiersState& qs, + bool existsInstMatch(context::Context* context, + QuantifiersState& qs, Node q, const std::vector<Node>& m, bool modEq = false, @@ -145,7 +147,8 @@ class CDInstMatchTrie * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ - bool addInstMatch(QuantifiersState& qs, + bool addInstMatch(context::Context* context, + QuantifiersState& qs, Node q, const std::vector<Node>& m, bool modEq = false, diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f0af73832..2a3974d49 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -54,11 +54,10 @@ Instantiate::Instantiate(Env& env, d_qreg(qr), d_treg(tr), d_pnm(pnm), - d_insts(qs.getUserContext()), - d_c_inst_match_trie_dom(qs.getUserContext()), - d_pfInst( - pnm ? new CDProof(pnm, qs.getUserContext(), "Instantiate::pfInst") - : nullptr) + d_insts(userContext()), + d_c_inst_match_trie_dom(userContext()), + d_pfInst(pnm ? new CDProof(pnm, userContext(), "Instantiate::pfInst") + : nullptr) { } @@ -507,7 +506,7 @@ bool Instantiate::existsInstantiation(Node q, std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { - return it->second->existsInstMatch(d_qstate, q, terms, modEq); + return it->second->existsInstMatch(userContext(), d_qstate, q, terms, modEq); } } else @@ -594,10 +593,10 @@ bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms) const auto res = d_c_inst_match_trie.insert({q, nullptr}); if (res.second) { - res.first->second = new CDInstMatchTrie(d_qstate.getUserContext()); + res.first->second = new CDInstMatchTrie(userContext()); } d_c_inst_match_trie_dom.insert(q); - return res.first->second->addInstMatch(d_qstate, q, terms); + return res.first->second->addInstMatch(userContext(), d_qstate, q, terms); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms); @@ -750,7 +749,7 @@ InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q) return it->second.get(); } std::shared_ptr<InstLemmaList> ill = - std::make_shared<InstLemmaList>(d_qstate.getUserContext()); + std::make_shared<InstLemmaList>(userContext()); d_insts.insert(q, ill); return ill.get(); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 983eee9ae..1de60422f 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1859,7 +1859,7 @@ QuantConflictFind::QuantConflictFind(Env& env, QuantifiersRegistry& qr, TermRegistry& tr) : QuantifiersModule(env, qs, qim, qr, tr), - d_conflict(qs.getSatContext(), false), + d_conflict(context(), false), d_true(NodeManager::currentNM()->mkConst<bool>(true)), d_false(NodeManager::currentNM()->mkConst<bool>(false)), d_effort(EFFORT_INVALID) diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 905424107..db07d07d0 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -33,8 +33,7 @@ QuantDSplit::QuantDSplit(Env& env, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(env, qs, qim, qr, tr), - d_added_split(qs.getUserContext()) + : QuantifiersModule(env, qs, qim, qr, tr), d_added_split(userContext()) { } diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index b2a08c249..20987b02e 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -31,7 +31,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( ProofNodeManager* pnm) : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"), d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)), - d_skolemize(new Skolemize(state, tr, pnm)) + d_skolemize(new Skolemize(env, state, tr, pnm)) { } diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 23b66b1de..bb0fa3899 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -35,16 +35,18 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Skolemize::Skolemize(QuantifiersState& qs, +Skolemize::Skolemize(Env& env, + QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm) - : d_qstate(qs), + : EnvObj(env), + d_qstate(qs), d_treg(tr), - d_skolemized(qs.getUserContext()), + d_skolemized(userContext()), d_pnm(pnm), - d_epg(pnm == nullptr ? nullptr - : new EagerProofGenerator( - pnm, qs.getUserContext(), "Skolemize::epg")) + d_epg(pnm == nullptr + ? nullptr + : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg")) { } diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index fbb79f5d2..294ad0084 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -26,6 +26,7 @@ #include "expr/type_node.h" #include "proof/eager_proof_generator.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -63,12 +64,15 @@ class TermRegistry; * default and can be enabled by option: * --quant-ind */ -class Skolemize +class Skolemize : protected EnvObj { typedef context::CDHashMap<Node, Node> NodeNodeMap; public: - Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm); + Skolemize(Env& env, + QuantifiersState& qs, + TermRegistry& tr, + ProofNodeManager* pnm); ~Skolemize() {} /** skolemize quantified formula q * If the return value ret of this function is non-null, then ret is a trust diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 871a85fbd..6b260bb81 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -409,7 +409,7 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* parent) - : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()), + : DecisionStrategyFmf(env, qs.getValuation()), d_qim(qim), d_tds(tds), d_parent(parent) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index da021227a..22ba879d7 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -241,11 +241,8 @@ void SynthConjecture::assign(Node q) } // register the strategy - d_feasible_strategy.reset( - new DecisionStrategySingleton("sygus_feasible", - d_feasible_guard, - d_qstate.getSatContext(), - d_qstate.getValuation())); + d_feasible_strategy.reset(new DecisionStrategySingleton( + d_env, "sygus_feasible", d_feasible_guard, d_qstate.getValuation())); d_qim.getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); // this must be called, both to ensure that the feasible guard is diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 4da273cd9..64bc578a5 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -529,7 +529,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types) */ Assert(d_dstrat.find(q) == d_dstrat.end()); DecisionStrategy* ds = new DecisionStrategySingleton( - "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation()); + d_env, "CeLiteral", lit, d_qstate.getValuation()); d_dstrat[q].reset(ds); d_qim.getDecisionManager()->registerStrategy( diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6aa2a816a..7126d3567 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -43,13 +43,12 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) d_qim(nullptr), d_qreg(qr), d_termsContext(), - d_termsContextUse(options::termDbCd() ? qs.getSatContext() - : &d_termsContext), + d_termsContextUse(options::termDbCd() ? context() : &d_termsContext), d_processed(d_termsContextUse), d_typeMap(d_termsContextUse), d_ops(d_termsContextUse), d_opMap(d_termsContextUse), - d_inactive_map(qs.getSatContext()) + d_inactive_map(context()) { d_consistent_ee = true; d_true = NodeManager::currentNM()->mkConst(true); diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 98618f3f7..ab999ad9b 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -33,8 +33,8 @@ TermRegistry::TermRegistry(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) : EnvObj(env), - d_presolve(qs.getUserContext(), true), - d_presolveCache(qs.getUserContext()), + d_presolve(userContext(), true), + d_presolveCache(userContext()), d_termEnum(new TermEnumeration), d_termPools(new TermPools(env, qs)), d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr) |