From: Andrew Reynolds Date: Fri, 17 Dec 2021 19:43:36 +0000 (-0600) Subject: Refactoring initialization of proofs (#7834) X-Git-Tag: cvc5-1.0.0~641 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7cb2cd925220e063a67c7eed6f829520b58ce53;p=cvc5.git Refactoring initialization of proofs (#7834) Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env. --- diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index f97c5bafb..778931f70 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -117,7 +117,7 @@ void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn) replace(i, trn.getNode(), trn.getGenerator()); } -void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg) +void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg) { d_pppg = pppg; } diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index b6bd8a94c..5c75fba2b 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -158,8 +158,14 @@ class AssertionPipeline return d_storeSubstsInAsserts && i == d_substsIndex; } //------------------------------------ for proofs - /** Set proof generator */ - void setProofGenerator(smt::PreprocessProofGenerator* pppg); + /** + * Enable proofs for this assertions pipeline. This must be called + * explicitly since we construct the assertions pipeline before we know + * whether proofs are enabled. + * + * @param pppg The preprocess proof generator of the proof manager. + */ + void enableProofs(smt::PreprocessProofGenerator* pppg); /** Is proof enabled? */ bool isProofEnabled() const; //------------------------------------ end for proofs diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 247a8b72e..ff672b368 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -54,10 +54,10 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) d_statistics(statisticsRegistry()), d_pnm(d_env.getProofNodeManager()), d_llpg(d_pnm ? new smt::PreprocessProofGenerator( - d_pnm, userContext(), "NonClausalSimp::llpg") + d_env, userContext(), "NonClausalSimp::llpg") : nullptr), d_llra(d_pnm ? new LazyCDProof( - d_pnm, nullptr, userContext(), "NonClausalSimp::llra") + d_pnm, nullptr, userContext(), "NonClausalSimp::llra") : nullptr), d_tsubsList(userContext()) { diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 8d066c1ba..0191bcb82 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -251,9 +251,9 @@ void Assertions::ensureBoolean(const Node& n) } } -void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg) +void Assertions::enableProofs(smt::PreprocessProofGenerator* pppg) { - d_assertions.setProofGenerator(pppg); + d_assertions.enableProofs(pppg); } bool Assertions::isProofEnabled() const diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 5cda366e6..96e5712a4 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -126,8 +126,14 @@ class Assertions : protected EnvObj void flipGlobalNegated(); //------------------------------------ for proofs - /** Set proof generator */ - void setProofGenerator(smt::PreprocessProofGenerator* pppg); + /** + * Enable proofs for this assertions class. This must be called + * explicitly since we construct the assertions before we know + * whether proofs are enabled. + * + * @param pppg The preprocess proof generator of the proof manager. + */ + void enableProofs(smt::PreprocessProofGenerator* pppg); /** Is proof enabled? */ bool isProofEnabled() const; //------------------------------------ end for proofs diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 54aba6b71..dd0cd3610 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -34,7 +34,7 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -ExpandDefs::ExpandDefs(Env& env) : d_env(env), d_tpg(nullptr) {} +ExpandDefs::ExpandDefs(Env& env) : EnvObj(env), d_tpg(nullptr) {} ExpandDefs::~ExpandDefs() {} @@ -164,11 +164,13 @@ TrustNode ExpandDefs::expandDefinitions(TNode n, return TrustNode::mkTrustRewrite(orig, res, tpg); } -void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm) +void ExpandDefs::enableProofs() { + // initialize if not done already if (d_tpg == nullptr) { - d_tpg.reset(new TConvProofGenerator(pnm, + Assert(d_env.getProofNodeManager() != nullptr); + d_tpg.reset(new TConvProofGenerator(d_env.getProofNodeManager(), d_env.getUserContext(), TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 8ecf276e2..669f56430 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -22,10 +22,10 @@ #include "expr/node.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; class ProofNodeManager; class TConvProofGenerator; @@ -37,7 +37,7 @@ namespace smt { * Its main features is expandDefinitions(TNode, ...), which returns the * expanded formula of a term. */ -class ExpandDefs +class ExpandDefs : protected EnvObj { public: ExpandDefs(Env& env); @@ -51,11 +51,8 @@ class ExpandDefs */ Node expandDefinitions(TNode n, std::unordered_map& cache); - /** - * Set proof node manager, which signals this class to enable proofs using the - * given proof node manager. - */ - void setProofNodeManager(ProofNodeManager* pnm); + /** Enable proofs using the proof node manager of the env. */ + void enableProofs(); private: /** @@ -65,8 +62,6 @@ class ExpandDefs TrustNode expandDefinitions(TNode n, std::unordered_map& cache, TConvProofGenerator* tpg); - /** Reference to the environment. */ - Env& d_env; /** A proof generator for the term conversion. */ std::unique_ptr d_tpg; }; diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index e2730151e..19a776587 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -23,22 +23,19 @@ #include "proof/proof.h" #include "proof/proof_checker.h" #include "proof/proof_node.h" +#include "smt/env.h" #include "theory/quantifiers/extended_rewrite.h" -#include "theory/rewriter.h" namespace cvc5 { namespace smt { -PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, - context::Context* c, - std::string name, - PfRule ra, - PfRule rpp) - : d_pnm(pnm), +PreprocessProofGenerator::PreprocessProofGenerator( + Env& env, context::Context* c, std::string name, PfRule ra, PfRule rpp) + : EnvObj(env), d_ctx(c ? c : &d_context), d_src(d_ctx), - d_helperProofs(pnm, d_ctx), - d_inputPf(pnm, c, "InputProof"), + d_helperProofs(env.getProofNodeManager(), d_ctx), + d_inputPf(env.getProofNodeManager(), c, "InputProof"), d_name(name), d_ra(ra), d_rpp(rpp) @@ -131,7 +128,7 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) return nullptr; } // make CDProof to construct the proof below - CDProof cdp(d_pnm); + CDProof cdp(d_env.getProofNodeManager()); Node curr = f; std::vector transChildren; @@ -180,7 +177,7 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) if (!proofStepProcessed) { // maybe its just an (extended) rewrite? - Node pr = theory::Rewriter::callExtendedRewrite(proven[0]); + Node pr = extendedRewrite(proven[0]); if (proven[1] == pr) { Node idr = mkMethodId(MethodId::RW_EXT_REWRITE); @@ -244,8 +241,6 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) return cdp.getProofFor(f); } -ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; } - LazyCDProof* PreprocessProofGenerator::allocateHelperProof() { return d_helperProofs.allocateProof(nullptr, d_ctx); @@ -259,7 +254,7 @@ void PreprocessProofGenerator::checkEagerPedantic(PfRule r) { // catch a pedantic failure now, which otherwise would not be // triggered since we are doing lazy proof generation - ProofChecker* pc = d_pnm->getChecker(); + ProofChecker* pc = d_env.getProofNodeManager()->getChecker(); std::stringstream serr; if (pc->isPedanticFailure(r, serr)) { diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index a0e88b3e9..928ea7bf3 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -24,6 +24,7 @@ #include "proof/proof_generator.h" #include "proof/proof_set.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -53,13 +54,13 @@ namespace smt { * whose free assumptions are intended to be input assertions, which are * implictly all assertions that are not notified to this class. */ -class PreprocessProofGenerator : public ProofGenerator +class PreprocessProofGenerator : protected EnvObj, public ProofGenerator { typedef context::CDHashMap NodeTrustNodeMap; public: /** - * @param pnm The proof node manager + * @param env Reference to the environment * @param c The context this class depends on * @param name The name of this generator (for debugging) * @param ra The proof rule to use when no generator is provided for new @@ -67,7 +68,7 @@ class PreprocessProofGenerator : public ProofGenerator * @param rpp The proof rule to use when no generator is provided for * preprocessing steps. */ - PreprocessProofGenerator(ProofNodeManager* pnm, + PreprocessProofGenerator(Env& env, context::Context* c = nullptr, std::string name = "PreprocessProofGenerator", PfRule ra = PfRule::PREPROCESS_LEMMA, @@ -98,8 +99,6 @@ class PreprocessProofGenerator : public ProofGenerator std::shared_ptr getProofFor(Node f) override; /** Identify */ std::string identify() const override; - /** Get the proof manager */ - ProofNodeManager* getManager(); /** * Allocate a helper proof. This returns a fresh lazy proof object that * remains alive in the context. This feature is used to construct @@ -114,8 +113,6 @@ class PreprocessProofGenerator : public ProofGenerator * to this class. */ void checkEagerPedantic(PfRule r); - /** The proof node manager */ - ProofNodeManager* d_pnm; /** A dummy context used by this class if none is provided */ context::Context d_context; /** The context used here */ diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 0fdb569c8..d7167c04c 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -42,8 +42,7 @@ Preprocessor::Preprocessor(Env& env, d_propagator(env, true, true), d_assertionsProcessed(env.getUserContext(), false), d_exDefs(env), - d_processor(env, stats), - d_pnm(nullptr) + d_processor(env, stats) { } @@ -149,12 +148,11 @@ Node Preprocessor::simplify(const Node& node) return ret; } -void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) +void Preprocessor::enableProofs(PreprocessProofGenerator* pppg) { Assert(pppg != nullptr); - d_pnm = pppg->getManager(); - d_exDefs.setProofNodeManager(d_pnm); - d_propagator.setProof(d_pnm, userContext(), pppg); + d_exDefs.enableProofs(); + d_propagator.enableProofs(userContext(), pppg); } } // namespace smt diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 957b5e36e..c91d106f5 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -99,9 +99,13 @@ class Preprocessor : protected EnvObj /** Same as above, for a list of assertions, updating in place */ void expandDefinitions(std::vector& ns); /** - * Set proof node manager. Enables proofs in this preprocessor. + * Enable proofs for this preprocessor. This must be called + * explicitly since we construct the preprocessor before we know + * whether proofs are enabled. + * + * @param pppg The preprocess proof generator of the proof manager. */ - void setProofGenerator(PreprocessProofGenerator* pppg); + void enableProofs(PreprocessProofGenerator* pppg); private: /** Reference to the abstract values utility */ @@ -123,8 +127,6 @@ class Preprocessor : protected EnvObj * passes. */ ProcessAssertions d_processor; - /** Proof node manager */ - ProofNodeManager* d_pnm; }; } // namespace smt diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 04f601680..798f7dd57 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -43,13 +43,15 @@ PfManager::PfManager(Env& env) options().proof.proofPedantic)), d_pnm(new ProofNodeManager( env.getOptions(), env.getRewriter(), d_pchecker.get())), - d_pppg(new PreprocessProofGenerator( - d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), + d_pppg(nullptr), d_pfpp(nullptr), d_finalProof(nullptr) { // enable proof support in the environment/rewriter d_env.setProofNodeManager(d_pnm.get()); + // now construct preprocess proof generator + d_pppg = std::make_unique( + env, env.getUserContext(), "smt::PreprocessProofGenerator"); // Now, initialize the proof postprocessor with the environment. // By default the post-processor will update all assumptions, which // can lead to SCOPE subproofs of the form @@ -67,11 +69,11 @@ PfManager::PfManager(Env& env) // be inferred from A, it was updated). This shape is problematic for // the Alethe reconstruction, so we disable the update of scoped // assumptions (which would disable the update of B1 in this case). - d_pfpp.reset(new ProofPostproccess( + d_pfpp = std::make_unique( env, d_pppg.get(), nullptr, - options().proof.proofFormatMode != options::ProofFormatMode::ALETHE)); + options().proof.proofFormatMode != options::ProofFormatMode::ALETHE); // add rules to eliminate here if (options().proof.proofGranularityMode diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 32838eccf..13d061f1f 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -192,9 +192,9 @@ void SolverEngine::finishInit() // start the unsat core manager d_ucManager.reset(new UnsatCoreManager()); // enable it in the assertions pipeline - d_asserts->setProofGenerator(pppg); + d_asserts->enableProofs(pppg); // enabled proofs in the preprocessor - d_smtSolver->getPreprocessor()->setProofGenerator(pppg); + d_smtSolver->getPreprocessor()->enableProofs(pppg); } Trace("smt-debug") << "SolverEngine::finishInit" << std::endl; diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 95b31eab2..1299a493a 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -81,8 +81,6 @@ class AbstractValues; class Assertions; class ResourceOutListener; class SmtNodeManagerListener; -class OptionsManager; -class Preprocessor; class CheckModels; /** Subsolvers */ class SmtSolver; diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 714dcfb01..b570b6b36 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -767,21 +767,21 @@ TrustNode CircuitPropagator::propagate() return d_conflict; } -void CircuitPropagator::setProof(ProofNodeManager* pnm, - context::Context* ctx, - ProofGenerator* defParent) +void CircuitPropagator::enableProofs(context::Context* ctx, + ProofGenerator* defParent) { - d_pnm = pnm; - d_epg.reset(new EagerProofGenerator(pnm, ctx)); + d_pnm = d_env.getProofNodeManager(); + Assert(d_pnm != nullptr); + d_epg.reset(new EagerProofGenerator(d_pnm, ctx)); d_proofInternal.reset(new LazyCDProofChain( - pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain")); + d_pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain")); if (defParent != nullptr) { // If we provide a parent proof generator (defParent), we want the ASSUME // leafs of proofs provided by this class to call the getProofFor method on // the parent. To do this, we use a LazyCDProofChain. d_proofExternal.reset(new LazyCDProofChain( - pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain")); + d_pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain")); } } diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index fa55e2711..01bc0ad35 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -134,14 +134,12 @@ class CircuitPropagator : protected EnvObj return false; } /** - * Set proof node manager, context and parent proof generator. + * Enable proofs based on context and parent proof generator. * * If parent is non-null, then it is responsible for the proofs provided * to this class. */ - void setProof(ProofNodeManager* pnm, - context::Context* ctx, - ProofGenerator* defParent); + void enableProofs(context::Context* ctx, ProofGenerator* defParent); private: /** A context-notify object that clears out stale data. */