From: Andrew Reynolds Date: Tue, 7 Sep 2021 21:39:52 +0000 (-0500) Subject: Refactoring of proof manager initialization (#7073) X-Git-Tag: cvc5-1.0.0~1264 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e607ce390cff26aa14862b2f9c1da727d14cdf68;p=cvc5.git Refactoring of proof manager initialization (#7073) No longer takes a backwards reference to SmtEngine. Also takes minor changes to proof post-processor from proof-new. --- diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index b741ec5d5..0225cf24c 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -59,6 +59,14 @@ name = "Proof" name = "none" help = "do not check rule applications" +[[option]] + name = "proofPpMerge" + category = "regular" + long = "proof-pp-merge" + type = "bool" + default = "true" + help = "merge subproofs in final proof post-processor" + [[option]] name = "proofGranularityMode" category = "regular" diff --git a/src/smt/env.h b/src/smt/env.h index e54f12fa5..d95e70226 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -40,6 +40,7 @@ class UserContext; namespace smt { class DumpManager; +class PfManager; } namespace theory { @@ -56,6 +57,7 @@ class TrustSubstitutionMap; class Env { friend class SmtEngine; + friend class smt::PfManager; public: /** diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index ae5de49e9..2c3a22a78 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -31,37 +31,42 @@ namespace cvc5 { namespace smt { -PfManager::PfManager(Env& env, SmtEngine* smte) - : d_env(env), +PfManager::PfManager(Env& env) + : EnvObj(env), d_pchecker(new ProofChecker( - d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER, - d_env.getOptions().proof.proofPedantic)), + options().proof.proofCheck == options::ProofCheckMode::EAGER, + options().proof.proofPedantic)), d_pnm(new ProofNodeManager(d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), - d_pfpp(new ProofPostproccess( - d_pnm.get(), - smte, - d_pppg.get(), - // by default the post-processor will update all assumptions, which - // can lead to SCOPE subproofs of the form - // A - // ... - // B1 B2 - // ... ... - // ------------ - // C - // ------------- SCOPE [B1, B2] - // B1 ^ B2 => C - // - // where A is an available assumption from outside the scope (note - // that B1 was an assumption of this SCOPE subproof but since it could - // be inferred from A, it was updated). This shape is problematic for - // the veriT reconstruction, so we disable the update of scoped - // assumptions (which would disable the update of B1 in this case). - options::proofFormatMode() != options::ProofFormatMode::VERIT)), + d_pfpp(nullptr), d_finalProof(nullptr) { + // enable proof support in the environment/rewriter + d_env.setProofNodeManager(d_pnm.get()); + // 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 + // A + // ... + // B1 B2 + // ... ... + // ------------ + // C + // ------------- SCOPE [B1, B2] + // B1 ^ B2 => C + // + // where A is an available assumption from outside the scope (note + // that B1 was an assumption of this SCOPE subproof but since it could + // be inferred from A, it was updated). This shape is problematic for + // the veriT reconstruction, so we disable the update of scoped + // assumptions (which would disable the update of B1 in this case). + d_pfpp.reset(new ProofPostproccess( + env, + d_pppg.get(), + nullptr, + options::proofFormatMode() != options::ProofFormatMode::VERIT)); + // add rules to eliminate here if (options::proofGranularityMode() != options::ProofGranularityMode::OFF) { @@ -159,6 +164,7 @@ void PfManager::printProof(std::ostream& out, // TODO (proj #37) according to the proof format, post process the proof node // TODO (proj #37) according to the proof format, print the proof node + // according to the proof format, post process and print the proof node if (options::proofFormatMode() == options::ProofFormatMode::DOT) { proof::DotPrinter dotPrinter; @@ -166,13 +172,16 @@ void PfManager::printProof(std::ostream& out, } else if (options::proofFormatMode() == options::ProofFormatMode::TPTP) { - out << "% SZS output start Proof for " << d_env.getOptions().driver.filename << std::endl; + out << "% SZS output start Proof for " << options().driver.filename + << std::endl; // TODO (proj #37) print in TPTP compliant format out << *fp << std::endl; - out << "% SZS output end Proof for " << d_env.getOptions().driver.filename << std::endl; + out << "% SZS output end Proof for " << options().driver.filename + << std::endl; } else { + // otherwise, print using default printer out << "(proof\n"; out << *fp; out << "\n)\n"; @@ -190,6 +199,8 @@ ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); } ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); } +rewriter::RewriteDb* PfManager::getRewriteDatabase() const { return nullptr; } + smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const { return d_pppg.get(); diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index fd24f62f6..034a4554f 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -20,15 +20,19 @@ #include "context/cdhashmap.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; class ProofChecker; class ProofNode; class ProofNodeManager; class SmtEngine; +namespace rewriter { +class RewriteDb; +} + namespace smt { class Assertions; @@ -68,10 +72,10 @@ class ProofPostproccess; * - If SmtEngine has been configured in a way that is incompatible with proofs * then unsat core production will be disabled. */ -class PfManager +class PfManager : protected EnvObj { public: - PfManager(Env& env, SmtEngine* smte); + PfManager(Env& env); ~PfManager(); /** * Print the proof on the given output stream. @@ -103,6 +107,8 @@ class PfManager ProofChecker* getProofChecker() const; /** Get a pointer to the ProofNodeManager owned by this. */ ProofNodeManager* getProofNodeManager() const; + /** Get the rewrite database, containing definitions of rewrites from DSL. */ + rewriter::RewriteDb* getRewriteDatabase() const; /** Get the proof generator for proofs of preprocessing. */ smt::PreprocessProofGenerator* getPreprocessProofGenerator() const; //--------------------------- end access to utilities @@ -117,8 +123,6 @@ class PfManager */ void getAssertions(Assertions& as, std::vector& assertions); - /** Reference to the env of SmtEngine */ - Env& d_env; /** The false node */ Node d_false; /** For the new proofs module */ @@ -129,6 +133,7 @@ class PfManager std::unique_ptr d_pppg; /** The proof post-processor */ std::unique_ptr d_pfpp; + /** * The final proof produced by the SMT engine. * Combines the proofs of preprocessing, prop engine and theory engine, to be diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 5ad311f8d..9db8f1020 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -17,10 +17,10 @@ #include "expr/skolem_manager.h" #include "options/proof_options.h" -#include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "proof/proof_node_manager.h" #include "smt/smt_engine.h" +#include "theory/arith/arith_utilities.h" #include "theory/builtin/proof_checker.h" #include "theory/bv/bitblast/proof_bitblaster.h" #include "theory/rewriter.h" @@ -34,14 +34,14 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm, - SmtEngine* smte, +ProofPostprocessCallback::ProofPostprocessCallback(Env& env, ProofGenerator* pppg, + rewriter::RewriteDb* rdb, bool updateScopedAssumptions) - : d_pnm(pnm), - d_smte(smte), + : d_env(env), + d_pnm(env.getProofNodeManager()), d_pppg(pppg), - d_wfpm(pnm), + d_wfpm(env.getProofNodeManager()), d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); @@ -949,6 +949,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, { // get the kind of rewrite MethodId idr = MethodId::RW_REWRITE; + TheoryId theoryId = Theory::theoryOf(args[0]); if (args.size() >= 2) { getMethodId(args[1], idr); @@ -963,7 +964,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // rewrites from theory::Rewriter bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT); // use rewrite with proof interface - Rewriter* rr = d_smte->getRewriter(); + Rewriter* rr = d_env.getRewriter(); TrustNode trn = rr->rewriteWithProof(args[0], isExtEq); std::shared_ptr pfn = trn.toProofNode(); if (pfn == nullptr) @@ -975,7 +976,6 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, { // update to THEORY_REWRITE with idr Assert(args.size() >= 1); - TheoryId theoryId = Theory::theoryOf(args[0].getType()); Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]}); } @@ -1001,8 +1001,20 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } else { - // don't know how to eliminate - return Node::null(); + // try to reconstruct as a standalone rewrite + std::vector targs; + targs.push_back(eq); + targs.push_back( + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId)); + // in this case, must be a non-standard rewrite kind + Assert(args.size() >= 2); + targs.push_back(args[1]); + Node eqp = expandMacros(PfRule::THEORY_REWRITE, {}, targs, cdp); + if (eqp.isNull()) + { + // don't know how to eliminate + return Node::null(); + } } if (args[0] == ret) { @@ -1194,16 +1206,15 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq, return true; } -ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, - SmtEngine* smte, +ProofPostproccess::ProofPostproccess(Env& env, ProofGenerator* pppg, + rewriter::RewriteDb* rdb, bool updateScopedAssumptions) - : d_pnm(pnm), - d_cb(pnm, smte, pppg, updateScopedAssumptions), + : d_cb(env, pppg, rdb, updateScopedAssumptions), // the update merges subproofs - d_updater(d_pnm, d_cb, true), - d_finalCb(pnm), - d_finalizer(d_pnm, d_finalCb) + d_updater(env.getProofNodeManager(), d_cb, options::proofPpMerge()), + d_finalCb(env.getProofNodeManager()), + d_finalizer(env.getProofNodeManager(), d_finalCb) { } diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index 1aa52dd50..c0cc7bc17 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -30,7 +30,11 @@ namespace cvc5 { -class SmtEngine; +class Env; + +namespace rewriter { +class RewriteDb; +} namespace smt { @@ -41,9 +45,9 @@ namespace smt { class ProofPostprocessCallback : public ProofNodeUpdaterCallback { public: - ProofPostprocessCallback(ProofNodeManager* pnm, - SmtEngine* smte, + ProofPostprocessCallback(Env& env, ProofGenerator* pppg, + rewriter::RewriteDb* rdb, bool updateScopedAssumptions); ~ProofPostprocessCallback() {} /** @@ -73,10 +77,10 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback private: /** Common constants */ Node d_true; - /** The proof node manager */ + /** Reference to the env */ + Env& d_env; + /** Pointer to the proof node manager */ ProofNodeManager* d_pnm; - /** Pointer to the SmtEngine, which should have proofs enabled */ - SmtEngine* d_smte; /** The preprocessing proof generator */ ProofGenerator* d_pppg; /** The witness form proof generator */ @@ -248,16 +252,15 @@ class ProofPostproccess { public: /** - * @param pnm The proof node manager we are using - * @param smte The SMT engine whose proofs are being post-processed + * @param env The environment we are using * @param pppg The proof generator for pre-processing proofs * @param updateScopedAssumptions Whether we post-process assumptions in * scope. Since doing so is sound and only problematic depending on who is * consuming the proof, it's true by default. */ - ProofPostproccess(ProofNodeManager* pnm, - SmtEngine* smte, + ProofPostproccess(Env& env, ProofGenerator* pppg, + rewriter::RewriteDb* rdb, bool updateScopedAssumptions = true); ~ProofPostproccess(); /** post-process */ @@ -266,8 +269,6 @@ class ProofPostproccess void setEliminateRule(PfRule rule); private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The post process callback */ ProofPostprocessCallback d_cb; /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 582ca0c2c..cd8bd1d7b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -194,20 +194,15 @@ void SmtEngine::finishInit() SetDefaults sdefaults(d_isInternalSubsolver); sdefaults.setDefaults(d_env->d_logic, getOptions()); - ProofNodeManager* pnm = nullptr; if (d_env->getOptions().smt.produceProofs) { // ensure bound variable uses canonical bound variables getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); // make the proof manager - d_pfManager.reset(new PfManager(*d_env.get(), this)); + d_pfManager.reset(new PfManager(*d_env.get())); PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); // start the unsat core manager d_ucManager.reset(new UnsatCoreManager()); - // use this proof node manager - pnm = d_pfManager->getProofNodeManager(); - // enable proof support in the environment/rewriter - d_env->setProofNodeManager(pnm); // enable it in the assertions pipeline d_asserts->setProofGenerator(pppg); // enabled proofs in the preprocessor