(proof-new) Improve debugging infrastructure for open proofs (#4984)

This includes more versions of checking whether a proof node is closed and standardizing output.

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 7a480fa97ff41e3d9ac62e5c409a9cd2154d5f93..2d114acd6dd74af5d362ec9c46f82685967f47b7 100644 (file)
--- 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<Node> assumps;
-  pfgEnsureClosedWrt(proven, pg, assumps, c, ctx, reqGen);
-}
-
-void pfgEnsureClosedWrt(Node proven,
-                        ProofGenerator* pg,
-                        const std::vector<Node>& 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<Node>& 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<ProofNode> 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<ProofNode> 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<Node> 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<Node> assumps;
+  ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
+}
+
+void pfgEnsureClosedWrt(Node proven,
+                        ProofGenerator* pg,
+                        const std::vector<Node>& 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<Node>& 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 298f9b4c61e39ae5f24546f0e08628dd393e4125..c53b7ff2381f1b61ed8fbc193e076899f55b8db3 100644 (file)
--- 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<Node>& 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 078e918b893ee2fb1940a4f8fcf436695b2cd772..4875b7c460b2174dca11f246fc95b4cdd3ea7d75 100644 (file)
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -29,6 +29,8 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
     const std::vector<Node>& 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<ProofNode> 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;
   }