Do not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)

There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.

After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.

Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.

6 files changed, 72 insertions, 61 deletions

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 18a5b049a..dfe006a86 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -347,7 +347,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
         children2.push_back(res);
         Node body = nm->mkNode(AND, children2);
         Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars);
-        res = nm->mkNode(EXISTS, bvl, body);
+        res = utils::mkForallInternal(bvl, body.negate()).negate();
       }
       // must also give a minimum length requirement
       res = nm->mkNode(AND, res, nm->mkNode(GEQ, lenx, lenSum));
@@ -486,7 +486,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       if (k.getKind() == BOUND_VARIABLE)
       {
         Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
-        body = nm->mkNode(EXISTS, bvl, body);
+        body = utils::mkForallInternal(bvl, body.negate()).negate();
       }
       // e.g. x in re.++( R1, "AB", R2 ) --->
       //  exists k.
@@ -575,7 +575,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
                                              : nm->mkNode(OR, char_constraints);
     Node body = nm->mkNode(OR, bound.negate(), conc);
     Node bvl = nm->mkNode(BOUND_VAR_LIST, index);
-    Node res = nm->mkNode(FORALL, bvl, body);
+    Node res = utils::mkForallInternal(bvl, body);
     // e.g.
     //   x in (re.* (re.union "A" "B" )) --->
     //   forall k. 0<=k<len(x) => (substr(x,k,1) in "A" OR substr(x,k,1) in "B")
@@ -605,7 +605,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
                 .eqNode(s);
         Node body = nm->mkNode(OR, bound.negate(), conc);
         Node bvl = nm->mkNode(BOUND_VAR_LIST, index);
-        Node res = nm->mkNode(FORALL, bvl, body);
+        Node res = utils::mkForallInternal(bvl, body);
         res = nm->mkNode(
             AND, nm->mkNode(INTS_MODULUS_TOTAL, lenx, lens).eqNode(zero), res);
         // e.g.
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 106ce09d0..268368e7f 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -928,7 +928,8 @@ Node RegExpOpr::reduceRegExpNeg(Node mem)
 
     conc = nm->mkNode(OR, s1r1, s2r2);
     conc = nm->mkNode(IMPLIES, g1, conc);
-    conc = nm->mkNode(FORALL, b1v, conc);
+    // must mark as an internal quantifier
+    conc = utils::mkForallInternal(b1v, conc);
     conc = nm->mkNode(AND, sne, conc);
   }
   else
@@ -999,7 +1000,8 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
   if (!b1v.isNull())
   {
     conc = nm->mkNode(OR, guard.negate(), conc);
-    conc = nm->mkNode(FORALL, b1v, conc);
+    // must mark as an internal quantifier
+    conc = utils::mkForallInternal(b1v, conc);
   }
   return conc;
 }
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 5f21d6e65..550a9af8b 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -20,9 +20,9 @@
 #include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "smt/logic_exception.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
@@ -35,13 +35,6 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-/** Mapping to a dummy node for marking an attribute on internal quantified
- * formulas */
-struct QInternalVarAttributeId
-{
-};
-typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
-
 StringsPreprocess::StringsPreprocess(SkolemCache* sc,
                                      HistogramStat<Kind>* statReductions)
     : d_sc(sc), d_statReductions(statReductions)
@@ -299,7 +292,7 @@ Node StringsPreprocess::reduce(Node t,
     // forall il.
     //   n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
     //     ~in_re(substr(s, i, l), r)
-    Node firstMatch = mkForallInternal(bvl, body);
+    Node firstMatch = utils::mkForallInternal(bvl, body);
     Node bvll = nm->mkNode(BOUND_VAR_LIST, l);
     Node validLen =
         nm->mkNode(AND,
@@ -311,8 +304,10 @@ Node StringsPreprocess::reduce(Node t,
         nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, s, skk, l), r));
     // skk != -1 =>
     //   exists l. (0 <= l < len(s) - skk) ^ in_re(substr(s, skk, l), r))
