Flatten quantified formulas introduced for negative REGEXP unfolding (c…

…vc5#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

@@ -993,18 +993,16 @@ 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 =
         nm->mkNode(Kind::STRING_SUBSTR, s, b1, nm->mkNode(Kind::SUB, lens, b1));
     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;
 }