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.

7 files changed, 46 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);
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)