From 4e6eb0a191ec78cbebd842f9c732ef9bd76bd724 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Sep 2020 19:13:54 -0500 Subject: [PATCH] (proof-new) Improve debugging infrastructure for open proofs (#4984) This includes more versions of checking whether a proof node is closed and standardizing output. --- src/expr/proof_generator.cpp | 136 ++++++++++++++++++++++++-------- src/expr/proof_generator.h | 18 ++++- src/expr/proof_node_manager.cpp | 13 ++- 3 files changed, 130 insertions(+), 37 deletions(-) diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index 7a480fa97..2d114acd6 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -68,22 +68,17 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) return false; } -void pfgEnsureClosed(Node proven, - ProofGenerator* pg, - const char* c, - const char* ctx, - bool reqGen) -{ - std::vector assumps; - pfgEnsureClosedWrt(proven, pg, assumps, c, ctx, reqGen); -} - -void pfgEnsureClosedWrt(Node proven, - ProofGenerator* pg, - const std::vector& assumps, - const char* c, - const char* ctx, - bool reqGen) +/** + * Ensure closed with respect to assumptions, internal version, which + * generalizes the check for a proof generator or a proof node. + */ +void ensureClosedWrtInternal(Node proven, + ProofGenerator* pg, + ProofNode* pnp, + const std::vector& assumps, + const char* c, + const char* ctx, + bool reqGen) { if (!options::proofNew()) { @@ -96,38 +91,68 @@ void pfgEnsureClosedWrt(Node proven, // trace is off and proof new eager checking is off, do not do check return; } - std::stringstream ss; - ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) - << " in context " << ctx; std::stringstream sdiag; bool isTraceOn = Trace.isOn(c); if (!isTraceOn) { sdiag << ", use -t " << c << " for details"; } - Trace(c) << "=== pfgEnsureClosed: " << ss.str() << std::endl; + bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); + if (!dumpProofTraceOn) + { + sdiag << ", use -t dump-proof-error for details on proof"; + } + // get the proof node in question, which is either provided or built by the + // proof generator + std::shared_ptr pn; + std::stringstream ss; + if (pnp != nullptr) + { + Assert(pg == nullptr); + ss << "ProofNode in context " << ctx; + } + else + { + ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) + << " in context " << ctx; + if (pg == nullptr) + { + // only failure if flag is true + if (reqGen) + { + Unreachable() << "...ensureClosed: no generator in context " << ctx + << sdiag.str(); + } + } + else + { + Assert(!proven.isNull()); + pn = pg->getProofFor(proven); + pnp = pn.get(); + } + } + Trace(c) << "=== ensureClosed: " << ss.str() << std::endl; Trace(c) << "Proven: " << proven << std::endl; - if (pg == nullptr) + if (pnp == nullptr) { - // only failure if flag is true - if (reqGen) + if (pg == nullptr) { - Unreachable() << "...pfgEnsureClosed: no generator in context " << ctx - << sdiag.str(); + // did not require generator + Assert(!reqGen); + Trace(c) << "...ensureClosed: no generator in context " << ctx + << std::endl; + return; } - Trace(c) << "...pfgEnsureClosed: no generator in context " << ctx - << std::endl; - return; } - std::shared_ptr pn = pg->getProofFor(proven); - Trace(c) << " Proof: " << *pn.get() << std::endl; - if (pn == nullptr) + // if we don't have a proof node, a generator failed + if (pnp == nullptr) { - AlwaysAssert(false) << "...pfgEnsureClosed: null proof from " << ss.str() + Assert(pg != nullptr); + AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str() << sdiag.str(); } std::vector fassumps; - expr::getFreeAssumptions(pn.get(), fassumps); + expr::getFreeAssumptions(pnp, fassumps); bool isClosed = true; std::stringstream ssf; for (const Node& fa : fassumps) @@ -150,11 +175,52 @@ void pfgEnsureClosedWrt(Node proven, Trace(c) << "- " << a << std::endl; } } + if (dumpProofTraceOn) + { + Trace("dump-proof-error") << " Proof: " << *pnp << std::endl; + } } - AlwaysAssert(isClosed) << "...pfgEnsureClosed: open proof from " << ss.str() + AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str() << sdiag.str(); - Trace(c) << "...pfgEnsureClosed: success" << std::endl; + Trace(c) << "...ensureClosed: success" << std::endl; Trace(c) << "====" << std::endl; } +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen) +{ + Assert(!proven.isNull()); + // proof generator may be null + std::vector assumps; + ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); +} + +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector& assumps, + const char* c, + const char* ctx, + bool reqGen) +{ + Assert(!proven.isNull()); + // proof generator may be null + ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); +} + +void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx) +{ + ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false); +} + +void pfnEnsureClosedWrt(ProofNode* pn, + const std::vector& assumps, + const char* c, + const char* ctx) +{ + ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); +} + } // namespace CVC4 diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 298f9b4c6..c53b7ff23 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -121,7 +121,9 @@ void pfgEnsureClosed(Node proven, /** * Debug check closed with Trace c. Context ctx is string for debugging and - * assumps is the set of allowed open assertions. + * assumps is the set of allowed open assertions. This method throws an + * assertion failure if pg cannot provide a proof for fact proven whose + * free assumptions are contained in assumps. * * @param reqGen Whether we consider a null generator to be a failure. */ @@ -132,6 +134,20 @@ void pfgEnsureClosedWrt(Node proven, const char* ctx, bool reqGen = true); +/** + * Debug check closed with Trace c, proof node versions. This gives an + * assertion failure if pn is not closed. Detailed information is printed + * on trace c. Context ctx is a string used for debugging. + */ +void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx); +/** + * Same as above, but throws an assertion failure only if the free assumptions + * of pn are not contained in assumps. + */ +void pfnEnsureClosedWrt(ProofNode* pn, + const std::vector& assumps, + const char* c, + const char* ctx); } // namespace CVC4 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 078e918b8..4875b7c46 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -29,6 +29,8 @@ std::shared_ptr ProofNodeManager::mkNode( const std::vector& args, Node expected) { + Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId() + << "} " << expected << "\n"; Node res = checkInternal(id, children, args, expected); if (res.isNull()) { @@ -106,12 +108,21 @@ std::shared_ptr ProofNodeManager::mkScope( } // All free assumptions should be arguments to SCOPE. std::stringstream ss; - pf->printDebug(ss); + + bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); + if (dumpProofTraceOn) + { + ss << "The proof : " << *pf << std::endl; + } ss << std::endl << "Free assumption: " << a << std::endl; for (const Node& aprint : ac) { ss << "- assumption: " << aprint << std::endl; } + if (!dumpProofTraceOn) + { + ss << "Use -t dump-proof-error for details on proof" << std::endl; + } Unreachable() << "Generated a proof that is not closed by the scope: " << ss.str() << std::endl; } -- 2.30.2