-    Node match = nm->mkNode(
-        OR, retNegOne, mkForallInternal(bvll, matchBody.negate()).negate());
+    Node match =
+        nm->mkNode(OR,
+                   retNegOne,
+                   utils::mkForallInternal(bvll, matchBody.negate()).negate());
 
     // assert:
     // IF:   n > len(s) OR 0 > n
@@ -382,7 +377,7 @@ Node StringsPreprocess::reduce(Node t,
     Node ux1lem = nm->mkNode(GEQ, n, ux1);
 
     lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
-    lem = mkForallInternal(xbv, lem);
+    lem = utils::mkForallInternal(xbv, lem);
     conc.push_back(lem);
 
     Node nonneg = nm->mkNode(GEQ, n, zero);
@@ -470,7 +465,7 @@ Node StringsPreprocess::reduce(Node t,
     Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
 
     lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
-    lem = mkForallInternal(xbv, lem);
+    lem = utils::mkForallInternal(xbv, lem);
     conc2.push_back(lem);
 
     Node sneg = nm->mkNode(LT, stoit, zero);
@@ -651,7 +646,7 @@ Node StringsPreprocess::reduce(Node t,
         ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
 
     Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
-    Node q = mkForallInternal(bvli, body);
+    Node q = utils::mkForallInternal(bvli, body);
     lem.push_back(q);
 
     // assert:
@@ -717,7 +712,7 @@ Node StringsPreprocess::reduce(Node t,
         nm->mkNode(STRING_IN_REGEXP, nm->mkNode(STRING_SUBSTR, k2, zero, l), y)
             .negate());
     // forall l. 0 <= l < len(k2) => ~in_re(substr(k2, 0, l), r)
-    Node shortestMatch = mkForallInternal(bvll, body);
+    Node shortestMatch = utils::mkForallInternal(bvll, body);
     // in_re(k2, y)
     Node match = nm->mkNode(STRING_IN_REGEXP, k2, y);
     // k = k1 ++ z ++ k3
@@ -811,7 +806,7 @@ Node StringsPreprocess::reduce(Node t,
             .negate());
     // forall l. 0 < l < Ul(i + 1) =>
     //   ~in_re(substr(x, Uf(i + 1) - Ul(i + 1), l), y')
-    flem.push_back(mkForallInternal(bvll, shortestMatchBody));
+    flem.push_back(utils::mkForallInternal(bvll, shortestMatchBody));
     Node pfxMatch =
         nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi));
     // Us(i) = substr(x, Uf(i), ii - Uf(i)) ++ z ++ Us(i + 1)
@@ -820,7 +815,7 @@ Node StringsPreprocess::reduce(Node t,
             .eqNode(nm->mkNode(
                 STRING_CONCAT, pfxMatch, z, nm->mkNode(APPLY_UF, us, ip1))));
     Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
-    Node forall = mkForallInternal(bvli, body);
+    Node forall = utils::mkForallInternal(bvli, body);
     lemmas.push_back(forall);
 
     // IF indexof(x, y', 0) = -1
@@ -886,7 +881,7 @@ Node StringsPreprocess::reduce(Node t,
     Node bound =
         nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
     Node body = nm->mkNode(OR, bound.negate(), ri.eqNode(res));
-    Node rangeA = mkForallInternal(bvi, body);
+    Node rangeA = utils::mkForallInternal(bvi, body);
 
     // upper 65 ... 90
     // lower 97 ... 122
@@ -921,7 +916,7 @@ Node StringsPreprocess::reduce(Node t,
     Node bound =
         nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
     Node body = nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx));
-    Node rangeA = mkForallInternal(bvi, body);
+    Node rangeA = utils::mkForallInternal(bvi, body);
     // assert:
     //   len(r) = len(x) ^
     //   forall i. 0 <= i < len(r) =>
@@ -952,7 +947,7 @@ Node StringsPreprocess::reduce(Node t,
             kind::EQUAL,
             NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
             s));
