From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Dec 2020 13:55:30 +0000 (-0600)
Subject:  (proof-new) Split proof ensure closed checks to own file (#5522)
X-Git-Tag: cvc5-1.0.0~2493
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=85f14a1ba37949afbd33f38c8565dc5d45a300fe;p=cvc5.git

 (proof-new) Split proof ensure closed checks to own file (#5522)

Split proof ensure closed checks to own file
---

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index f0825f180..ea35284fb 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -55,6 +55,8 @@ libcvc4_add_sources(
   proof.h
   proof_checker.cpp
   proof_checker.h
+  proof_ensure_closed.cpp
+  proof_ensure_closed.h
   proof_generator.cpp
   proof_generator.h
   proof_node.cpp
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 267da2607..0c209f393 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/lazy_proof.h"
 
+#include "expr/proof_ensure_closed.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index a98ba7453..c58bb78e4 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -15,6 +15,7 @@
 #include "expr/lazy_proof_chain.h"
 
 #include "expr/proof.h"
+#include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/smt_options.h"
 
diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
new file mode 100644
index 000000000..14b7f06f1
--- /dev/null
+++ b/src/expr/proof_ensure_closed.cpp
@@ -0,0 +1,177 @@
+/*********************                                                        */
+/*! \file proof_ensure_closed.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of debug checks for ensuring proofs are closed
+ **/
+
+#include "expr/proof_ensure_closed.h"
+
+#include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
+
+namespace CVC4 {
+
+/**
+ * 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())
+  {
+    // proofs not enabled, do not do check
+    return;
+  }
+  bool isTraceDebug = Trace.isOn(c);
+  if (!options::proofNewEagerChecking() && !isTraceDebug)
+  {
+    // trace is off and proof new eager checking is off, do not do check
+    return;
+  }
+  std::stringstream sdiag;
+  bool isTraceOn = Trace.isOn(c);
+  if (!isTraceOn)
+  {
+    sdiag << ", use -t " << c << " for details";
+  }
+  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 (pnp == nullptr)
+  {
+    if (pg == nullptr)
+    {
+      // did not require generator
+      Assert(!reqGen);
+      Trace(c) << "...ensureClosed: no generator in context " << ctx
+               << std::endl;
+      return;
+    }
+  }
+  // if we don't have a proof node, a generator failed
+  if (pnp == nullptr)
+  {
+    Assert(pg != nullptr);
+    AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str()
+                        << sdiag.str();
+  }
+  std::vector<Node> fassumps;
+  expr::getFreeAssumptions(pnp, fassumps);
+  bool isClosed = true;
+  std::stringstream ssf;
+  for (const Node& fa : fassumps)
+  {
+    if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end())
+    {
+      isClosed = false;
+      ssf << "- " << fa << std::endl;
+    }
+  }
+  if (!isClosed)
+  {
+    Trace(c) << "Free assumptions:" << std::endl;
+    Trace(c) << ssf.str();
+    if (!assumps.empty())
+    {
+      Trace(c) << "Expected assumptions:" << std::endl;
+      for (const Node& a : assumps)
+      {
+        Trace(c) << "- " << a << std::endl;
+      }
+    }
+    if (dumpProofTraceOn)
+    {
+      Trace("dump-proof-error") << " Proof: " << *pnp << std::endl;
+    }
+  }
+  AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str()
+                         << sdiag.str();
+  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_ensure_closed.h b/src/expr/proof_ensure_closed.h
new file mode 100644
index 000000000..03ee1e717
--- /dev/null
+++ b/src/expr/proof_ensure_closed.h
@@ -0,0 +1,71 @@
+/*********************                                                        */
+/*! \file proof_ensure_closed.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Debug checks for ensuring proofs are closed
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_ENSURE_CLOSED_H
+#define CVC4__EXPR__PROOF_ENSURE_CLOSED_H
+
+#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+/**
+ * Debug check closed on Trace c. Context ctx is string for debugging.
+ * This method throws an assertion failure if pg cannot provide a closed
+ * proof for fact proven. This is checked only if --proof-new-eager-checking
+ * is enabled or the Trace c is enabled.
+ *
+ * @param reqGen Whether we consider a null generator to be a failure.
+ */
+void pfgEnsureClosed(Node proven,
+                     ProofGenerator* pg,
+                     const char* c,
+                     const char* ctx,
+                     bool reqGen = true);
+
+/**
+ * Debug check closed with Trace c. Context ctx is string for debugging and
+ * 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.
+ */
+void pfgEnsureClosedWrt(Node proven,
+                        ProofGenerator* pg,
+                        const std::vector<Node>& assumps,
+                        const char* c,
+                        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_ENSURE_CLOSED_H */
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 68a819122..d2206a570 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -70,159 +70,4 @@ bool ProofGenerator::addProofTo(Node f,
   return false;
 }
 
-/**
- * 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())
-  {
-    // proofs not enabled, do not do check
-    return;
-  }
-  bool isTraceDebug = Trace.isOn(c);
-  if (!options::proofNewEagerChecking() && !isTraceDebug)
-  {
-    // trace is off and proof new eager checking is off, do not do check
-    return;
-  }
-  std::stringstream sdiag;
-  bool isTraceOn = Trace.isOn(c);
-  if (!isTraceOn)
-  {
-    sdiag << ", use -t " << c << " for details";
-  }
-  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 (pnp == nullptr)
-  {
-    if (pg == nullptr)
-    {
-      // did not require generator
-      Assert(!reqGen);
-      Trace(c) << "...ensureClosed: no generator in context " << ctx
-               << std::endl;
-      return;
-    }
-  }
-  // if we don't have a proof node, a generator failed
-  if (pnp == nullptr)
-  {
-    Assert(pg != nullptr);
-    AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str()
-                        << sdiag.str();
-  }
-  std::vector<Node> fassumps;
-  expr::getFreeAssumptions(pnp, fassumps);
-  bool isClosed = true;
-  std::stringstream ssf;
-  for (const Node& fa : fassumps)
-  {
-    if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end())
-    {
-      isClosed = false;
-      ssf << "- " << fa << std::endl;
-    }
-  }
-  if (!isClosed)
-  {
-    Trace(c) << "Free assumptions:" << std::endl;
-    Trace(c) << ssf.str();
-    if (!assumps.empty())
-    {
-      Trace(c) << "Expected assumptions:" << std::endl;
-      for (const Node& a : assumps)
-      {
-        Trace(c) << "- " << a << std::endl;
-      }
-    }
-    if (dumpProofTraceOn)
-    {
-      Trace("dump-proof-error") << " Proof: " << *pnp << std::endl;
-    }
-  }
-  AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str()
-                         << sdiag.str();
-  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 6e6316356..869f226b8 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -107,49 +107,6 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
-/**
- * Debug check closed on Trace c. Context ctx is string for debugging.
- * This method throws an assertion failure if pg cannot provide a closed
- * proof for fact proven. This is checked only if --proof-new-eager-checking
- * is enabled or the Trace c is enabled.
- *
- * @param reqGen Whether we consider a null generator to be a failure.
- */
-void pfgEnsureClosed(Node proven,
-                     ProofGenerator* pg,
-                     const char* c,
-                     const char* ctx,
-                     bool reqGen = true);
-
-/**
- * Debug check closed with Trace c. Context ctx is string for debugging and
- * 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.
- */
-void pfgEnsureClosedWrt(Node proven,
-                        ProofGenerator* pg,
-                        const std::vector<Node>& assumps,
-                        const char* c,
-                        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_updater.cpp b/src/expr/proof_node_updater.cpp
index 834f4381f..af32c223d 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -15,6 +15,7 @@
 #include "expr/proof_node_updater.h"
 
 #include "expr/lazy_proof.h"
+#include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
 
 namespace CVC4 {
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index fc5f92434..3b1df8a00 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -14,6 +14,7 @@
 
 #include "prop/prop_proof_manager.h"
 
+#include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
 
 namespace CVC4 {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e771f8bb8..da0fc8de4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,6 +26,7 @@
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_visitor.h"
+#include "expr/proof_ensure_closed.h"
 #include "options/bv_options.h"
 #include "options/options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index 6c792e355..905004cb8 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/trust_node.h"
 
+#include "expr/proof_ensure_closed.h"
 #include "expr/proof_generator.h"
 
 namespace CVC4 {