From 92fa7692b6b33ff308f73b687b269d7e5e43cf7f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 29 Apr 2024 21:18:22 -0500
Subject: [PATCH] Flatten quantified formulas introduced for negative REGEXP
 unfolding (#10684)

This modifies quantified formulas introduced for negative REGEXP unfolding so that they do not contain nested Boolean structure, i.e. (=> (and A B) C) is converted to (or (not A) (not B) C).

Note these rules have yet to be formalized so there is not an ALF signature for these yet.

This avoids the need for rewrite steps in the bodies of quantified formulas in final proofs, which moreover RARE fails to find in some cases.
---
 src/theory/strings/regexp_operation.cpp | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 1593bc7fb4a..b353250c02c 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -993,9 +993,8 @@ Node RegExpOpr::reduceRegExpNeg(Node mem)
     Node sne = s.eqNode(emp).negate();
     Node b1 = nm->mkBoundVar(nm->integerType());
     Node b1v = nm->mkNode(Kind::BOUND_VAR_LIST, b1);
-    Node g1 = nm->mkNode(Kind::AND,
-                         nm->mkNode(Kind::GT, b1, zero),
-                         nm->mkNode(Kind::GEQ, lens, b1));
+    Node g11n = nm->mkNode(Kind::GT, b1, zero).notNode();
+    Node g12n = nm->mkNode(Kind::GEQ, lens, b1).notNode();
     // internal
     Node s1 = nm->mkNode(Kind::STRING_SUBSTR, s, zero, b1);
     Node s2 =
@@ -1003,8 +1002,7 @@ Node RegExpOpr::reduceRegExpNeg(Node mem)
     Node s1r1 = nm->mkNode(Kind::STRING_IN_REGEXP, s1, r[0]).negate();
     Node s2r2 = nm->mkNode(Kind::STRING_IN_REGEXP, s2, r).negate();
 
-    conc = nm->mkNode(Kind::OR, s1r1, s2r2);
-    conc = nm->mkNode(Kind::IMPLIES, g1, conc);
+    conc = nm->mkNode(Kind::OR, {g11n, g12n, s1r1, s2r2});
     // must mark as an internal quantifier
     conc = utils::mkForallInternal(b1v, conc);
     conc = nm->mkNode(Kind::AND, sne, conc);
@@ -1037,15 +1035,14 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
   Node lens = nm->mkNode(Kind::STRING_LENGTH, s);
   Node b1;
   Node b1v;
-  Node guard;
+  Node guard1n, guard2n;
   if (reLen.isNull())
   {
     b1 = SkolemCache::mkIndexVar(mem);
     b1v = nm->mkNode(Kind::BOUND_VAR_LIST, b1);
-    guard = nm->mkNode(
-        Kind::AND,
-        nm->mkNode(Kind::GEQ, b1, zero),
-        nm->mkNode(Kind::GEQ, nm->mkNode(Kind::STRING_LENGTH, s), b1));
+    guard1n = nm->mkNode(Kind::GEQ, b1, zero).notNode();
+    guard2n =
+        nm->mkNode(Kind::GEQ, nm->mkNode(Kind::STRING_LENGTH, s), b1).notNode();
   }
   else
   {
@@ -1077,13 +1074,17 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
   }
   Node r2 = nvec.size() == 1 ? nvec[0] : nm->mkNode(Kind::REGEXP_CONCAT, nvec);
   Node s2r2 = nm->mkNode(Kind::STRING_IN_REGEXP, s2, r2).negate();
-  Node conc = nm->mkNode(Kind::OR, s1r1, s2r2);
+  Node conc;
   if (!b1v.isNull())
   {
-    conc = nm->mkNode(Kind::OR, guard.negate(), conc);
+    conc = nm->mkNode(Kind::OR, {guard1n, guard2n, s1r1, s2r2});
     // must mark as an internal quantifier
     conc = utils::mkForallInternal(b1v, conc);
   }
+  else
+  {
+    conc = nm->mkNode(Kind::OR, s1r1, s2r2);
+  }
   return conc;
 }