From: Andrew Reynolds Date: Wed, 2 Feb 2022 14:46:48 +0000 (-0600) Subject: Extend proof step buffer to optionally ensure unique conclusions (#8017) X-Git-Tag: cvc5-1.0.0~481 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=908f725bf8bc70d53a7aa87e9d890f7b62a633a2;p=cvc5.git Extend proof step buffer to optionally ensure unique conclusions (#8017) Fixes cvc5/cvc5-projects#439. This extended (theory) proof step buffer with options for discarding duplicate conclusions. This option is now used in the strings theory proof construction, which may have duplication of conclusions due to purification. It simplifies some of the logic regarding popStep in this utility which is required due to the new policy. --- diff --git a/src/proof/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp index 309802505..0de55f043 100644 --- a/src/proof/proof_step_buffer.cpp +++ b/src/proof/proof_step_buffer.cpp @@ -15,6 +15,7 @@ #include "proof/proof_step_buffer.h" +#include "proof/proof.h" #include "proof/proof_checker.h" using namespace cvc5::kind; @@ -47,15 +48,31 @@ std::ostream& operator<<(std::ostream& out, ProofStep step) return out; } -ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {} +ProofStepBuffer::ProofStepBuffer(ProofChecker* pc, + bool ensureUnique, + bool autoSym) + : d_autoSym(autoSym), d_checker(pc), d_ensureUnique(ensureUnique) +{ +} Node ProofStepBuffer::tryStep(PfRule id, const std::vector& children, const std::vector& args, Node expected) +{ + bool added; + return tryStep(added, id, children, args, expected); +} + +Node ProofStepBuffer::tryStep(bool& added, + PfRule id, + const std::vector& children, + const std::vector& args, + Node expected) { if (d_checker == nullptr) { + added = false; Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker."; return Node::null(); } @@ -64,19 +81,44 @@ Node ProofStepBuffer::tryStep(PfRule id, if (!res.isNull()) { // add proof step - d_steps.push_back( - std::pair(res, ProofStep(id, children, args))); + added = addStep(id, children, args, res); + } + else + { + added = false; } return res; } -void ProofStepBuffer::addStep(PfRule id, +bool ProofStepBuffer::addStep(PfRule id, const std::vector& children, const std::vector& args, Node expected) { + if (d_ensureUnique) + { + if (d_allSteps.find(expected) != d_allSteps.end()) + { + Trace("psb-debug") << "Discard " << expected << " from " << id + << std::endl; + return false; + } + d_allSteps.insert(expected); + // if we are automatically considering symmetry, we also add the symmetric + // fact here + if (d_autoSym) + { + Node sexpected = CDProof::getSymmFact(expected); + if (!sexpected.isNull()) + { + d_allSteps.insert(sexpected); + } + } + Trace("psb-debug") << "Add " << expected << " from " << id << std::endl; + } d_steps.push_back( std::pair(expected, ProofStep(id, children, args))); + return true; } void ProofStepBuffer::addSteps(ProofStepBuffer& psb) @@ -96,6 +138,10 @@ void ProofStepBuffer::popStep() Assert(!d_steps.empty()); if (!d_steps.empty()) { + if (d_ensureUnique) + { + d_allSteps.erase(d_steps.back().first); + } d_steps.pop_back(); } } @@ -107,6 +153,10 @@ const std::vector>& ProofStepBuffer::getSteps() const return d_steps; } -void ProofStepBuffer::clear() { d_steps.clear(); } +void ProofStepBuffer::clear() +{ + d_steps.clear(); + d_allSteps.clear(); +} } // namespace cvc5 diff --git a/src/proof/proof_step_buffer.h b/src/proof/proof_step_buffer.h index 4c1bfa8a3..227de5f96 100644 --- a/src/proof/proof_step_buffer.h +++ b/src/proof/proof_step_buffer.h @@ -56,7 +56,19 @@ std::ostream& operator<<(std::ostream& out, ProofStep step); class ProofStepBuffer { public: - ProofStepBuffer(ProofChecker* pc = nullptr); + /** + * @param pc The proof checker we are using + * @param ensureUnique Whether we ensure that the conclusions of steps + * added to this buffer are unique. Later steps with the same conclusion as + * a previous one are discarded. + * @param autoSym Whether this proof step buffer is considering symmetry + * automatically. For example, this should be true if the steps of this buffer + * are being added to a CDProof with automatic symmetry. This impacts + * uniqueness of conclusions and whether certain steps are necessary. + */ + ProofStepBuffer(ProofChecker* pc = nullptr, + bool ensureUnique = false, + bool autoSym = true); ~ProofStepBuffer() {} /** * Returns the conclusion of the proof step, as determined by the proof @@ -70,8 +82,18 @@ class ProofStepBuffer const std::vector& children, const std::vector& args, Node expected = Node::null()); - /** Same as above, without checking */ - void addStep(PfRule id, + /** Same as try step, but tracks whether a step was added */ + Node tryStep(bool& added, + PfRule id, + const std::vector& children, + const std::vector& args, + Node expected = Node::null()); + /** + * Same as above, without checking + * @return true if a step was added. This may return false if e.g. expected + * was a duplicate conclusion. + */ + bool addStep(PfRule id, const std::vector& children, const std::vector& args, Node expected); @@ -86,11 +108,23 @@ class ProofStepBuffer /** Clear */ void clear(); + protected: + /** + * Whether this proof step buffer is being added to a CDProof with automatic + * symmetry. This impacts uniqueness of conclusions and whether certain + * steps are necessary. + */ + bool d_autoSym; + private: /** The proof checker*/ ProofChecker* d_checker; /** the queued proof steps */ std::vector> d_steps; + /** Whether we are ensuring the conclusions in the buffer are unique */ + bool d_ensureUnique; + /** The set of conclusions in steps */ + std::unordered_set d_allSteps; }; } // namespace cvc5 diff --git a/src/proof/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp index 79e98471d..1f6dc6442 100644 --- a/src/proof/theory_proof_step_buffer.cpp +++ b/src/proof/theory_proof_step_buffer.cpp @@ -21,8 +21,10 @@ using namespace cvc5::kind; namespace cvc5 { -TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc) - : ProofStepBuffer(pc) +TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc, + bool ensureUnique, + bool autoSym) + : ProofStepBuffer(pc, ensureUnique, autoSym) { } @@ -36,7 +38,8 @@ bool TheoryProofStepBuffer::applyEqIntro(Node src, std::vector args; args.push_back(src); addMethodIds(args, ids, ida, idr); - Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args); + bool added; + Node res = tryStep(added, PfRule::MACRO_SR_EQ_INTRO, exp, args); if (res.isNull()) { // failed to apply @@ -47,7 +50,10 @@ bool TheoryProofStepBuffer::applyEqIntro(Node src, if (res != expected) { // did not provide the correct target - popStep(); + if (added) + { + popStep(); + } return false; } // successfully proved src == tgt. @@ -62,7 +68,7 @@ bool TheoryProofStepBuffer::applyPredTransform(Node src, MethodId idr) { // symmetric equalities - if (CDProof::isSame(src, tgt)) + if (d_autoSym && CDProof::isSame(src, tgt)) { return true; } @@ -113,8 +119,9 @@ Node TheoryProofStepBuffer::applyPredElim(Node src, children.insert(children.end(), exp.begin(), exp.end()); std::vector args; addMethodIds(args, ids, ida, idr); - Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); - if (CDProof::isSame(src, srcRew)) + bool added; + Node srcRew = tryStep(added, PfRule::MACRO_SR_PRED_ELIM, children, args); + if (d_autoSym && added && CDProof::isSame(src, srcRew)) { popStep(); } diff --git a/src/proof/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h index ac58d3718..e4b4debd0 100644 --- a/src/proof/theory_proof_step_buffer.h +++ b/src/proof/theory_proof_step_buffer.h @@ -33,7 +33,9 @@ namespace cvc5 { class TheoryProofStepBuffer : public ProofStepBuffer { public: - TheoryProofStepBuffer(ProofChecker* pc = nullptr); + TheoryProofStepBuffer(ProofChecker* pc = nullptr, + bool ensureUnique = false, + bool autoSym = true); ~TheoryProofStepBuffer() {} //---------------------------- utilities builtin proof rules /** diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 1bed68dc7..9f0c2cb3f 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -73,7 +73,8 @@ bool InferProofCons::addProofTo(CDProof* pf, // now go back and convert it to proof steps and add to proof bool useBuffer = false; ProofStep ps; - TheoryProofStepBuffer psb(pf->getManager()->getChecker()); + // ensure proof steps are unique + TheoryProofStepBuffer psb(pf->getManager()->getChecker(), true); // run the conversion convert(infer, isRev, conc, exp, ps, psb, useBuffer); // make the proof based on the step or the buffer @@ -159,6 +160,14 @@ void InferProofCons::convert(InferenceId infer, } // try to find a set of proof steps to incorporate into the buffer psb.clear(); + // explicitly add ASSUME steps to the proof step buffer for premises of the + // inference, so that they will not be overwritten in the reconstruction + // below + for (const Node& ec : ps.d_children) + { + Trace("strings-ipc-debug") << "Explicit add " << ec << std::endl; + psb.addStep(PfRule::ASSUME, {}, {ec}, ec); + } NodeManager* nm = NodeManager::currentNM(); Node nodeIsRev = nm->mkConst(isRev); switch (infer) @@ -354,19 +363,15 @@ void InferProofCons::convert(InferenceId infer, { break; } + Trace("strings-ipc-core") + << "Main equality after purify " << pmainEq << std::endl; std::vector childrenSRew; childrenSRew.push_back(pmainEq); childrenSRew.insert(childrenSRew.end(), pcsr.begin(), pcsr.end()); // now, conclude the proper equality Node mainEqSRew = psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {}); - if (CDProof::isSame(mainEqSRew, pmainEq)) - { - Trace("strings-ipc-core") << "...undo step" << std::endl; - // the rule added above was not necessary - psb.popStep(); - } - else if (mainEqSRew == conc) + if (mainEqSRew == conc) { Trace("strings-ipc-core") << "...success after rewrite!" << std::endl; useBuffer = true; @@ -387,12 +392,6 @@ void InferProofCons::convert(InferenceId infer, // fail break; } - else if (mainEqCeq == mainEqSRew) - { - Trace("strings-ipc-core") << "...undo step" << std::endl; - // not necessary, probably first component of equality - psb.popStep(); - } // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the // inference involved t and s. if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ @@ -583,12 +582,6 @@ void InferProofCons::convert(InferenceId infer, Node mainEqMain = psb.tryStep(rule, childrenMain, argsMain); Trace("strings-ipc-core") << "Main equality after " << rule << " " << mainEqMain << std::endl; - if (mainEqMain == mainEqCeq) - { - Trace("strings-ipc-core") << "...undo step" << std::endl; - // not necessary, probably first component of equality - psb.popStep(); - } // either equal or rewrites to it std::vector cexp; if (psb.applyPredTransform(mainEqMain, conc, cexp)) diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 6022f5443..cde81c365 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -137,7 +137,7 @@ class InferProofCons : public ProofGenerator * true. In this case, the argument psb is updated to contain (possibly * multiple) proof steps for how to construct a proof for the given inference. * In particular, psb will contain a set of steps that form a proof - * whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant. + * whose conclusion is conc and whose free assumptions are exp. */ static void convert(InferenceId infer, bool isRev, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ec3b13caa..6c7862d1e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2755,6 +2755,7 @@ set(regress_2_tests regress2/strings/issue6639-replace-re-all.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 + regress2/strings/proj-439-cyclic-str-ipc.smt2 regress2/strings/proof-fail-083021-delta.smt2 regress2/strings/range-perf.smt2 regress2/strings/repl-repl-i-no-push.smt2 diff --git a/test/regress/regress2/strings/proj-439-cyclic-str-ipc.smt2 b/test/regress/regress2/strings/proj-439-cyclic-str-ipc.smt2 new file mode 100644 index 000000000..5a6927e1b --- /dev/null +++ b/test/regress/regress2/strings/proj-439-cyclic-str-ipc.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-const x Int) +(declare-fun u () String) +(assert (and (not (= 0 (ite (str.prefixof "mo" u) 1 0))) (not (= 0 (ite (str.contains (str.substr (str.substr u 10 (str.len u)) 0 (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0))) "W") 1 0))) (= 0 (ite (not (= "aost" (str.++ (str.substr (str.substr u 1 (str.len u)) 0 (str.indexof (str.substr (str.substr u 10 (str.len u)) (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0)) (str.len (str.substr u 0 (str.len u)))) "W" 0)) (str.substr (str.++ (str.replace (str.substr (str.substr u 10 (str.len u)) 0 (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0))) "A" "a") (str.substr u 0 x)) (+ 1 (str.indexof (str.substr (str.substr u 10 (str.len u)) (+ 1 (str.indexof (str.substr u 10 (str.len u)) "A" 0)) (str.len (str.substr u 0 (str.len u)))) "W" 0)) (str.len (str.substr u 0 (str.len u))))))) 1 0)))) +(check-sat)