diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-15 07:24:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-15 12:24:28 +0000 |
commit | b4469530d2f6de599ddf7207a1914b88be49de5b (patch) | |
tree | c89ea3bb1abd21faa609986dd63aebcf9a9ebb07 /src/theory | |
parent | cf4b6eab2f451a29cf0ca3b94b02c32c22b273a4 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.h | 5 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 15 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.h | 9 | ||||
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 5 |
5 files changed, 30 insertions, 9 deletions
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<InferInfo>(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<InferProofCons> 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<InferProofCons> 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<Node> 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<Node> iexp = nf_exp; iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF); |