From 88f1d4e1b1ae8c7b320ec357fb02fdecbc096f7b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 6 May 2022 17:36:04 -0500
Subject: [PATCH] Fallback for sequential substitution proof reconstruction
 (#8730)

This makes our proof reconstruction fallback to a trivial sequential reconstruction in very rare cases where a sequential substitution fails to reconstruct. This can happen in some rare cases where terms are used in the domain of a substitution that otherwise would be modified by earlier substitutions. This occurs on 2 QF_SLIA benchmarks, attached is a delta-debugged version.

This also changes a warning message to a trace for this case, as a warning message may cause LFSC proof checking to fail when it should just give a warning for a TRUST_SUBS step, which is the default behavior regardless.
---
 src/smt/proof_post_processor.cpp              | 52 +++++++++++++++----
 test/regress/cli/CMakeLists.txt               |  1 +
 .../cli/regress2/strings/dd.trust-subs.smt2   |  7 +++
 3 files changed, 49 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/cli/regress2/strings/dd.trust-subs.smt2

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 202cb1292..7317ed351 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -952,19 +952,49 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     Node ts = builtin::BuiltinProofRuleChecker::applySubstitution(
         t, children, ids, ida);
     Node eqq = t.eqNode(ts);
+    // should have the same conclusion, if not, then tcpg does not agree with
+    // the substitution.
     if (eq != eqq)
     {
-      pfn = nullptr;
-    }
-    // should give a proof, if not, then tcpg does not agree with the
-    // substitution.
-    if (pfn == nullptr)
-    {
-      warning() << "resort to TRUST_SUBS" << std::endl
-                << eq << std::endl
-                << eqq << std::endl
-                << "from " << children << " applied to " << t << std::endl;
-      cdp->addStep(eqq, PfRule::TRUST_SUBS, {}, {eqq});
+      // this can happen in very rare cases where e.g. x -> a; f(x) -> b
+      // and t*{x -> a} = t*{x -> a}*{f(x) -> b} != t*{x -> a, f(x) -> b}
+      if (ida == MethodId::SBA_SEQUENTIAL && vsList.size() > 1)
+      {
+        Trace("smt-proof-pp-debug")
+            << "resort to sequential reconstruction" << std::endl;
+        // just do the naive sequential reconstruction,
+        // (SUBS F1 ... Fn t) ---> (TRANS (SUBS F1 t) ... (SUBS Fn tn))
+        Node curr = t;
+        std::vector<Node> transChildren;
+        for (size_t i = 0, nvs = vsList.size(); i < nvs; i++)
+        {
+          size_t ii = nvs - 1 - i;
+          TNode var = vsList[ii];
+          TNode subs = ssList[ii];
+          Node next = curr.substitute(var, subs);
+          if (next != curr)
+          {
+            Node eqo = curr.eqNode(next);
+            transChildren.push_back(eqo);
+            // ensure the proof for the substitution exists
+            addProofForSubsStep(var, subs, fromList[ii], cdp);
+            // do the single step SUBS on curr with the default arguments
+            cdp->addStep(eqo, PfRule::SUBS, {var.eqNode(subs)}, {curr});
+            curr = next;
+          }
+        }
+        Assert(curr == ts);
+        cdp->addStep(eqq, PfRule::TRANS, transChildren, {});
+      }
+      else
+      {
+        Trace("smt-proof-pp-debug")
+            << "resort to TRUST_SUBS" << std::endl
+            << eq << std::endl
+            << eqq << std::endl
+            << "from " << children << " applied to " << t << std::endl;
+        cdp->addStep(eqq, PfRule::TRUST_SUBS, {}, {eqq});
+      }
     }
     else
     {
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index adc3ec611..15977b980 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2949,6 +2949,7 @@ set(regress_2_tests
   regress2/strings/cmu-disagree-0707-dd.smt2
   regress2/strings/cmu-prereg-fmf.smt2
   regress2/strings/cmu-repl-len-nterm.smt2
+  regress2/strings/dd.trust-subs.smt2
   regress2/strings/issue3203.smt2
   regress2/strings/issue5381.smt2
   regress2/strings/issue6483.smt2
diff --git a/test/regress/cli/regress2/strings/dd.trust-subs.smt2 b/test/regress/cli/regress2/strings/dd.trust-subs.smt2
new file mode 100644
index 000000000..28c980036
--- /dev/null
+++ b/test/regress/cli/regress2/strings/dd.trust-subs.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (distinct (str.replace (str.replace "B" x y) "A" x) (str.replace "B" x (str.replace y "A" x))))
+(check-sat)
-- 
2.30.2