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.

13 files changed, 115 insertions, 73 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7ae07d196..ee3701d51 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -292,14 +292,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Trace("smt") << "turning on quantifier logic, for strings-exp"
                    << std::endl;
     }
-    // We require bounded quantifier handling.
-    if (!opts.quantifiers.fmfBoundWasSetByUser)
-    {
-      opts.quantifiers.fmfBound = true;
-      Trace("smt") << "turning on fmf-bound, for strings-exp" << std::endl;
-    }
     // Note we allow E-matching by default to support combinations of sequences
-    // and quantifiers.
+    // and quantifiers. We also do not enable fmfBound here, which would
+    // enable bounded integer instantiation for *all* quantifiers. Instead,
+    // the bounded integers module will always process internally generated
+    // quantifiers (those marked with InternalQuantAttribute).
   }
   // whether we must disable proofs
   bool disableProofs = false;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 5ecc33778..3fd478c31 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -317,6 +317,19 @@ void BoundedIntegers::checkOwnership(Node f)
 {
   //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
   Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
+  // determine if we should look at the quantified formula at all
+  if (!options::fmfBound())
+  {
+    // only applying it to internal quantifiers
+    QuantAttributes& qattr = d_qreg.getQuantAttributes();
+    if (!qattr.isInternal(f))
+    {
+      Trace("bound-int") << "...not internal, skip" << std::endl;
+      return;
+    }
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
 
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index f6b8f30f4..27ec187a9 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/quantifiers_modules.h"
 
 #include "options/quantifiers_options.h"
+#include "options/strings_options.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_registry.h"
 
@@ -74,14 +75,15 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
     d_synth_e.reset(new SynthEngine(qs, qim, qr, tr));
     modules.push_back(d_synth_e.get());
   }
-  // finite model finding
-  if (options::fmfBound())
+  // bounded integer instantiation is used when the user requests it via
+  // fmfBound, or if strings are enabled.
+  if (options::fmfBound() || options::stringExp())
   {
     d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
     modules.push_back(d_bint.get());
   }
 
-  if (options::finiteModelFind() || options::fmfBound())
+  if (options::finiteModelFind() || options::fmfBound() || options::stringExp())
   {
     d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
     modules.push_back(d_model_engine.get());
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
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da67705f5..5312e70a3 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2198,6 +2198,7 @@ set(regress_1_tests
   regress1/strings/rev-ex5.smt2
   regress1/strings/rew-020618.smt2
   regress1/strings/rew-check1.smt2
+  regress1/strings/seq-quant-infinite-branch.smt2
   regress1/strings/simple-re-consume.smt2
   regress1/strings/stoi-400million.smt2
   regress1/strings/stoi-solve.smt2
diff --git a/test/regress/regress1/fmf/bug651.smt2 b/test/regress/regress1/fmf/bug651.smt2
index d243e0ce7..956a55cd3 100644
--- a/test/regress/regress1/fmf/bug651.smt2
+++ b/test/regress/regress1/fmf/bug651.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models
+; COMMAND-LINE: --fmf-fun --no-check-models --fmf-bound
 ; EXPECT: sat
 (set-logic UFDTSLIA)
 (set-option :produce-models true)
diff --git a/test/regress/regress1/quantifiers/issue3537.smt2 b/test/regress/regress1/quantifiers/issue3537.smt2
index 7f0ab060f..442eb65ac 100644
--- a/test/regress/regress1/quantifiers/issue3537.smt2
+++ b/test/regress/regress1/quantifiers/issue3537.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --finite-model-find
+; COMMAND-LINE: --strings-exp --finite-model-find --fmf-bound
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((UNIT 0)) (((Unit))
diff --git a/test/regress/regress1/strings/seq-quant-infinite-branch.smt2 b/test/regress/regress1/strings/seq-quant-infinite-branch.smt2
new file mode 100644
index 000000000..9816301d4
--- /dev/null
+++ b/test/regress/regress1/strings/seq-quant-infinite-branch.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const x8 Bool)
+(set-option :strings-exp true)
+(declare-fun s () (Seq Int))
+(declare-fun x () Int)
+(declare-fun i () Int)
+(declare-fun i@ () Int)
+(assert (and (forall ((u Int)) (or (> 0 u) (>= u i) (distinct x (seq.nth s u))))
+             (or (and x8 (not x8))
+                 (and (= i@ (+ i 1))
+                      (distinct x (seq.nth s i))
+                      (exists ((u Int)) (and (<= 0 u)
+                                             (< u i@)
+                                             (= x (seq.nth s u))))
+                 )
+        )))
+(check-sat)