From dd850b74cb3ff5ab043ccfa124443791dcbcc0bf Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Oct 2021 10:45:19 -0500
Subject: [PATCH] Properly guard proof construction for STRINGS_EXTF_EQ_REW
 (#7519)

Fixes one of the issues raised in cvc5/cvc5-projects#331, the other involves missing skolem definitions for str.replace_all_re @4tXJ7f .

This properly guards cases of proof reconstruction for STRINGS_EXTF_EQ_REW where an intermediate step in the proof checker inferring something stronger than what it is asked to prove. In particular, substitution+rewriting is more powerful than congruence+rewriting:
s=x => (str.<= t s) ----> (= r "") since (str.<= t "") ----> (= r "")
but additionally:
(str.<= t s) * { s -> x } ----> true, which is possible if s occurs as a subterm of t.

The proof reconstruction for STRINGS_EXTF_EQ_REW is not precise as there are several other aspects that are not covered. After this PR, we properly guard and fail to reconstruct if the above issue arises, so the assertion failure will not throw.
---
 src/theory/strings/extf_solver.cpp      | 15 +++++++++------
 src/theory/strings/infer_proof_cons.cpp | 17 +++++++++++++++++
 2 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 4b12d2673..2de9bda96 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -259,6 +259,7 @@ void ExtfSolver::checkExtfEval(int effort)
   {
     // Setup information about n, including if it is equal to a constant.
     ExtfInfoTmp& einfo = d_extfInfoTmp[n];
+    Assert(einfo.d_exp.empty());
     Node r = d_state.getRepresentative(n);
     einfo.d_const = d_bsolver.getConstantEqc(r);
     // Get the current values of the children of n.
@@ -292,8 +293,8 @@ void ExtfSolver::checkExtfEval(int effort)
       Node sn = nm->mkNode(n.getKind(), schildren);
       Trace("strings-extf-debug")
           << "Check extf " << n << " == " << sn
-          << ", constant = " << einfo.d_const << ", effort=" << effort << "..."
-          << std::endl;
+          << ", constant = " << einfo.d_const << ", effort=" << effort
+          << ", exp " << exp << std::endl;
       einfo.d_exp.insert(einfo.d_exp.end(), exp.begin(), exp.end());
       // inference is rewriting the substituted node
       Node nrc = Rewriter::rewrite(sn);
@@ -490,8 +491,9 @@ void ExtfSolver::checkExtfInference(Node n,
     return;
   }
   NodeManager* nm = NodeManager::currentNM();
-  Trace("strings-extf-infer") << "checkExtfInference: " << n << " : " << nr
-                              << " == " << in.d_const << std::endl;
+  Trace("strings-extf-infer")
+      << "checkExtfInference: " << n << " : " << nr << " == " << in.d_const
+      << " with exp " << in.d_exp << std::endl;
 
   // add original to explanation
   if (n.getType().isBoolean())
@@ -662,8 +664,9 @@ void ExtfSolver::checkExtfInference(Node n,
   if (inferEqrr != inferEqr)
   {
     inferEqrr = Rewriter::rewrite(inferEqrr);
-    Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
-                                << " ...reduces to " << inferEqrr << std::endl;
+    Trace("strings-extf-infer")
+        << "checkExtfInference: " << inferEq << " ...reduces to " << inferEqrr
+        << " with explanation " << in.d_exp << std::endl;
     d_im.sendInternalInference(in.d_exp, inferEqrr, InferenceId::STRINGS_EXTF_EQ_REW);
   }
 }
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 5eba8663a..5090b15cb 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -217,18 +217,35 @@ void InferProofCons::convert(InferenceId infer,
       Node src = ps.d_children[ps.d_children.size() - 1];
       std::vector<Node> expe(ps.d_children.begin(), ps.d_children.end() - 1);
       // start with a default rewrite
+      Trace("strings-ipc-core")
+          << "Generate proof for STRINGS_EXTF_EQ_REW, starting with " << src
+          << std::endl;
       Node mainEqSRew = psb.applyPredElim(src, expe);
+      Trace("strings-ipc-core")
+          << "...after pred elim: " << mainEqSRew << std::endl;
       if (mainEqSRew == conc)
       {
+        Trace("strings-ipc-core") << "...success" << std::endl;
         useBuffer = true;
         break;
       }
+      else if (mainEqSRew.getKind() != EQUAL)
+      {
+        // Note this can happen in rare cases where substitution+rewriting
+        // is more powerful than congruence+rewriting. We fail to reconstruct
+        // the proof in this case.
+        Trace("strings-ipc-core")
+            << "...failed, not equality after rewriting" << std::endl;
+        break;
+      }
       // may need the "extended equality rewrite"
       Node mainEqSRew2 = psb.applyPredElim(mainEqSRew,
                                            {},
                                            MethodId::SB_DEFAULT,
                                            MethodId::SBA_SEQUENTIAL,
                                            MethodId::RW_REWRITE_EQ_EXT);
+      Trace("strings-ipc-core")
+          << "...after extended equality rewrite: " << mainEqSRew2 << std::endl;
       if (mainEqSRew2 == conc)
       {
         useBuffer = true;
-- 
2.30.2