Add proof letify utility (#6881)

Towards support for external proof conversions.

3 files changed, 224 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 445d38896..9f208ac46 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -169,6 +169,8 @@ libcvc5_add_sources(
   proof/proof_ensure_closed.h
   proof/proof_generator.cpp
   proof/proof_generator.h
+  proof/proof_letify.cpp
+  proof/proof_letify.h
   proof/proof_node.cpp
   proof/proof_node.h
   proof/proof_node_algorithm.cpp
diff --git a/src/proof/proof_letify.cpp b/src/proof/proof_letify.cpp
new file mode 100644
index 000000000..c6269631c
--- /dev/null
+++ b/src/proof/proof_letify.cpp
@@ -0,0 +1,124 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Utilities for computing letification of proofs.
+ */
+
+#include "proof/proof_letify.h"
+
+namespace cvc5 {
+namespace proof {
+
+bool ProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn)
+{
+  return pn->getRule() != PfRule::SCOPE;
+}
+
+void ProofLetify::computeProofLet(const ProofNode* pn,
+                                  std::vector<const ProofNode*>& pletList,
+                                  std::map<const ProofNode*, size_t>& pletMap,
+                                  size_t thresh,
+                                  ProofLetifyTraverseCallback* pltc)
+{
+  Assert(pletList.empty() && pletMap.empty());
+  if (thresh == 0)
+  {
+    // value of 0 means do not introduce let
+    return;
+  }
+  std::vector<const ProofNode*> visitList;
+  std::map<const ProofNode*, size_t> pcount;
+  if (pltc == nullptr)
+  {
+    // use default callback
+    ProofLetifyTraverseCallback defaultPltc;
+    computeProofCounts(pn, visitList, pcount, &defaultPltc);
+  }
+  else
+  {
+    computeProofCounts(pn, visitList, pcount, pltc);
+  }
+  // Now populate the pletList and pletMap
+  convertProofCountToLet(visitList, pcount, pletList, pletMap, thresh);
+}
+
+void ProofLetify::computeProofCounts(const ProofNode* pn,
+                                     std::vector<const ProofNode*>& visitList,
+                                     std::map<const ProofNode*, size_t>& pcount,
+                                     ProofLetifyTraverseCallback* pltc)
+{
+  std::map<const ProofNode*, size_t>::iterator it;
+  std::vector<const ProofNode*> visit;
+  const ProofNode* cur;
+  visit.push_back(pn);
+  do
+  {
+    cur = visit.back();
+    it = pcount.find(cur);
+    if (it == pcount.end())
+    {
+      pcount[cur] = 0;
+      if (!pltc->shouldTraverse(cur))
+      {
+        // callback indicated we should not traverse
+        continue;
+      }
+      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
+      for (const std::shared_ptr<ProofNode>& cp : pc)
+      {
+        visit.push_back(cp.get());
+      }
+    }
+    else
+    {
+      if (it->second == 0)
+      {
+        visitList.push_back(cur);
+      }
+      pcount[cur]++;
+      visit.pop_back();
+    }
+  } while (!visit.empty());
+}
+
+void ProofLetify::convertProofCountToLet(
+    const std::vector<const ProofNode*>& visitList,
+    const std::map<const ProofNode*, size_t>& pcount,
+    std::vector<const ProofNode*>& pletList,
+    std::map<const ProofNode*, size_t>& pletMap,
+    size_t thresh)
+{
+  Assert(pletList.empty() && pletMap.empty());
+  if (thresh == 0)
+  {
+    // value of 0 means do not introduce let
+    return;
+  }
+  // Assign ids for those whose count is > 1, traverse in reverse order
+  // so that deeper proofs are assigned lower identifiers
+  std::map<const ProofNode*, size_t>::const_iterator itc;
+  for (const ProofNode* pn : visitList)
+  {
+    itc = pcount.find(pn);
+    Assert(itc != pcount.end());
+    if (itc->second >= thresh && pn->getRule() != PfRule::ASSUME)
+    {
+      pletList.push_back(pn);
+      // start with id 1
+      size_t id = pletMap.size() + 1;
+      pletMap[pn] = id;
+    }
+  }
+}
+
+}  // namespace proof
+}  // namespace cvc5
diff --git a/src/proof/proof_letify.h b/src/proof/proof_letify.h
new file mode 100644
index 000000000..cfe1259e5
--- /dev/null
+++ b/src/proof/proof_letify.h
@@ -0,0 +1,98 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Utilities for computing letification of proofs.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__PROOF_LETIFY_H
+#define CVC5__PROOF__PROOF_LETIFY_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "proof/proof_node.h"
+
+namespace cvc5 {
+namespace proof {
+
+/**
+ * A callback which asks whether a proof node should be traversed for
+ * proof letification. For example, this may make it so that SCOPE is not
+ * traversed.
+ */
+class ProofLetifyTraverseCallback
+{
+ public:
+  virtual ~ProofLetifyTraverseCallback() {}
+  /**
+   * Should we traverse proof node pn for letification? If this returns false,
+   * then pn is being treated as a black box for letification.
+   */
+  virtual bool shouldTraverse(const ProofNode* pn);
+};
+
+/**
+ * Utilities for letification.
+ */
+class ProofLetify
+{
+ public:
+  /**
+   * Stores proofs in map that require letification, mapping them to a unique
+   * identifier. For each proof node in the domain of pletMap in the list
+   * pletList such that pletList[i] does not contain subproof pletList[j] for
+   * j>i.
+   *
+   * @param pn The proof node to letify
+   * @param pletList The list of proofs occurring in pn that should be letified
+   * @param pletMap Mapping from proofs in pletList to an identifier
+   * @param thresh The number of times a proof node has to occur to be added
+   * to pletList
+   * @param pltc A callback indicating whether to traverse a proof node during
+   * this call.
+   */
+  static void computeProofLet(const ProofNode* pn,
+                              std::vector<const ProofNode*>& pletList,
+                              std::map<const ProofNode*, size_t>& pletMap,
+                              size_t thresh = 2,
+                              ProofLetifyTraverseCallback* pltc = nullptr);
+
+ private:
+  /**
+   * Convert a map from proof nodes to # occurrences (pcount) to a list
+   * pletList / pletMap as described in the method above, where thresh
+   * is the minimum number of occurrences to be added to the list.
+   */
+  static void convertProofCountToLet(
+      const std::vector<const ProofNode*>& visitList,
+      const std::map<const ProofNode*, size_t>& pcount,
+      std::vector<const ProofNode*>& pletList,
+      std::map<const ProofNode*, size_t>& pletMap,
+      size_t thresh = 2);
+  /**
+   * Compute the count of sub proof nodes in pn, store in pcount. Additionally,
+   * store each proof node in the domain of pcount in an order in visitList
+   * such that visitList[i] does not contain sub proof visitList[j] for j>i.
+   */
+  static void computeProofCounts(const ProofNode* pn,
+                                 std::vector<const ProofNode*>& visitList,
+                                 std::map<const ProofNode*, size_t>& pcount,
+                                 ProofLetifyTraverseCallback* pltc);
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif