Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

1 files changed, 0 insertions, 183 deletions

diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
deleted file mode 100644
index e89bd6692..000000000
--- a/src/expr/proof_ensure_closed.cpp
+++ /dev/null
@@ -1,183 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Implementation of debug checks for ensuring proofs are closed.
- */
-
-#include "expr/proof_ensure_closed.h"
-
-#include <sstream>
-
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "options/proof_options.h"
-#include "options/smt_options.h"
-
-namespace cvc5 {
-
-/**
- * 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::produceProofs())
-  {
-    // proofs not enabled, do not do check
-    return;
-  }
-  bool isTraceDebug = Trace.isOn(c);
-  if (!options::proofEagerChecking() && !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 cvc5