(proof-new) Fix regular expression unfolding under substitution (#5958)

This case was previously unhandled and exercised by a recently added regression.

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index c3e1ce294c089399d91af09adcca10082a924a0b..3bbfc1c981d6c7a5c71b1ac1e846432ce92560c0 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -533,16 +533,34 @@ void InferProofCons::convert(InferenceId infer,
     case InferenceId::STRINGS_RE_UNFOLD_POS:
     case InferenceId::STRINGS_RE_UNFOLD_NEG:
     {
-      if (infer == InferenceId::STRINGS_RE_UNFOLD_POS)
+      Assert (!ps.d_children.empty());
+      size_t nchild = ps.d_children.size();
+      Node mem = ps.d_children[nchild-1];
+      if (nchild>1)
+      {
+        // if more than one, apply MACRO_SR_PRED_ELIM
+        std::vector<Node> tcs;
+        tcs.insert(tcs.end(),
+                          ps.d_children.begin(),
+                          ps.d_children.begin() + (nchild-1));
+        mem = psb.applyPredElim(mem, tcs);
+        useBuffer = true;
+      }
+      PfRule r = PfRule::UNKNOWN;
+      if (mem.isNull())
+      {
+        // failed to eliminate above
+        Assert(false) << "Failed to apply MACRO_SR_PRED_ELIM for RE unfold";
+        useBuffer = false;
+      }
+      else if (infer == InferenceId::STRINGS_RE_UNFOLD_POS)
       {
-        ps.d_rule = PfRule::RE_UNFOLD_POS;
+        r = PfRule::RE_UNFOLD_POS;
       }
       else
       {
-        ps.d_rule = PfRule::RE_UNFOLD_NEG;
+        r = PfRule::RE_UNFOLD_NEG;
         // it may be an optimized form of concat simplification
-        Assert(ps.d_children.size() == 1);
-        Node mem = ps.d_children[0];
         Assert(mem.getKind() == NOT && mem[0].getKind() == STRING_IN_REGEXP);
         if (mem[0][1].getKind() == REGEXP_CONCAT)
         {
@@ -552,10 +570,20 @@ void InferProofCons::convert(InferenceId infer,
           // version
           if (!reLen.isNull())
           {
-            ps.d_rule = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED;
+            r = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED;
           }
         }
       }
+      if (useBuffer)
+      {
+        mem = psb.tryStep(r, {mem}, {});
+        // should match the conclusion
+        useBuffer = (mem==conc);
+      }
+      else
+      {
+        ps.d_rule = r;
+      }
     }
     break;
     // ========================== Reduction