[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)

Previously the trivial cycle check only covered the case in which the currently-being-expanded assumption `A` had as its stored proof node `pf` an assumption proof justifying itself. However, it can be the case that `pf` is not an assumption proof, but a proof that nevertheless has `A` as one of its free assumptions. This commit generalizes the trivial cycle check to account for this.

3 files changed, 58 insertions, 30 deletions

diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp
index b6f3b527f..0de5673ab 100644
--- a/src/proof/lazy_proof_chain.cpp
+++ b/src/proof/lazy_proof_chain.cpp
@@ -109,13 +109,8 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
       }
       // map node whose proof node must be expanded to the respective poof node
       toConnect[cur] = curPfn;
-      // We may not want to recursively connect this proof or, if it's
-      // assumption, there is nothing to connect, so we skip. Note that in the
-      // special case in which curPfn is an assumption and cur is actually the
-      // initial fact that getProofFor is called on, the cycle detection below
-      // would prevent this method from generating the assumption proof for it,
-      // which would be wrong.
-      if (!rec || curPfn->getRule() == PfRule::ASSUME)
+      // We may not want to recursively connect this proof so we skip.
+      if (!rec)
       {
         visited[cur] = true;
         continue;
@@ -126,34 +121,58 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
       // retrieve free assumptions and their respective proof nodes
       std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
       expr::getFreeAssumptionsMap(curPfn, famap);
-      if (Trace.isOn("lazy-cdproofchain"))
+      if (d_cyclic)
       {
-        unsigned alreadyToVisit = 0;
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: " << famap.size()
-            << " free assumptions:\n";
-        for (auto fap : famap)
+        // First check for a trivial cycle, which is when cur is a free
+        // assumption of curPfn. Note that in the special case in the special
+        // case in which curPfn has cur as an assumption and cur is actually the
+        // initial fact that getProofFor is called on, the general cycle
+        // detection below would prevent this method from generating a proof for
+        // cur, which would be wrong since there is a justification for it in
+        // curPfn.
+        bool isCyclic = false;
+        for (const auto& fap : famap)
+        {
+          if (cur == fap.first)
+          {
+            // connect it to one of the assumption proof nodes
+            toConnect[cur] = fap.second[0];
+            isCyclic = true;
+            break;
+          }
+        }
+        if (isCyclic)
         {
           Trace("lazy-cdproofchain")
-              << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
-          alreadyToVisit +=
-              std::find(visit.begin(), visit.end(), fap.first) != visit.end()
-                  ? 1
-                  : 0;
+              << "LazyCDProofChain::getProofFor: trivial cycle detected for "
+              << cur << ", abort\n";
+          visited[cur] = true;
+          continue;
         }
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: " << alreadyToVisit
-            << " already to visit\n";
-      }
-      // If we are controlling cycle, check whether any of the assumptions of
-      // cur would provoke a cycle. In such a case we treat cur as an
-      // assumption, removing it from toConnect, and do not proceed to expand
-      // any of its assumptions.
-      if (d_cyclic)
-      {
+        if (Trace.isOn("lazy-cdproofchain"))
+        {
+          unsigned alreadyToVisit = 0;
+          Trace("lazy-cdproofchain")
+              << "LazyCDProofChain::getProofFor: " << famap.size()
+              << " free assumptions:\n";
+          for (auto fap : famap)
+          {
+            Trace("lazy-cdproofchain")
+                << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
+            alreadyToVisit +=
+                std::find(visit.begin(), visit.end(), fap.first) != visit.end()
+                    ? 1
+                    : 0;
+          }
+          Trace("lazy-cdproofchain")
+              << "LazyCDProofChain::getProofFor: " << alreadyToVisit
+              << " already to visit\n";
+        }
+        // If we are controlling cycle, check whether any of the assumptions of
+        // cur would provoke a cycle. In such we remove cur from toConnect and
+        // do not proceed to expand any of its assumptions.
         Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking "
                                    << cur << " for cycle check\n";
-        bool isCyclic = false;
         // enqueue free assumptions to process
         for (const auto& fap : famap)
         {
diff --git a/test/regress/regress1/quantifiers/recfact.cvc.smt2 b/test/regress/regress1/quantifiers/recfact.cvc.smt2
index 02676b625..e36707360 100644
--- a/test/regress/regress1/quantifiers/recfact.cvc.smt2
+++ b/test/regress/regress1/quantifiers/recfact.cvc.smt2
@@ -1,4 +1,9 @@
 ; EXPECT: unsat
+; COMMAND-LINE:
+; COMMAND-LINE: --produce-proofs
+;; The second command line option, other than the default, is to test
+;; unsat core checking with proofs, which at one point had issues for
+;; this benchmark due to cycle detection in LazyCDProofChain
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :fmf-fun true)
diff --git a/test/regress/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/regress1/strings/issue6184-unsat-core.smt2
index 5e257da00..8dcfe81f8 100644
--- a/test/regress/regress1/strings/issue6184-unsat-core.smt2
+++ b/test/regress/regress1/strings/issue6184-unsat-core.smt2
@@ -1,5 +1,9 @@
-; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
+; COMMAND-LINE: --strings-exp
+; COMMAND-LINE: --strings-exp --produce-proofs
+;; The second command line option is to test unsat core checking with
+;; proofs, which at one point had issues for this benchmark due to
+;; cycle detection in LazyCDProofChain
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :check-unsat-cores true)