From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Aug 2021 18:58:14 +0000 (-0500)
Subject: Add containsAssumption proof utility (#6953)
X-Git-Tag: cvc5-1.0.0~1409
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6db55eeefaf15f8aa1c08a73ad2a589da443cdc0;p=cvc5.git

Add containsAssumption proof utility (#6953)

Work towards making our policy for subproof merging safer.
---

diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp
index 82ccc034f..5f56d785e 100644
--- a/src/proof/proof_node_algorithm.cpp
+++ b/src/proof/proof_node_algorithm.cpp
@@ -136,6 +136,71 @@ void getFreeAssumptionsMap(
   } while (!visit.empty());
 }
 
+bool containsAssumption(const ProofNode* pn,
+                        std::unordered_map<const ProofNode*, bool>& caMap)
+{
+  std::unordered_map<const ProofNode*, bool> visited;
+  std::unordered_map<const ProofNode*, bool>::iterator it;
+  std::vector<const ProofNode*> visit;
+  visit.push_back(pn);
+  bool foundAssumption = false;
+  const ProofNode* cur;
+  while (!visit.empty())
+  {
+    cur = visit.back();
+    visit.pop_back();
+    // have we already computed?
+    it = caMap.find(cur);
+    if (it != caMap.end())
+    {
+      // if cached, we set found assumption to true if applicable and continue
+      if (it->second)
+      {
+        foundAssumption = true;
+      }
+      continue;
+    }
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      PfRule r = cur->getRule();
+      if (r == PfRule::ASSUME)
+      {
+        visited[cur] = true;
+        caMap[cur] = true;
+        foundAssumption = true;
+      }
+      else if (!foundAssumption)
+      {
+        // if we haven't found an assumption yet, recurse. Otherwise, we will
+        // not bother computing whether this subproof contains an assumption
+        // since we know its parent already contains one by another child.
+        visited[cur] = false;
+        visit.push_back(cur);
+        const std::vector<std::shared_ptr<ProofNode>>& children =
+            cur->getChildren();
+        for (const std::shared_ptr<ProofNode>& cp : children)
+        {
+          visit.push_back(cp.get());
+        }
+      }
+    }
+    else if (!it->second)
+    {
+      visited[cur] = true;
+      // we contain an assumption if we've found an assumption in a child
+      caMap[cur] = foundAssumption;
+    }
+  }
+  return caMap[cur];
+}
+
+bool containsAssumption(const ProofNode* pn)
+{
+  std::unordered_map<const ProofNode*, bool> caMap;
+  return containsAssumption(pn, caMap);
+}
+
 bool containsSubproof(ProofNode* pn, ProofNode* pnc)
 {
   std::unordered_set<const ProofNode*> visited;
diff --git a/src/proof/proof_node_algorithm.h b/src/proof/proof_node_algorithm.h
index 1ccefb0a2..f35a84c87 100644
--- a/src/proof/proof_node_algorithm.h
+++ b/src/proof/proof_node_algorithm.h
@@ -56,6 +56,27 @@ void getFreeAssumptionsMap(
     std::shared_ptr<ProofNode> pn,
     std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap);
 
+/**
+ * Return true if pn contains a subproof whose rule is ASSUME. Notice that we
+ * do *not* distinguish between free vs. non-free assumptions in this call.
+ * This call involves at most a single dag traversal over the proof node.
+ *
+ * This call will partially populate caMap. In particular, it will only fill
+ * caMap for the proof nodes that were traversed up to where the first
+ * assumption in pn was found.
+ *
+ * @param pn The proof node.
+ * @param caMap Cache of results, mapping proof nodes to whether they contain
+ * assumptions.
+ * @return true if pn contains assumptions
+ */
+bool containsAssumption(const ProofNode* pn,
+                        std::unordered_map<const ProofNode*, bool>& caMap);
+/**
+ * Same as above, with an empty cache as the initial value of caMap.
+ */
+bool containsAssumption(const ProofNode* pn);
+
 /**
  * @return true if pn contains pnc.
  */