(proof-new) Refactoring cyclic checks (#5291)

This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true.

It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.

4 files changed, 88 insertions, 38 deletions

diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 8f8813f41..b21bdec23 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -39,6 +39,7 @@ void getFreeAssumptionsMap(
   std::unordered_map<ProofNode*, bool> visited;
   std::unordered_map<ProofNode*, bool>::iterator it;
   std::vector<std::shared_ptr<ProofNode>> visit;
+  std::vector<std::shared_ptr<ProofNode>> traversing;
   // Maps a bound assumption to the number of bindings it is under
   // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
   // (ASSUME x), and x would be mapped to 1.
@@ -68,10 +69,10 @@ void getFreeAssumptionsMap(
     const std::vector<Node>& cargs = cur->getArguments();
     if (it == visited.end())
     {
-      visited[cur.get()] = true;
       PfRule id = cur->getRule();
       if (id == PfRule::ASSUME)
       {
+        visited[cur.get()] = true;
         Assert(cargs.size() == 1);
         Node f = cargs[0];
         if (!scopeDepth.count(f))
@@ -89,36 +90,84 @@ void getFreeAssumptionsMap(
             scopeDepth[a] += 1;
           }
           // will need to unbind the variables below
-          visited[cur.get()] = false;
-          visit.push_back(cur);
         }
         // The following loop cannot be merged with the loop above because the
         // same subproof
+        visited[cur.get()] = false;
+        visit.push_back(cur);
+        traversing.push_back(cur);
         const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
         for (const std::shared_ptr<ProofNode>& cp : cs)
         {
+          if (std::find(traversing.begin(), traversing.end(), cp)
+              != traversing.end())
+          {
+            Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
+                           "--proof-new-eager-checking)"
+                        << std::endl;
+          }
           visit.push_back(cp);
         }
       }
     }
     else if (!it->second)
     {
+      Assert(!traversing.empty());
+      traversing.pop_back();
       visited[cur.get()] = true;
-      Assert(cur->getRule() == PfRule::SCOPE);
-      // unbind its assumptions
-      for (const Node& a : cargs)
+      if (cur->getRule() == PfRule::SCOPE)
       {
-        auto scopeCt = scopeDepth.find(a);
-        Assert(scopeCt != scopeDepth.end());
-        scopeCt->second -= 1;
-        if (scopeCt->second == 0)
+        // unbind its assumptions
+        for (const Node& a : cargs)
         {
-          scopeDepth.erase(scopeCt);
+          auto scopeCt = scopeDepth.find(a);
+          Assert(scopeCt != scopeDepth.end());
+          scopeCt->second -= 1;
+          if (scopeCt->second == 0)
+          {
+            scopeDepth.erase(scopeCt);
+          }
         }
       }
     }
   } while (!visit.empty());
 }
 
+bool containsSubproof(ProofNode* pn, ProofNode* pnc)
+{
+  std::unordered_set<const ProofNode*> visited;
+  return containsSubproof(pn, pnc, visited);
+}
+
+bool containsSubproof(ProofNode* pn,
+                      ProofNode* pnc,
+                      std::unordered_set<const ProofNode*>& visited)
+{
+  std::unordered_map<const ProofNode*, bool>::iterator it;
+  std::vector<const ProofNode*> visit;
+  visit.push_back(pn);
+  const ProofNode* cur;
+  while (!visit.empty())
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur == pnc)
+      {
+        return true;
+      }
+      const std::vector<std::shared_ptr<ProofNode>>& children =
+          cur->getChildren();
+      for (const std::shared_ptr<ProofNode>& cp : children)
+      {
+        visit.push_back(cp.get());
+      }
+    }
+  }
+  return false;
+}
+
 }  // namespace expr
 }  // namespace CVC4
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index 71d29532f..d6bd1963c 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -53,6 +53,20 @@ void getFreeAssumptionsMap(
     std::shared_ptr<ProofNode> pn,
     std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap);
 
+/**
+ * @return true if pn contains pnc.
+ */
+bool containsSubproof(ProofNode* pn, ProofNode* pnc);
+
+/**
+ * Same as above, with a visited cache.
+ *
+ * @return true if pn contains pnc.
+ */
+bool containsSubproof(ProofNode* pn,
+                      ProofNode* pnc,
+                      std::unordered_set<const ProofNode*>& visited);
+
 }  // namespace expr
 }  // namespace CVC4
 
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 8ed9779d3..c238f9e35 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/proof.h"
 #include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
@@ -300,23 +301,12 @@ bool ProofNodeManager::updateNodeInternal(
 {
   Assert(pn != nullptr);
   // ---------------- check for cyclic
-  std::unordered_map<const ProofNode*, bool> visited;
-  std::unordered_map<const ProofNode*, bool>::iterator it;
-  std::vector<const ProofNode*> visit;
-  for (const std::shared_ptr<ProofNode>& cp : children)
+  if (options::proofNewEagerChecking())
   {
-    visit.push_back(cp.get());
-  }
-  const ProofNode* cur;
-  while (!visit.empty())
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-    if (it == visited.end())
+    std::unordered_set<const ProofNode*> visited;
+    for (const std::shared_ptr<ProofNode>& cpc : children)
     {
-      visited[cur] = true;
-      if (cur == pn)
+      if (expr::containsSubproof(cpc.get(), pn, visited))
       {
         std::stringstream ss;
         ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
@@ -334,10 +324,6 @@ bool ProofNodeManager::updateNodeInternal(
         }
         Unreachable() << ss.str();
       }
-      for (const std::shared_ptr<ProofNode>& cp : cur->d_children)
-      {
-        visit.push_back(cp.get());
-      }
     }
   }
   // ---------------- end check for cyclic
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index db7fb1a6f..2dbb2a873 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -32,7 +32,7 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
   NodeManager* nm = NodeManager::currentNM();
   std::map<const ProofNode*, Node>::iterator it;
   std::vector<const ProofNode*> visit;
-  std::vector<const ProofNode*> constructing;
+  std::vector<const ProofNode*> traversing;
   const ProofNode* cur;
   visit.push_back(pn);
   do
@@ -44,16 +44,17 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
     if (it == d_pnMap.end())
     {
       d_pnMap[cur] = Node::null();
-      constructing.push_back(cur);
+      traversing.push_back(cur);
       visit.push_back(cur);
       const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
       for (const std::shared_ptr<ProofNode>& cp : pc)
       {
-        if (std::find(constructing.begin(), constructing.end(), cp.get())
-            != constructing.end())
+        if (std::find(traversing.begin(), traversing.end(), cp.get())
+            != traversing.end())
         {
-          AlwaysAssert(false)
-              << "ProofNodeToSExpr::convertToSExpr: cyclic proof!" << std::endl;
+          Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
+                         "--proof-new-eager-checking)"
+                      << std::endl;
           return Node::null();
         }
         visit.push_back(cp.get());
@@ -61,8 +62,8 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
     }
     else if (it->second.isNull())
     {
-      Assert(!constructing.empty());
-      constructing.pop_back();
+      Assert(!traversing.empty());
+      traversing.pop_back();
       std::vector<Node> children;
       // add proof rule
       children.push_back(getOrMkPfRuleVariable(cur->getRule()));