From: Haniel Barbosa Date: Fri, 5 Nov 2021 22:48:22 +0000 (-0300) Subject: [proofs] Fix open sat proof (#7509) X-Git-Tag: cvc5-1.0.0~875 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0181355bdf6b76fc550a2dca16fc0ac5e48c25ca;p=cvc5.git [proofs] Fix open sat proof (#7509) Improves how LazyCDProofChain handles cycles, which fixes a particular case triggered by the added regression. Also makes LazyCDProofChain::getProofFor more robust in that when it can't connect the requested fact it yields an assumption proof node. Fixes cvc5/cvc5-projects#324 --- diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp index 4cb39cc40..b6f3b527f 100644 --- a/src/proof/lazy_proof_chain.cpp +++ b/src/proof/lazy_proof_chain.cpp @@ -59,7 +59,9 @@ const std::map> LazyCDProofChain::getLinks() std::shared_ptr LazyCDProofChain::getProofFor(Node fact) { Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor " << fact << "\n"; + << "LazyCDProofChain::getProofFor of gen " << d_name << "\n"; + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: " << fact << "\n"; // which facts have had proofs retrieved for. This is maintained to avoid // cycles. It also saves the proof node of the fact std::unordered_map> toConnect; @@ -107,9 +109,14 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) } // map node whose proof node must be expanded to the respective poof node toConnect[cur] = curPfn; - if (!rec) + // 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 don't want to recursively connect this proof visited[cur] = true; continue; } @@ -138,11 +145,44 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) << "LazyCDProofChain::getProofFor: " << alreadyToVisit << " already to visit\n"; } - // mark for post-traversal if we are controlling cycles + // 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) { Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking " << cur << " for cycle check\n"; + bool isCyclic = false; + // enqueue free assumptions to process + for (const auto& fap : famap) + { + // A cycle is characterized by cur having an assumption being + // *currently* expanded that is seen again, i.e. in toConnect and not + // yet post-visited + auto itToConnect = toConnect.find(fap.first); + if (itToConnect != toConnect.end() && !visited[fap.first]) + { + // Since we have a cycle with an assumption, cur will be an + // assumption in the final proof node produced by this + // method. + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: cyclic assumption " + << fap.first << "\n"; + isCyclic = true; + break; + } + } + if (isCyclic) + { + visited[cur] = true; + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: Removing " << cur + << " from toConnect\n"; + auto itToConnect = toConnect.find(cur); + toConnect.erase(itToConnect); + continue; + } visit.push_back(cur); visited[cur] = false; } @@ -151,27 +191,11 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) visited[cur] = true; } // enqueue free assumptions to process - for (const std::pair>>& - fap : famap) + for (const auto& fap : famap) { - // check cycles - if (d_cyclic) - { - // cycles are assumptions being *currently* expanded and seen again, - // i.e. in toConnect and not yet post-visited - auto itToConnect = toConnect.find(fap.first); - if (itToConnect != toConnect.end() && !visited[fap.first]) - { - // Since we have a cycle with an assumption, this fact will be an - // assumption in the final proof node produced by this - // method. Thus we erase it as something to be connected, which - // will keep it as an assumption. - Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: " - "removing cyclic assumption " - << fap.first << " from expansion\n"; - continue; - } - } + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: marking " << fap.first + << " for revisit and for expansion\n"; // We always add assumptions to visit so that their last seen occurrence // is expanded (rather than the first seen occurrence, if we were not // adding assumptions, say, in assumptionsToExpand). This is so because @@ -244,6 +268,7 @@ std::shared_ptr LazyCDProofChain::getProofFor(Node fact) d_manager->updateNode(pfn.get(), npfn.second.get()); } } + Trace("lazy-cdproofchain") << "===========\n"; // final proof of fact auto it = toConnect.find(fact); if (it == toConnect.end()) diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 74617a521..0b3f28c61 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -634,23 +634,23 @@ void SatProofManager::finalizeProof(Node inConflictNode, { for (const Node& fa : fassumps) { - Trace("sat-proof") << "- "; auto it = d_cnfStream->getTranslationCache().find(fa); if (it != d_cnfStream->getTranslationCache().end()) { - Trace("sat-proof") << it->second << "\n"; + Trace("sat-proof") << "- " << it->second << "\n"; Trace("sat-proof") << " - " << fa << "\n"; continue; } // then it's a clause + std::stringstream ss; Assert(fa.getKind() == kind::OR); for (const Node& n : fa) { it = d_cnfStream->getTranslationCache().find(n); Assert(it != d_cnfStream->getTranslationCache().end()); - Trace("sat-proof") << it->second << " "; + ss << it->second << " "; } - Trace("sat-proof") << "\n"; + Trace("sat-proof") << "- " << ss.str() << "\n"; Trace("sat-proof") << " - " << fa << "\n"; } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b6ccbcc54..13434f829 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -872,6 +872,7 @@ set(regress_0_tests regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 + regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 regress0/proofs/scope.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 diff --git a/test/regress/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 b/test/regress/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 new file mode 100644 index 000000000..dfd30e1fd --- /dev/null +++ b/test/regress/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --check-proofs --proof-check=eager +; EXPECT: unsat +(set-logic ALL) +(declare-const x Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (and (ite c x false) (ite (or x d) (not b) x) (ite d (= b (ite b true d)) b))) +(check-sat)