Avoid use of extended rewriter in strings proof reconstruction, no use of REWRITE in final string proofs again

2 files changed, 20 insertions, 7 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index fe7071bcb..6099b7274 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1028,7 +1028,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       if (retCurr != ret)
       {
         // try to prove the rewritten form is equal to the extended rewritten
-        // form
+        // form, treated as a stand alone (theory) rewrite
         Node eqp = retCurr.eqNode(ret);
         std::vector<Node> targs;
         targs.push_back(eqp);
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index d2401653b..27e88cf00 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -259,13 +259,8 @@ void InferProofCons::convert(InferenceId infer,
       childrenSRew.push_back(pmainEq);
       childrenSRew.insert(childrenSRew.end(), pcsr.begin(), pcsr.end());
       // now, conclude the proper equality
-      std::vector<Node> argsSRew;
-      addMethodIds(argsSRew,
-                   MethodId::SB_DEFAULT,
-                   MethodId::SBA_SEQUENTIAL,
-                   MethodId::RW_EXT_REWRITE);
       Node mainEqSRew =
-          psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, argsSRew);
+          psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {});
       if (CDProof::isSame(mainEqSRew, pmainEq))
       {
         Trace("strings-ipc-core") << "...undo step" << std::endl;
@@ -343,6 +338,24 @@ void InferProofCons::convert(InferenceId infer,
           Trace("strings-ipc-core") << "...success!" << std::endl;
         }
       }
+      else if (infer == InferenceId::STRINGS_F_NCTN || infer == InferenceId::STRINGS_N_NCTN)
+      {
+        // May require extended equality rewrite, applied after the rewrite
+        // above. Notice we need both in sequence since ext equality rewriting
+        // is not recursive.
+        std::vector<Node> argsERew;
+        addMethodIds(argsERew,
+                    MethodId::SB_DEFAULT,
+                    MethodId::SBA_SEQUENTIAL,
+                    MethodId::RW_REWRITE_EQ_EXT);
+        Node mainEqERew =
+              psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, {mainEqCeq}, argsERew);
+        if (mainEqERew == conc)
+        {
+          useBuffer = true;
+          Trace("strings-ipc-core") << "...success!" << std::endl;
+        }
+      }
       else
       {
         std::vector<Node> tvec;