From: Andrew Reynolds Date: Wed, 6 Oct 2021 15:12:17 +0000 (-0500) Subject: Eliminate more hard coded uses of user context (#7309) X-Git-Tag: cvc5-1.0.0~1120 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b9fef64a317128b94dbf266ee50a30f6f3a64ac;p=cvc5.git Eliminate more hard coded uses of user context (#7309) This is in preparation to make the "lemma context" configurable. --- diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index f7d274484..e419f3ae1 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -53,8 +53,6 @@ ArithCongruenceManager::ArithCongruenceManager( d_setupLiteral(setup), d_avariables(avars), d_ee(nullptr), - d_satContext(context()), - d_userContext(userContext()), d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() : nullptr), // Construct d_pfGenEe with the SAT context, since its proof include @@ -84,13 +82,13 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) { // use our own copy d_allocEe.reset( - new eq::EqualityEngine(d_notify, d_satContext, "arithCong::ee", true)); + new eq::EqualityEngine(d_notify, context(), "arithCong::ee", true)); d_ee = d_allocEe.get(); if (d_pnm != nullptr) { // allocate an internal proof equality engine d_allocPfee.reset( - new eq::ProofEqEngine(d_satContext, d_userContext, *d_ee, d_pnm)); + new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm)); d_ee->setProofEqualityEngine(d_allocPfee.get()); } } diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 3050f5821..b847c63ae 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -114,11 +114,6 @@ class ArithCongruenceManager : protected EnvObj eq::EqualityEngine* d_ee; /** The equality engine we allocated */ std::unique_ptr d_allocEe; - /** The sat context */ - context::Context* d_satContext; - /** The user context */ - context::UserContext* d_userContext; - /** proof manager */ ProofNodeManager* d_pnm; /** A proof generator for storing proofs of facts that are asserted to the EQ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 207907fcc..a970abc45 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -47,7 +47,7 @@ NonlinearExtension::NonlinearExtension(Env& env, d_hasNlTerms(false), d_checkCounter(0), d_extTheoryCb(state.getEqualityEngine()), - d_extTheory(d_extTheoryCb, context(), userContext(), d_im), + d_extTheory(env, d_extTheoryCb, d_im), d_model(), d_trSlv(d_im, d_model, d_env), d_extState(d_im, d_model, d_env), diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 627129c3a..9eb6e3cdc 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -81,18 +81,16 @@ bool ExtTheoryCallback::getReduction(int effort, return false; } -ExtTheory::ExtTheory(ExtTheoryCallback& p, - context::Context* c, - context::UserContext* u, - TheoryInferenceManager& im) - : d_parent(p), +ExtTheory::ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im) + : EnvObj(env), + d_parent(p), d_im(im), - d_ext_func_terms(c), - d_extfExtReducedIdMap(c), - d_ci_inactive(u), - d_has_extf(c), - d_lemmas(u), - d_pp_lemmas(u) + d_ext_func_terms(context()), + d_extfExtReducedIdMap(context()), + d_ci_inactive(userContext()), + d_has_extf(context()), + d_lemmas(userContext()), + d_pp_lemmas(userContext()) { d_true = NodeManager::currentNM()->mkConst(true); } @@ -260,7 +258,7 @@ bool ExtTheory::doInferencesInternal(int effort, bool processed = false; if (sterms[i] != terms[i]) { - Node sr = Rewriter::rewrite(sterms[i]); + Node sr = rewrite(sterms[i]); // ask the theory if this term is reduced, e.g. is it constant or it // is a non-extf term. ExtReducedId id; diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index 01b191e0a..998dac146 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -41,6 +41,7 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/theory_inference_manager.h" namespace cvc5 { @@ -163,7 +164,7 @@ class ExtTheoryCallback * underlying theory for a "derivable substitution", whereby extended functions * may be reducable. */ -class ExtTheory +class ExtTheory : protected EnvObj { using NodeBoolMap = context::CDHashMap; using NodeExtReducedIdMap = context::CDHashMap; @@ -174,10 +175,7 @@ class ExtTheory * * If cacheEnabled is false, we do not cache results of getSubstitutedTerm. */ - ExtTheory(ExtTheoryCallback& p, - context::Context* c, - context::UserContext* u, - TheoryInferenceManager& im); + ExtTheory(Env& env, ExtTheoryCallback& p, TheoryInferenceManager& im); virtual ~ExtTheory() {} /** Tells this class to treat terms with Kind k as extended functions */ void addFunctionKind(Kind k) { d_extf_kind[k] = true; } diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index d5f06b6e9..da3e506fc 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -54,7 +54,7 @@ void CandidateRewriteFilter::initialize(SygusSampler* ss, ssn << "_dyn_rewriter_" << drewrite_counter; drewrite_counter++; d_drewrite = std::unique_ptr( - new DynamicRewriter(ssn.str(), &d_fake_context)); + new DynamicRewriter(ssn.str(), &d_fakeContext)); } bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index 4995dc7c2..527632786 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -104,8 +104,8 @@ class CandidateRewriteFilter bool d_use_sygus_type; //----------------------------congruence filtering - /** a (dummy) user context, used for d_drewrite */ - context::UserContext d_fake_context; + /** a (dummy) context, used for d_drewrite */ + context::Context d_fakeContext; /** dynamic rewriter class */ std::unique_ptr d_drewrite; //----------------------------end congruence filtering diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index 4d69ea732..1fc08b288 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -25,9 +25,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -DynamicRewriter::DynamicRewriter(const std::string& name, - context::UserContext* u) - : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u) +DynamicRewriter::DynamicRewriter(const std::string& name, context::Context* c) + : d_equalityEngine(c, "DynamicRewriter::" + name, true), d_rewrites(c) { d_equalityEngine.addFunctionKind(kind::APPLY_UF); } diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 3187b7c03..5e1f45b35 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -55,7 +55,7 @@ class DynamicRewriter typedef context::CDList NodeList; public: - DynamicRewriter(const std::string& name, context::UserContext* u); + DynamicRewriter(const std::string& name, context::Context* c); ~DynamicRewriter() {} /** inform this class that the equality a = b holds. */ void addRewrite(Node a, Node b); diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index e1a342178..a83167591 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -25,10 +25,9 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { -RelevanceManager::RelevanceManager(context::UserContext* userContext, - Valuation val) +RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val) : d_val(val), - d_input(userContext), + d_input(lemContext), d_computed(false), d_success(false), d_trackRSetExp(false), @@ -36,7 +35,7 @@ RelevanceManager::RelevanceManager(context::UserContext* userContext, { if (options::produceDifficulty()) { - d_dman.reset(new DifficultyManager(userContext, val)); + d_dman.reset(new DifficultyManager(lemContext, val)); d_trackRSetExp = true; // we cannot miniscope AND at the top level, since we need to // preserve the exact form of preprocessed assertions so the dependencies diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index f8cd8e1ee..287694445 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -76,7 +76,11 @@ class RelevanceManager typedef context::CDList NodeList; public: - RelevanceManager(context::UserContext* userContext, Valuation val); + /** + * @param lemContext The context which lemmas live at + * @param val The valuation class, for computing what is relevant. + */ + RelevanceManager(context::Context* lemContext, Valuation val); /** * Notify (preprocessed) assertions. This is called for input formulas or * lemmas that need justification that have been fully processed, just before diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index e4f1b6fab..6c0f6ae10 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -37,8 +37,6 @@ SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine) d_theoryEngine(theoryEngine), d_inConflict(env.getContext(), false), d_conflictPolarity(), - d_satContext(env.getContext()), - d_userContext(env.getUserContext()), d_equalityEngine(nullptr), d_pfee(nullptr) { @@ -55,8 +53,8 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee) if (d_pfee == nullptr) { ProofNodeManager* pnm = d_env.getProofNodeManager(); - d_pfeeAlloc.reset( - new eq::ProofEqEngine(d_satContext, d_userContext, *ee, pnm)); + d_pfeeAlloc.reset(new eq::ProofEqEngine( + d_env.getContext(), d_env.getUserContext(), *ee, pnm)); d_pfee = d_pfeeAlloc.get(); d_equalityEngine->setProofEqualityEngine(d_pfee); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 3b21c27a8..2bdb9d574 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -266,10 +266,6 @@ class SharedTermsDatabase : public context::ContextNotifyObj { * This method gets called on backtracks from the context manager. */ void contextNotifyPop() override { backtrack(); } - /** The SAT search context. */ - context::Context* d_satContext; - /** The user level assertion context. */ - context::UserContext* d_userContext; /** Equality engine */ theory::eq::EqualityEngine* d_equalityEngine; /** Proof equality engine, if we allocated one */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ac6d9b611..27640341a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -59,7 +59,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_termReg(env, d_state, d_statistics, d_pnm), d_extTheoryCb(), d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), - d_extTheory(d_extTheoryCb, context(), userContext(), d_im), + d_extTheory(env, d_extTheoryCb, d_im), d_rewriter(env.getRewriter(), &d_statistics.d_rewrites), d_bsolver(env, d_state, d_im), d_csolver(env, d_state, d_im, d_termReg, d_bsolver), diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 073accdae..eaa9a1746 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -24,8 +24,8 @@ using namespace cvc5::kind; namespace cvc5 { TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, - context::UserContext* u) - : d_pnm(pnm), d_proofs(u) + context::Context* c) + : d_pnm(pnm), d_proofs(c) { d_false = NodeManager::currentNM()->mkConst(false); } diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index 68f7dea32..1cb99b039 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -42,7 +42,7 @@ class TheoryEngineProofGenerator : public ProofGenerator NodeLazyCDProofMap; public: - TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u); + TheoryEngineProofGenerator(ProofNodeManager* pnm, context::Context* c); ~TheoryEngineProofGenerator() {} /** * Make trust explanation. Called when lpf has a proof of lit from free diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index ca8b3f740..b6e445334 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -30,10 +30,10 @@ namespace theory { namespace eq { ProofEqEngine::ProofEqEngine(context::Context* c, - context::UserContext* u, + context::Context* lc, EqualityEngine& ee, ProofNodeManager* pnm) - : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()), + : EagerProofGenerator(pnm, lc, "pfee::" + ee.identify()), d_ee(ee), d_factPg(c, pnm), d_assumpPg(pnm), diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index baf155dac..9ebdd03e5 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -85,8 +85,14 @@ class ProofEqEngine : public EagerProofGenerator typedef context::CDHashMap> NodeProofMap; public: + /** + * @param c The SAT context + * @param lc The context lemmas live in + * @param ee The equality engine this is layered on + * @param pnm The proof node manager for producing proof nodes. + */ ProofEqEngine(context::Context* c, - context::UserContext* u, + context::Context* lc, EqualityEngine& ee, ProofNodeManager* pnm); ~ProofEqEngine() {}