[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during double SYMM elimination (#7630)

This fixes the potential for cyclic proofs in CDProof when P and (SYMM P) are added as proofs to a CDProof with automatic managing of symmetry.

This manifested as non-termination on the seqArray branch with proofs enabled, instead, if this were to occur, we should throw an error, which is easy to catch.

2 files changed, 26 insertions, 0 deletions

diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
index dc370a04d..ffccd42ba 100644
--- a/src/proof/proof.cpp
+++ b/src/proof/proof.cpp
@@ -287,6 +287,24 @@ bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
 {
   if (!doCopy)
   {
+    // If we are automatically managing symmetry, we strip off SYMM steps.
+    // This avoids cyclic proofs in cases where P and (SYMM P) are added as
+    // proofs to the same CDProof.
+    if (d_autoSymm)
+    {
+      std::vector<std::shared_ptr<ProofNode>> processed;
+      while (pn->getRule() == PfRule::SYMM)
+      {
+        pn = pn->getChildren()[0];
+        if (std::find(processed.begin(), processed.end(), pn)
+            != processed.end())
+        {
+          Unreachable() << "Cyclic proof encountered when cancelling symmetry "
+                           "steps during addProof";
+        }
+        processed.push_back(pn);
+      }
+    }
     // If we aren't doing a deep copy, we either store pn or link its top
     // node into the existing pointer
     Node curFact = pn->getResult();
diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 72c39c59f..e0a7f81c0 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -403,12 +403,20 @@ std::shared_ptr<ProofNode> ProofNodeManager::clone(
 
 ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn)
 {
+  // processed is almost always size <= 1
+  std::vector<ProofNode*> processed;
   while (pn->getRule() == PfRule::SYMM)
   {
     std::shared_ptr<ProofNode> pnc = pn->getChildren()[0];
     if (pnc->getRule() == PfRule::SYMM)
     {
       pn = pnc->getChildren()[0].get();
+      if (std::find(processed.begin(), processed.end(), pn) != processed.end())
+      {
+        Unreachable()
+            << "Cyclic proof encountered when cancelling double symmetry";
+      }
+      processed.push_back(pn);
     }
     else
     {