From: Andrew Reynolds Date: Fri, 15 Oct 2021 12:24:28 +0000 (-0500) Subject: Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366) X-Git-Tag: cvc5-1.0.0~1060 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4469530d2f6de599ddf7207a1914b88be49de5b;p=cvc5.git Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366) This makes string proof construction more robust by maintaining two separate proof inference constructors, one for facts and one for lemmas/conflicts. This avoids issues where 2 lemmas with the same conclusion (but possibly different explanations) are added in the same call to check. This fixes one of the two issues related to proofs for #6973. --- diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 34597c8be..5eba8663a 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -59,6 +59,11 @@ void InferProofCons::notifyFact(const InferInfo& ii) d_lazyFactMap.insert(ii.d_conc, iic); } +void InferProofCons::notifyLemma(const InferInfo& ii) +{ + d_lazyFactMap[ii.d_conc] = std::make_shared(ii); +} + bool InferProofCons::addProofTo(CDProof* pf, Node conc, InferenceId infer, diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 110d231cf..02b266fd7 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -69,6 +69,11 @@ class InferProofCons : public ProofGenerator * only for facts that are explained. */ void notifyFact(const InferInfo& ii); + /** + * Same as above, but always overwrites. This is used for lemmas and + * conflicts, which do not necessarily have unique conclusions. + */ + void notifyLemma(const InferInfo& ii); /** * This returns the proof for fact. This is required for using this class as diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 0e971fc54..1f531a97c 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -42,7 +42,8 @@ InferenceManager::InferenceManager(Env& env, d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) + d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr), + d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -279,12 +280,12 @@ void InferenceManager::processConflict(const InferInfo& ii) { Assert(!d_state.isInConflict()); // setup the fact to reproduce the proof in the call below - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } // make the trust node - TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get()); + TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get()); Assert(tconf.getKind() == TrustNodeKind::CONFLICT); Trace("strings-assert") << "(assert (not " << tconf.getNode() << ")) ; conflict " << ii.getId() << std::endl; @@ -335,11 +336,11 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) } // ensure that the proof generator is ready to explain the final conclusion // of the lemma (ii.d_conc). - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } - TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get()); + TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get()); Trace("strings-pending") << "Process pending lemma : " << tlem.getNode() << std::endl; diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 49f10d7cb..9f4cd1986 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -249,8 +249,15 @@ class InferenceManager : public InferenceManagerBuffered ExtTheory& d_extt; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; - /** Conversion from inferences to proofs */ + /** Conversion from inferences to proofs for facts */ std::unique_ptr d_ipc; + /** + * Conversion from inferences to proofs for lemmas and conflicts. This is + * separate from the above proof generator to avoid rare cases where the + * conclusion of a lemma is a duplicate of the conclusion of another lemma, + * or is a fact in the current equality engine. + */ + std::unique_ptr d_ipcl; /** Common constants */ Node d_true; Node d_false; diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 614a5e6e0..898c0f1b7 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -546,7 +546,10 @@ bool RegExpSolver::checkPDerivative( { std::vector noExplain; noExplain.push_back(atom); - noExplain.push_back(x.eqNode(d_emptyString)); + if (x != d_emptyString) + { + noExplain.push_back(x.eqNode(d_emptyString)); + } std::vector iexp = nf_exp; iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 54fb91db4..587b2d9d6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2204,6 +2204,7 @@ set(regress_1_tests regress1/strings/issue6653-rre-small.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 + regress1/strings/issue6973-dup-lemma-conc.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 new file mode 100644 index 000000000..4c6fe5c62 --- /dev/null +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun a () String) +(assert + (str.in_re "" + (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all))) + (str.to_re + (ite + (str.in_re "" + (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a "")) + (re.inter (str.to_re a) + (re.++ (str.to_re a) + (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all)))))) + a ""))))) +(check-sat)