From: Andrew Reynolds Date: Thu, 2 Sep 2021 17:02:46 +0000 (-0500) Subject: Implement lazy proof checking modes (#7106) X-Git-Tag: cvc5-1.0.0~1292 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=66b67160df9ce4974039a1c137e84c859fad5237;p=cvc5.git Implement lazy proof checking modes (#7106) This implements several variants of lazy proof checking in the core proof checker. Note this extends the ProofNode class with an additional Boolean d_provenChecked indicating whether the d_proven field was checked by the underlying proof checker. This PR updates the default proof checking mode to lazy. The previous default can now be enabled by --proof-check=eager-simple. --- diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 071f14dec..b741ec5d5 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -39,12 +39,25 @@ name = "Proof" help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof" [[option]] - name = "proofEagerChecking" + name = "proofCheck" category = "regular" - long = "proof-eager-checking" - type = "bool" - default = "false" - help = "check proofs eagerly with proof for local debugging" + long = "proof-check=MODE" + type = "ProofCheckMode" + default = "LAZY" + help = "select proof checking mode" + help_mode = "Proof checking modes." +[[option.mode.EAGER]] + name = "eager" + help = "check rule applications and proofs from generators eagerly for local debugging" +[[option.mode.EAGER_SIMPLE]] + name = "eager-simple" + help = "check rule applications during construction" +[[option.mode.LAZY]] + name = "lazy" + help = "check rule applications only during final proof construction" +[[option.mode.NONE]] + name = "none" + help = "do not check rule applications" [[option]] name = "proofGranularityMode" diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp index c835ca03d..4cb39cc40 100644 --- a/src/proof/lazy_proof_chain.cpp +++ b/src/proof/lazy_proof_chain.cpp @@ -272,8 +272,8 @@ void LazyCDProofChain::addLazyStep(Node expected, << " set to generator " << pg->identify() << "\n"; // note this will rewrite the generator for expected, if any d_gens.insert(expected, pg); - // check if chain is closed if options::proofEagerChecking() is on - if (options::proofEagerChecking()) + // check if chain is closed if eager checking is on + if (options::proofCheck() == options::ProofCheckMode::EAGER) { Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: Checking closed proof...\n"; diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 1d5aa61b4..28a09fc9c 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -85,8 +85,10 @@ ProofCheckerStatistics::ProofCheckerStatistics() { } -ProofChecker::ProofChecker(uint32_t pclevel, rewriter::RewriteDb* rdb) - : d_pclevel(pclevel), d_rdb(rdb) +ProofChecker::ProofChecker(bool eagerCheck, + uint32_t pclevel, + rewriter::RewriteDb* rdb) + : d_eagerCheck(eagerCheck), d_pclevel(pclevel), d_rdb(rdb) { } @@ -245,7 +247,7 @@ Node ProofChecker::checkInternal(PfRule id, } } // fails if pedantic level is not met - if (options::proofEagerChecking()) + if (d_eagerCheck) { std::stringstream serr; if (isPedanticFailure(id, serr, enableOutput)) diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index 6092a1932..a32f23fe4 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -105,7 +105,9 @@ class ProofCheckerStatistics class ProofChecker { public: - ProofChecker(uint32_t pclevel = 0, rewriter::RewriteDb* rdb = nullptr); + ProofChecker(bool eagerCheck, + uint32_t pclevel = 0, + rewriter::RewriteDb* rdb = nullptr); ~ProofChecker() {} /** * Return the formula that is proven by proof node pn, or null if pn is not @@ -189,6 +191,8 @@ class ProofChecker std::map d_checker; /** Maps proof trusted rules to their pedantic level */ std::map d_plevel; + /** Whether we check for pedantic failures eagerly */ + bool d_eagerCheck; /** The pedantic level of this checker */ uint32_t d_pclevel; /** Pointer to the rewrite database */ diff --git a/src/proof/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp index 774b25ef6..3e91aa799 100644 --- a/src/proof/proof_ensure_closed.cpp +++ b/src/proof/proof_ensure_closed.cpp @@ -43,7 +43,7 @@ void ensureClosedWrtInternal(Node proven, return; } bool isTraceDebug = Trace.isOn(c); - if (!options::proofEagerChecking() && !isTraceDebug) + if (options::proofCheck() != options::ProofCheckMode::EAGER && !isTraceDebug) { // trace is off and proof new eager checking is off, do not do check return; diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp index e3affb306..2a141919d 100644 --- a/src/proof/proof_node.cpp +++ b/src/proof/proof_node.cpp @@ -23,6 +23,7 @@ namespace cvc5 { ProofNode::ProofNode(PfRule id, const std::vector>& children, const std::vector& args) + : d_provenChecked(false) { setValue(id, children, args); } diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h index db82cc63d..f4552ae43 100644 --- a/src/proof/proof_node.h +++ b/src/proof/proof_node.h @@ -123,6 +123,8 @@ class ProofNode std::vector d_args; /** The cache of the fact that has been proven, modifiable by ProofChecker */ Node d_proven; + /** Was d_proven actually checked, or is it trusted? */ + bool d_provenChecked; }; inline size_t ProofNodeHashFunction::operator()( diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index 7e41a9057..a3ef944e0 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -31,6 +31,8 @@ namespace cvc5 { ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); + // we always allocate a proof checker, regardless of the proof checking mode + Assert(d_checker != nullptr); } std::shared_ptr ProofNodeManager::mkNode( @@ -41,7 +43,8 @@ std::shared_ptr ProofNodeManager::mkNode( { Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId() << "} " << expected << "\n"; - Node res = checkInternal(id, children, args, expected); + bool didCheck = false; + Node res = checkInternal(id, children, args, expected, didCheck); if (res.isNull()) { // if it was invalid, then we return the null node @@ -51,6 +54,7 @@ std::shared_ptr ProofNodeManager::mkNode( std::shared_ptr pn = std::make_shared(id, children, args); pn->d_proven = res; + pn->d_provenChecked = didCheck; return pn; } @@ -291,32 +295,49 @@ bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) { return false; } + // copy whether we did the check + pn->d_provenChecked = pnr->d_provenChecked; // can shortcut re-check of rule return updateNodeInternal( pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false); } +void ProofNodeManager::ensureChecked(ProofNode* pn) +{ + if (pn->d_provenChecked) + { + // already checked + return; + } + // directly call the proof checker + Node res = d_checker->check(pn, pn->getResult()); + pn->d_provenChecked = true; + // should have the correct result + Assert(res == pn->d_proven); +} + Node ProofNodeManager::checkInternal( PfRule id, const std::vector>& children, const std::vector& args, - Node expected) + Node expected, + bool& didCheck) { - Node res; - if (d_checker) + // if the user supplied an expected result, then we trust it if we are in + // a proof checking mode that does not eagerly check rule applications + if (!expected.isNull()) { - // check with the checker, which takes expected as argument - res = d_checker->check(id, children, args, expected); - Assert(!res.isNull()) - << "ProofNodeManager::checkInternal: failed to check proof"; - } - else - { - // otherwise we trust the expected value, if it exists - Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker " - "or expected value provided"; - res = expected; + if (options::proofCheck() == options::ProofCheckMode::LAZY + || options::proofCheck() == options::ProofCheckMode::NONE) + { + return expected; + } } + // check with the checker, which takes expected as argument + Node res = d_checker->check(id, children, args, expected); + didCheck = true; + Assert(!res.isNull()) + << "ProofNodeManager::checkInternal: failed to check proof"; return res; } @@ -371,6 +392,7 @@ std::shared_ptr ProofNodeManager::clone( visited[cur] = cloned; // we trust the above cloning does not change what is proven cloned->d_proven = cur->d_proven; + cloned->d_provenChecked = cur->d_provenChecked; } } Assert(visited.find(orig) != visited.end()); @@ -403,7 +425,7 @@ bool ProofNodeManager::updateNodeInternal( { Assert(pn != nullptr); // ---------------- check for cyclic - if (options::proofEagerChecking()) + if (options::proofCheck() == options::ProofCheckMode::EAGER) { std::unordered_set visited; for (const std::shared_ptr& cpc : children) @@ -436,7 +458,8 @@ bool ProofNodeManager::updateNodeInternal( if (needsCheck) { // We expect to prove the same thing as before - Node res = checkInternal(id, children, args, pn->d_proven); + bool didCheck = false; + Node res = checkInternal(id, children, args, pn->d_proven, didCheck); if (res.isNull()) { // if it was invalid, then we do not update @@ -444,6 +467,7 @@ bool ProofNodeManager::updateNodeInternal( } // proven field should already be the same as the result Assert(res == pn->d_proven); + pn->d_provenChecked = didCheck; } // we update its value diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 541686a30..928aabb76 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -163,6 +163,10 @@ class ProofNodeManager * unchanged. */ bool updateNode(ProofNode* pn, ProofNode* pnr); + /** + * Ensure that pn is checked, regardless of the proof check format. + */ + void ensureChecked(ProofNode* pn); /** Get the underlying proof checker */ ProofChecker* getChecker() const; /** @@ -193,11 +197,15 @@ class ProofNodeManager * This throws an assertion error if we fail to check such a proof node, or * if expected is provided (non-null) and is different what is proven by the * other arguments. + * + * The flag didCheck is set to true if the underlying proof checker was + * invoked. This may be false if e.g. the proof checking mode is lazy. */ Node checkInternal(PfRule id, const std::vector>& children, const std::vector& args, - Node expected); + Node expected, + bool& didCheck); /** * Update node internal, return true if successful. This is called by * the update node methods above. The argument needsCheck is whether we diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index dd22416db..9060c318c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -220,7 +220,8 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) Assert(ppSkolems.size() == ppLemmas.size()); // do final checks on the lemmas we are about to send - if (isProofEnabled() && options::proofEagerChecking()) + if (isProofEnabled() + && options::proofCheck() == options::ProofCheckMode::EAGER) { Assert(tplemma.getGenerator() != nullptr); // ensure closed, make the proof node eagerly here to debug diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 8891016a4..da49a5990 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -685,7 +685,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, } } while (expanded); // now we should be able to close it - if (options::proofEagerChecking()) + if (options::proofCheck() == options::ProofCheckMode::EAGER) { std::vector assumptionsVec; for (const Node& a : d_assumptions) diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 1eea6286b..1e322ccd3 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -256,7 +256,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; } void PreprocessProofGenerator::checkEagerPedantic(PfRule r) { - if (options::proofEagerChecking()) + if (options::proofCheck() == options::ProofCheckMode::EAGER) { // catch a pedantic failure now, which otherwise would not be // triggered since we are doing lazy proof generation diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index ae35b346c..93b4cae19 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -59,7 +59,7 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr pn, { PfRule r = pn->getRule(); // if not doing eager pedantic checking, fail if below threshold - if (!options::proofEagerChecking()) + if (options::proofCheck() != options::ProofCheckMode::EAGER) { if (!d_pedanticFailure) { @@ -70,6 +70,10 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr pn, } } } + if (options::proofCheck() != options::ProofCheckMode::NONE) + { + d_pnm->ensureChecked(pn.get()); + } uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r); if (plevel != 0) { diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 49f67e94c..ae5de49e9 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -33,7 +33,9 @@ namespace smt { PfManager::PfManager(Env& env, SmtEngine* smte) : d_env(env), - d_pchecker(new ProofChecker(options::proofPedantic())), + d_pchecker(new ProofChecker( + d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER, + d_env.getOptions().proof.proofPedantic)), d_pnm(new ProofNodeManager(d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 3c9a82a61..65762a50b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -369,7 +369,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const << reasonNoProofs.str() << "." << std::endl; opts.smt.produceProofs = false; opts.smt.checkProofs = false; - opts.proof.proofEagerChecking = false; } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 27e7b8530..5403928ec 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -876,12 +876,14 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, } // Check that UNSAT results generate a proof correctly. if (d_env->getOptions().smt.checkProofs - || d_env->getOptions().proof.proofEagerChecking) + || d_env->getOptions().proof.proofCheck + == options::ProofCheckMode::EAGER) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { if ((d_env->getOptions().smt.checkProofs - || d_env->getOptions().proof.proofEagerChecking) + || d_env->getOptions().proof.proofCheck + == options::ProofCheckMode::EAGER) && !d_env->getOptions().smt.produceProofs) { throw ModalException( @@ -1368,7 +1370,7 @@ void SmtEngine::checkProof() // internal check the proof PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - if (d_env->getOptions().proof.proofEagerChecking) + if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER) { pe->checkProof(d_asserts->getAssertionList()); } @@ -1439,7 +1441,6 @@ std::vector SmtEngine::reduceUnsatCore(const std::vector& core) // disable all proof options coreChecker->getOptions().smt.produceProofs = false; coreChecker->getOptions().smt.checkProofs = false; - coreChecker->getOptions().proof.proofEagerChecking = false; for (const Node& ucAssertion : core) { @@ -1504,7 +1505,6 @@ void SmtEngine::checkUnsatCore() { // disable all proof options coreChecker->getOptions().smt.produceProofs = false; coreChecker->getOptions().smt.checkProofs = false; - coreChecker->getOptions().proof.proofEagerChecking = false; // set up separation logic heap if necessary TypeNode sepLocType, sepDataType; diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2 index ccd0b7634..6744e3a0e 100644 --- a/test/regress/regress0/arith/non-normal.smt2 +++ b/test/regress/regress0/arith/non-normal.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --proof-eager-checking +; COMMAND-LINE: --proof-check=eager ; EXPECT: sat (set-logic QF_UFLRA) (declare-fun v1 () Real)