From 54eac4f9781d9c07446453697128c4bd036c110d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Jul 2021 16:15:28 -0500 Subject: [PATCH] Fix for context on input proof generator (#6873) The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent. This also refactors the debugging traces in this class. --- src/smt/preprocess_proof_generator.cpp | 37 +++++++++++++------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/proofs/cyclic-ucp.smt2 | 10 ++++++ 3 files changed, 36 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress0/proofs/cyclic-ucp.smt2 diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 12a802f14..5511800a1 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -36,7 +36,7 @@ PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, d_ctx(c ? c : &d_context), d_src(d_ctx), d_helperProofs(pnm, d_ctx), - d_inputPf(pnm, nullptr), + d_inputPf(pnm, c, "InputProof"), d_name(name), d_ra(ra), d_rpp(rpp) @@ -50,12 +50,18 @@ void PreprocessProofGenerator::notifyInput(Node n) void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) { + if (n.isConst() && n.getConst()) + { + // ignore true assertions + return; + } Trace("smt-proof-pp-debug") - << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl; + << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n + << " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl; if (d_src.find(n) == d_src.end()) { // if no proof generator provided for (non-true) assertion - if (pg == nullptr && (!n.isConst() || !n.getConst())) + if (pg == nullptr) { checkEagerPedantic(d_ra); } @@ -95,8 +101,7 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp) Assert(tnp.getKind() == TrustNodeKind::REWRITE); Node np = tnp.getNode(); Trace("smt-proof-pp-debug") - << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven() - << std::endl; + << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl; if (d_src.find(np) == d_src.end()) { if (tnp.getGenerator() == nullptr) @@ -113,17 +118,19 @@ void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp) std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) { + Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name + << ") input " << f << std::endl; NodeTrustNodeMap::iterator it = d_src.find(f); if (it == d_src.end()) { + Trace("smt-pppg") << "...no proof for " << identify() << " " << f + << std::endl; // could be an assumption, return nullptr return nullptr; } // make CDProof to construct the proof below CDProof cdp(d_pnm); - Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name - << ") input " << f << std::endl; Node curr = f; std::vector transChildren; std::unordered_set processed; @@ -150,27 +157,30 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) bool proofStepProcessed = false; // if a generator for the step was provided, it is stored in the proof - Trace("smt-pppg") << "...get provided proof" << std::endl; + Trace("smt-pppg-debug") + << "...get provided proof " << (*it).second << std::endl; std::shared_ptr pfr = (*it).second.toProofNode(); if (pfr != nullptr) { - Trace("smt-pppg") << "...add provided" << std::endl; + Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl; Assert(pfr->getResult() == proven); cdp.addProof(pfr); proofStepProcessed = true; } - Trace("smt-pppg") << "...update" << std::endl; + Trace("smt-pppg-debug") << "...update" << std::endl; TrustNodeKind tnk = (*it).second.getKind(); if (tnk == TrustNodeKind::REWRITE) { - Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl; + Trace("smt-pppg-debug") + << "...rewritten from " << proven[0] << std::endl; Assert(proven.getKind() == kind::EQUAL); if (!proofStepProcessed) { // maybe its just a simple rewrite? if (proven[1] == theory::Rewriter::rewrite(proven[0])) { + Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl; cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]}); proofStepProcessed = true; } @@ -180,6 +190,7 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) curr = proven[0]; success = true; // find the next node + Trace("smt-pppg") << "...continue " << curr << std::endl; it = d_src.find(curr); } else @@ -190,7 +201,9 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) if (!proofStepProcessed) { - Trace("smt-pppg") << "...add missing step" << std::endl; + Trace("smt-pppg-debug") + << "...justify missing step with " + << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl; // add trusted step, the rule depends on the kind of trust node cdp.addStep( proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven}); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 39fa83311..205729553 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -827,6 +827,7 @@ set(regress_0_tests regress0/printer/let_shadowing.smt2 regress0/printer/symbol_starting_w_digit.smt2 regress0/printer/tuples_and_records.cvc + regress0/proofs/cyclic-ucp.smt2 regress0/proofs/issue277-circuit-propagator.smt2 regress0/proofs/open-pf-if-unordered-iff.smt2 regress0/proofs/scope.smt2 diff --git a/test/regress/regress0/proofs/cyclic-ucp.smt2 b/test/regress/regress0/proofs/cyclic-ucp.smt2 new file mode 100644 index 000000000..1fe29c262 --- /dev/null +++ b/test/regress/regress0/proofs/cyclic-ucp.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -i +; EXPECT: unsat +; EXPECT: unsat +(set-logic ALL) +(push) +(assert (= "A" "")) +(check-sat) +(pop) +(assert (= "" "A")) +(check-sat) -- 2.30.2