-    retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
+    retNode = utils::mkForallInternal(b1v, body.negate()).negate();
   }
   else if (t.getKind() == kind::STRING_LEQ)
   {
@@ -982,8 +977,9 @@ Node StringsPreprocess::reduce(Node t,
     }
     conj.push_back(nm->mkNode(ITE, ite_ch));
 
-    Node conjn = nm->mkNode(
-        EXISTS, nm->mkNode(BOUND_VAR_LIST, k), nm->mkNode(AND, conj));
+    Node conjn = utils::mkForallInternal(nm->mkNode(BOUND_VAR_LIST, k),
+                                         nm->mkNode(AND, conj).negate())
+                     .negate();
     // Intuitively, the reduction says either x and y are equal, or they have
     // some (maximal) common prefix after which their characters at position k
     // are distinct, and the comparison of their code matches the return value
@@ -1095,31 +1091,6 @@ Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
   return ret;
 }
 
-Node StringsPreprocess::mkForallInternal(Node bvl, Node body)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  QInternalVarAttribute qiva;
-  Node qvar;
-  if (bvl.hasAttribute(qiva))
-  {
-    qvar = bvl.getAttribute(qiva);
-  }
-  else
-  {
-    SkolemManager* sm = nm->getSkolemManager();
-    qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
-    // this dummy variable marks that the quantified formula is internal
-    qvar.setAttribute(InternalQuantAttribute(), true);
-    // remember the dummy variable
-    bvl.setAttribute(qiva, qvar);
-  }
-  // make the internal attribute, and put it in a singleton list
-  Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
-  Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
-  // make the overall formula
-  return nm->mkNode(FORALL, bvl, body, ipl);
-}
-
 }  // namespace strings
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 7f0efe50f..01e6fa856 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -91,14 +91,6 @@ class StringsPreprocess {
    * visited stores a cache of previous results.
    */
   Node simplifyRec(Node t, std::vector<Node>& asserts);
-  /**
-   * Make internal quantified formula with bound variable list bvl and body.
-   * Internally, we get a node corresponding to marking a quantified formula as
-   * an "internal" one. This node is provided as the third argument of the
-   * FORALL returned by this method. This ensures that E-matching is not applied
-   * to the quantified formula.
-   */
-  static Node mkForallInternal(Node bvl, Node body);
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index cfe126ef3..27bf090ca 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -17,7 +17,10 @@
 
 #include <sstream>
 
+#include "expr/attribute.h"
+#include "expr/skolem_manager.h"
 #include "options/strings_options.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/strings_entail.h"
@@ -421,6 +424,40 @@ unsigned getLoopMinOccurrences(TNode node)
   return node.getOperator().getConst<RegExpLoop>().d_loopMinOcc;
 }
 
+/**
+ * Mapping to a dummy node for marking an attribute on internal quantified
+ * formulas. This ensures that reductions are deterministic.
+ */
+struct QInternalVarAttributeId
+{
+};
+typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
+
+Node mkForallInternal(Node bvl, Node body)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  QInternalVarAttribute qiva;
+  Node qvar;
+  if (bvl.hasAttribute(qiva))
+  {
+    qvar = bvl.getAttribute(qiva);
+  }
+  else
+  {
+    SkolemManager* sm = nm->getSkolemManager();
+    qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
+    // this dummy variable marks that the quantified formula is internal
+    qvar.setAttribute(InternalQuantAttribute(), true);
+    // remember the dummy variable
+    bvl.setAttribute(qiva, qvar);
+  }
+  // make the internal attribute, and put it in a singleton list
+  Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
+  Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
+  // make the overall formula
+  return nm->mkNode(FORALL, bvl, body, ipl);
+}
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index ec093031e..58162ac1b 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -216,6 +216,15 @@ unsigned getLoopMaxOccurrences(TNode node);
 /* Get the minimum occurrences of given regexp loop node. */
 unsigned getLoopMinOccurrences(TNode node);
 
+/**
+ * Make internal quantified formula with bound variable list bvl and body.
+ * Internally, we get a node corresponding to marking a quantified formula as
+ * an "internal" one. This node is provided as the third argument of the
+ * FORALL returned by this method. This ensures that E-matching is not applied
+ * to the quantified formula.
+ */
+Node mkForallInternal(Node bvl, Node body);
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory