From 5279adad97c7e85ca36ebc9497fa1b6c801c7ab6 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 9 Nov 2021 16:35:38 -0300 Subject: [PATCH] [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. --- src/proof/lazy_proof_chain.cpp | 77 ++++++++++++------- .../regress1/quantifiers/recfact.cvc.smt2 | 5 ++ .../strings/issue6184-unsat-core.smt2 | 6 +- 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 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 LazyCDProofChain::getProofFor(Node fact) // retrieve free assumptions and their respective proof nodes std::map>> 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) -- 2.30.2