(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)

This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function).

This allows us to justify the regular expression inclusion inference as a rewrite.

5 files changed, 41 insertions, 8 deletions

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index f1a818bf3..2953a2b3c 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -70,6 +70,7 @@ const char* toString(Rewrite r)
     case Rewrite::ITOS_EVAL: return "ITOS_EVAL";
     case Rewrite::RE_AND_EMPTY: return "RE_AND_EMPTY";
     case Rewrite::RE_ANDOR_FLATTEN: return "RE_ANDOR_FLATTEN";
+    case Rewrite::RE_ANDOR_INC_CONFLICT: return "RE_ANDOR_INC_CONFLICT";
     case Rewrite::RE_CHAR_IN_STR_STAR: return "RE_CHAR_IN_STR_STAR";
     case Rewrite::RE_CONCAT: return "RE_CONCAT";
     case Rewrite::RE_CONCAT_FLATTEN: return "RE_CONCAT_FLATTEN";
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index cfa8c8448..7a315ebd3 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -75,6 +75,7 @@ enum class Rewrite : uint32_t
   ITOS_EVAL,
   RE_AND_EMPTY,
   RE_ANDOR_FLATTEN,
+  RE_ANDOR_INC_CONFLICT,
   RE_CHAR_IN_STR_STAR,
   RE_CONCAT,
   RE_CONCAT_FLATTEN,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index d8b8765eb..aa85d1056 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -920,6 +920,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
   Trace("strings-rewrite-debug")
       << "Strings::rewriteAndOrRegExp start " << node << std::endl;
   std::vector<Node> node_vec;
+  std::vector<Node> polRegExp[2];
   for (const Node& ni : node)
   {
     if (ni.getKind() == nk)
@@ -951,20 +952,48 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
     else if (std::find(node_vec.begin(), node_vec.end(), ni) == node_vec.end())
     {
       node_vec.push_back(ni);
+      uint32_t pindex = ni.getKind() == REGEXP_COMPLEMENT ? 1 : 0;
+      Node nia = pindex == 1 ? ni[0] : ni;
+      polRegExp[pindex].push_back(nia);
     }
   }
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<Node> nvec;
+  std::vector<Node> emptyVec;
+  // use inclusion tests
+  for (const Node& negMem : polRegExp[1])
+  {
+    for (const Node& posMem : polRegExp[0])
+    {
+      Node m1 = nk == REGEXP_INTER ? negMem : posMem;
+      Node m2 = nk == REGEXP_INTER ? posMem : negMem;
+      // inclusion test for conflicting case m1 contains m2
+      // (re.inter (re.comp R1) R2) --> re.none where R1 includes R2
+      // (re.union R1 (re.comp R2)) --> (re.* re.allchar) where R1 includes R2
+      if (RegExpEntail::regExpIncludes(m1, m2))
+      {
+        Node retNode;
+        if (nk == REGEXP_INTER)
+        {
+          retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec);
+        }
+        else
+        {
+          retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
+        }
+        return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT);
+      }
+    }
+  }
   Node retNode;
   if (node_vec.empty())
   {
     if (nk == REGEXP_INTER)
     {
-      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, nvec));
+      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
     }
     else
     {
-      retNode = nm->mkNode(kind::REGEXP_EMPTY, nvec);
+      retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec);
     }
   }
   else
@@ -1442,6 +1471,7 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node)
                                    << node << " to " << retNode << std::endl;
     return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
   }
+  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return RewriteResponse(REWRITE_DONE, retNode);
 }
 
@@ -1746,7 +1776,6 @@ Node SequencesRewriter::rewriteSubstr(Node node)
       }
     }
   }
-  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
 
@@ -2103,7 +2132,6 @@ Node SequencesRewriter::rewriteContains(Node node)
     }
   }
 
-  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
 
@@ -2318,7 +2346,6 @@ Node SequencesRewriter::rewriteIndexof(Node node)
     }
   }
 
-  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
 
@@ -2806,7 +2833,6 @@ Node SequencesRewriter::rewriteReplace(Node node)
   // contains( t, s ) =>
   //   contains( replace( t, s, r ), r ) ----> true
 
-  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
 
@@ -2859,7 +2885,6 @@ Node SequencesRewriter::rewriteReplaceAll(Node node)
     return rri;
   }
 
-  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 506857479..2df07db5a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -964,6 +964,7 @@ set(regress_0_tests
   regress0/strings/parser-syms.cvc
   regress0/strings/quad-028-2-2-unsat.smt2
   regress0/strings/re.all.smt2
+  regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2
   regress0/strings/re_diff.smt2
   regress0/strings/regexp-native-simple.cvc
diff --git a/test/regress/regress0/strings/re-in-rewrite.smt2 b/test/regress/regress0/strings/re-in-rewrite.smt2
new file mode 100644
index 000000000..d1567768d
--- /dev/null
+++ b/test/regress/regress0/strings/re-in-rewrite.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () String)
+(assert (str.in_re x (re.inter (re.comp (re.++ re.allchar (re.* re.allchar))) (re.++ (str.to_re "a") (re.* re.allchar)))))
+(check-sat)