From: Andrew Reynolds Date: Wed, 13 Oct 2021 04:38:46 +0000 (-0500) Subject: Make (proof) equality engine use Env (#7336) X-Git-Tag: cvc5-1.0.0~1072 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45c91fb32195d4f8de014c8ef91814c6625bcf43;p=cvc5.git Make (proof) equality engine use Env (#7336) --- diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index e419f3ae1..4aee9e981 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -81,14 +81,13 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) if (options().arith.arithEqSolver) { // use our own copy - d_allocEe.reset( - new eq::EqualityEngine(d_notify, context(), "arithCong::ee", true)); + d_allocEe = std::make_unique( + d_env, context(), d_notify, "arithCong::ee", true); d_ee = d_allocEe.get(); if (d_pnm != nullptr) { // allocate an internal proof equality engine - d_allocPfee.reset( - new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm)); + d_allocPfee = std::make_unique(d_env, *d_ee); d_ee->setProofEqualityEngine(d_allocPfee.get()); } } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index cf31f0cb6..9e69c9f71 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -77,7 +77,7 @@ TheoryArrays::TheoryArrays(Env& env, name + "number of setModelVal splits")), d_numSetModelValConflicts(statisticsRegistry().registerInt( name + "number of setModelVal conflicts")), - d_ppEqualityEngine(userContext(), name + "pp", true), + d_ppEqualityEngine(d_env, userContext(), name + "pp", true), d_ppFacts(userContext()), d_rewriter(env.getRewriter(), d_pnm), d_state(env, valuation), @@ -85,7 +85,7 @@ TheoryArrays::TheoryArrays(Env& env, d_literalsToPropagate(context()), d_literalsToPropagateIndex(context(), 0), d_isPreRegistered(context()), - d_mayEqualEqualityEngine(context(), name + "mayEqual", true), + d_mayEqualEqualityEngine(d_env, context(), name + "mayEqual", true), d_notify(*this), d_infoMap(context(), name), d_mergeQueue(context()), diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp index a91aea94e..142853b95 100644 --- a/src/theory/ee_manager.cpp +++ b/src/theory/ee_manager.cpp @@ -41,10 +41,11 @@ eq::EqualityEngine* EqEngineManager::allocateEqualityEngine(EeSetupInfo& esi, if (esi.d_notify != nullptr) { return new eq::EqualityEngine( - *esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers); + d_env, c, *esi.d_notify, esi.d_name, esi.d_constantsAreTriggers); } // the theory doesn't care about explicit notifications - return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers); + return new eq::EqualityEngine( + d_env, c, esi.d_name, esi.d_constantsAreTriggers); } } // namespace theory diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp index 0e6610833..079cdd904 100644 --- a/src/theory/ee_manager_central.cpp +++ b/src/theory/ee_manager_central.cpp @@ -31,7 +31,8 @@ EqEngineManagerCentral::EqEngineManagerCentral(Env& env, d_masterEENotify(nullptr), d_masterEqualityEngine(nullptr), d_centralEENotify(*this), - d_centralEqualityEngine(d_centralEENotify, context(), "central::ee", true) + d_centralEqualityEngine( + env, context(), d_centralEENotify, "central::ee", true) { for (TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; @@ -41,10 +42,8 @@ EqEngineManagerCentral::EqEngineManagerCentral(Env& env, } if (env.isTheoryProofProducing()) { - d_centralPfee.reset(new eq::ProofEqEngine(context(), - userContext(), - d_centralEqualityEngine, - env.getProofNodeManager())); + d_centralPfee = + std::make_unique(env, d_centralEqualityEngine); d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get()); } } @@ -112,8 +111,8 @@ void EqEngineManagerCentral::initializeTheories() d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe)); if (!masterEqToCentral) { - d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine( - *d_masterEENotify.get(), c, "master::ee", false)); + d_masterEqualityEngineAlloc = std::make_unique( + d_env, c, *d_masterEENotify.get(), "master::ee", false); d_masterEqualityEngine = d_masterEqualityEngineAlloc.get(); } else diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 6dee1910b..1de625d48 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -58,8 +58,8 @@ void EqEngineManagerDistributed::initializeTheories() QuantifiersEngine* qe = d_te.getQuantifiersEngine(); Assert(qe != nullptr); d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe)); - d_masterEqualityEngine.reset(new eq::EqualityEngine( - *d_masterEENotify.get(), c, "theory::master", false)); + d_masterEqualityEngine = std::make_unique( + d_env, c, *d_masterEENotify.get(), "theory::master", false); } // allocate equality engines per theory for (TheoryId theoryId = theory::THEORY_FIRST; diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 3b4babe75..5a5d97064 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -42,7 +42,8 @@ CandidateRewriteDatabase::CandidateRewriteDatabase( d_rewAccel(rewAccel), d_silent(silent), d_filterPairs(filterPairs), - d_using_sygus(false) + d_using_sygus(false), + d_crewrite_filter(env) { } void CandidateRewriteDatabase::initialize(const std::vector& vars, diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index da3e506fc..e856f1519 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -30,8 +30,9 @@ namespace quantifiers { // the number of d_drewrite objects we have allocated (to avoid name conflicts) static unsigned drewrite_counter = 0; -CandidateRewriteFilter::CandidateRewriteFilter() - : d_ss(nullptr), +CandidateRewriteFilter::CandidateRewriteFilter(Env& env) + : EnvObj(env), + d_ss(nullptr), d_tds(nullptr), d_use_sygus_type(false), d_drewrite(nullptr), @@ -53,8 +54,8 @@ void CandidateRewriteFilter::initialize(SygusSampler* ss, std::stringstream ssn; ssn << "_dyn_rewriter_" << drewrite_counter; drewrite_counter++; - d_drewrite = std::unique_ptr( - new DynamicRewriter(ssn.str(), &d_fakeContext)); + d_drewrite = + std::make_unique(d_env, &d_fakeContext, ssn.str()); } 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 527632786..d92a9b40c 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -21,7 +21,9 @@ #define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H #include + #include "expr/match_trie.h" +#include "smt/env_obj.h" #include "theory/quantifiers/dynamic_rewrite.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/sygus_sampler.h" @@ -46,10 +48,10 @@ namespace quantifiers { * pairs". A relevant pair ( t, s ) typically corresponds to a (candidate) * rewrite t = s. */ -class CandidateRewriteFilter +class CandidateRewriteFilter : protected EnvObj { public: - CandidateRewriteFilter(); + CandidateRewriteFilter(Env& env); /** initialize * diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index da8727c12..b98088a71 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -93,7 +93,8 @@ ConjectureGenerator::ConjectureGenerator(Env& env, TermRegistry& tr) : QuantifiersModule(env, qs, qim, qr, tr), d_notify(*this), - d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false), + d_uequalityEngine( + env, context(), d_notify, "ConjectureGenerator::ee", false), d_ee_conjectures(context()), d_conj_count(0), d_subs_confirmCount(0), diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index 1fc08b288..79b509533 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/dynamic_rewrite.h" #include "expr/skolem_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" using namespace std; @@ -25,8 +26,10 @@ namespace cvc5 { namespace theory { namespace quantifiers { -DynamicRewriter::DynamicRewriter(const std::string& name, context::Context* c) - : d_equalityEngine(c, "DynamicRewriter::" + name, true), d_rewrites(c) +DynamicRewriter::DynamicRewriter(Env& env, + context::Context* c, + const std::string& name) + : d_equalityEngine(env, 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 5e1f45b35..e20f5eea6 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -24,6 +24,9 @@ #include "theory/uf/equality_engine.h" namespace cvc5 { + +class Env; + namespace theory { namespace quantifiers { @@ -55,7 +58,7 @@ class DynamicRewriter typedef context::CDList NodeList; public: - DynamicRewriter(const std::string& name, context::Context* c); + DynamicRewriter(Env& env, context::Context* c, const std::string& name); ~DynamicRewriter() {} /** inform this class that the equality a = b holds. */ void addRewrite(Node a, Node b); diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 6c0f6ae10..9503d1378 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -52,9 +52,7 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee) d_pfee = d_equalityEngine->getProofEqualityEngine(); if (d_pfee == nullptr) { - ProofNodeManager* pnm = d_env.getProofNodeManager(); - d_pfeeAlloc.reset(new eq::ProofEqEngine( - d_env.getContext(), d_env.getUserContext(), *ee, pnm)); + d_pfeeAlloc = std::make_unique(d_env, *ee); d_pfee = d_pfeeAlloc.get(); d_equalityEngine->setProofEqualityEngine(d_pfee); } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 415672e97..9844d13bc 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -132,8 +132,12 @@ void Theory::finishInitStandalone() if (needsEqualityEngine(esi)) { // always associated with the same SAT context as the theory - d_allocEqualityEngine.reset(new eq::EqualityEngine( - *esi.d_notify, context(), esi.d_name, esi.d_constantsAreTriggers)); + d_allocEqualityEngine = + std::make_unique(d_env, + context(), + *esi.d_notify, + esi.d_name, + esi.d_constantsAreTriggers); // use it as the official equality engine setEqualityEngine(d_allocEqualityEngine.get()); } diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 1699e91ad..22b5e9c44 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -76,8 +76,7 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) d_pfee = d_ee->getProofEqualityEngine(); if (d_pfee == nullptr) { - d_pfeeAlloc.reset( - new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm)); + d_pfeeAlloc = std::make_unique(d_env, *d_ee); d_pfee = d_pfeeAlloc.get(); d_ee->setProofEqualityEngine(d_pfee); } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 34704181c..a62bf876c 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -20,6 +20,7 @@ #include "base/output.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/uf/eq_proof.h" @@ -99,59 +100,63 @@ EqualityEngine::~EqualityEngine() { free(d_triggerDatabase); } -EqualityEngine::EqualityEngine(context::Context* context, +EqualityEngine::EqualityEngine(Env& env, + context::Context* c, std::string name, bool constantsAreTriggers, bool anyTermTriggers) - : ContextNotifyObj(context), + : ContextNotifyObj(c), d_masterEqualityEngine(0), - d_context(context), - d_done(context, false), + d_env(env), + d_context(c), + d_done(c, false), d_notify(&s_notifyNone), - d_applicationLookupsCount(context, 0), - d_nodesCount(context, 0), - d_assertedEqualitiesCount(context, 0), - d_equalityTriggersCount(context, 0), - d_subtermEvaluatesSize(context, 0), + d_applicationLookupsCount(c, 0), + d_nodesCount(c, 0), + d_assertedEqualitiesCount(c, 0), + d_equalityTriggersCount(c, 0), + d_subtermEvaluatesSize(c, 0), d_stats(name + "::"), d_inPropagate(false), d_constantsAreTriggers(constantsAreTriggers), d_anyTermsAreTriggers(anyTermTriggers), - d_triggerDatabaseSize(context, 0), - d_triggerTermSetUpdatesSize(context, 0), - d_deducedDisequalitiesSize(context, 0), - d_deducedDisequalityReasonsSize(context, 0), - d_propagatedDisequalities(context), + d_triggerDatabaseSize(c, 0), + d_triggerTermSetUpdatesSize(c, 0), + d_deducedDisequalitiesSize(c, 0), + d_deducedDisequalityReasonsSize(c, 0), + d_propagatedDisequalities(c), d_name(name) { init(); } -EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, - context::Context* context, +EqualityEngine::EqualityEngine(Env& env, + context::Context* c, + EqualityEngineNotify& notify, std::string name, bool constantsAreTriggers, bool anyTermTriggers) - : ContextNotifyObj(context), + : ContextNotifyObj(c), d_masterEqualityEngine(nullptr), d_proofEqualityEngine(nullptr), - d_context(context), - d_done(context, false), + d_env(env), + d_context(c), + d_done(c, false), d_notify(&s_notifyNone), - d_applicationLookupsCount(context, 0), - d_nodesCount(context, 0), - d_assertedEqualitiesCount(context, 0), - d_equalityTriggersCount(context, 0), - d_subtermEvaluatesSize(context, 0), + d_applicationLookupsCount(c, 0), + d_nodesCount(c, 0), + d_assertedEqualitiesCount(c, 0), + d_equalityTriggersCount(c, 0), + d_subtermEvaluatesSize(c, 0), d_stats(name + "::"), d_inPropagate(false), d_constantsAreTriggers(constantsAreTriggers), d_anyTermsAreTriggers(anyTermTriggers), - d_triggerDatabaseSize(context, 0), - d_triggerTermSetUpdatesSize(context, 0), - d_deducedDisequalitiesSize(context, 0), - d_deducedDisequalityReasonsSize(context, 0), - d_propagatedDisequalities(context), + d_triggerDatabaseSize(c, 0), + d_triggerTermSetUpdatesSize(c, 0), + d_deducedDisequalitiesSize(c, 0), + d_deducedDisequalityReasonsSize(c, 0), + d_propagatedDisequalities(c), d_name(name) { init(); @@ -1849,7 +1854,7 @@ Node EqualityEngine::evaluateTerm(TNode node) { builder << childRep; } Node newNode = builder; - return Rewriter::rewrite(newNode); + return d_env.getRewriter()->rewrite(newNode); } void EqualityEngine::processEvaluationQueue() { diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 0710ac6c7..232f90595 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -37,6 +37,9 @@ #include "util/statistics_stats.h" namespace cvc5 { + +class Env; + namespace theory { namespace eq { @@ -70,11 +73,16 @@ class EqualityEngine : public context::ContextNotifyObj { /** * Initialize the equality engine, given the notification class. * + * @param env The environment, which is used for rewriting + * @param c The context which this equality engine depends, which is typically + * although not necessarily same as the SAT context of env. + * @param name The name of this equality engine, for statistics * @param constantTriggers Whether we treat constants as trigger terms * @param anyTermTriggers Whether we use any terms as triggers */ - EqualityEngine(EqualityEngineNotify& notify, - context::Context* context, + EqualityEngine(Env& env, + context::Context* c, + EqualityEngineNotify& notify, std::string name, bool constantTriggers, bool anyTermTriggers = true); @@ -82,7 +90,8 @@ class EqualityEngine : public context::ContextNotifyObj { /** * Initialize the equality engine with no notification class. */ - EqualityEngine(context::Context* context, + EqualityEngine(Env& env, + context::Context* c, std::string name, bool constantsAreTriggers, bool anyTermTriggers = true); @@ -120,7 +129,9 @@ class EqualityEngine : public context::ContextNotifyObj { Statistics(const std::string& name); };/* struct EqualityEngine::statistics */ -private: + private: + /** The environment we are using */ + Env& d_env; /** The context we are using */ context::Context* d_context; diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index b6e445334..71688fc15 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -18,6 +18,7 @@ #include "proof/lazy_proof_chain.h" #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" #include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine.h" @@ -29,22 +30,24 @@ namespace cvc5 { namespace theory { namespace eq { -ProofEqEngine::ProofEqEngine(context::Context* c, - context::Context* lc, - EqualityEngine& ee, - ProofNodeManager* pnm) - : EagerProofGenerator(pnm, lc, "pfee::" + ee.identify()), +ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee) + : EagerProofGenerator(env.getProofNodeManager(), + env.getUserContext(), + "pfee::" + ee.identify()), d_ee(ee), - d_factPg(c, pnm), - d_assumpPg(pnm), - d_pnm(pnm), - d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()), - d_keep(c) + d_factPg(env.getContext(), env.getProofNodeManager()), + d_assumpPg(env.getProofNodeManager()), + d_pnm(env.getProofNodeManager()), + d_proof(env.getProofNodeManager(), + nullptr, + env.getContext(), + "pfee::LazyCDProof::" + ee.identify()), + d_keep(env.getContext()) { NodeManager* nm = NodeManager::currentNM(); d_true = nm->mkConst(true); d_false = nm->mkConst(false); - AlwaysAssert(pnm != nullptr) + AlwaysAssert(env.getProofNodeManager() != nullptr) << "Should not construct ProofEqEngine without proof node manager"; } diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 9ebdd03e5..fc8520dd1 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -30,6 +30,7 @@ namespace cvc5 { +class Env; class ProofNode; class ProofNodeManager; @@ -86,15 +87,10 @@ class ProofEqEngine : public EagerProofGenerator public: /** - * @param c The SAT context - * @param lc The context lemmas live in + * @param env The environment * @param ee The equality engine this is layered on - * @param pnm The proof node manager for producing proof nodes. */ - ProofEqEngine(context::Context* c, - context::Context* lc, - EqualityEngine& ee, - ProofNodeManager* pnm); + ProofEqEngine(Env& env, EqualityEngine& ee); ~ProofEqEngine() {} //-------------------------- assert fact /**