Fix lower vs upper bound issue for eager RE conflicts (#8482)

Fixes #8481.

diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp
index 6de587a810420728c1bcd140f26277d461142b08..4b815b3f9243d55beeb43e7da719f00536b092df 100644 (file)
--- a/src/theory/strings/eager_solver.cpp
+++ b/src/theory/strings/eager_solver.cpp
@@ -227,6 +227,9 @@ bool EagerSolver::addEndpointConst(EqcInfo* e, Node t, Node c, bool isSuf)
 
 bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
 {
+  Trace("strings-eager-aconf-debug")
+      << "addArithmeticBound " << t << ", isLower = " << isLower << "..."
+      << std::endl;
   Assert(e != nullptr);
   Assert(!t.isNull());
   Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
@@ -257,6 +260,9 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
     Assert(!prevob.isNull() && prevob.isConst()
            && prevob.getType().isRealOrInt());
     Rational prevobr = prevob.getConst<Rational>();
+    Trace("strings-eager-aconf-debug")
+        << "Previous opposite bound was " << prevobr << ", current bound is "
+        << br << ", isLower = " << isLower << std::endl;
     if (prevobr != br && (prevobr < br) == isLower)
     {
       // conflict
@@ -283,7 +289,7 @@ Node EagerSolver::getBoundForLength(Node t, bool isLower) const
 {
   if (t.getKind() == STRING_IN_REGEXP)
   {
-    return d_rent.getConstantBoundLengthForRegexp(t[1]);
+    return d_rent.getConstantBoundLengthForRegexp(t[1], isLower);
   }
   Assert(t.getKind() == STRING_LENGTH);
   // it is prohibitively expensive to convert to original form and rewrite,

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index e8b2c28f23bc4ae2b961ffdc46b28fd9ab91eb45..5686a1aee9e7581c62c19af9c7db17d5b835f333 100644 (file)
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -776,6 +776,9 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const
   {
     ret = d_zero;
   }
+  Trace("strings-rentail") << "getConstantBoundLengthForRegexp: " << n
+                           << ", isLower=" << isLower << " returns " << ret
+                           << std::endl;
   setConstantBoundCache(n, ret, isLower);
   return ret;
 }

diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h
index 3e5946b7d8358fc92494363bf081c7ff9fb2f0fb..d36ab1d24033bb23439636e1d0b1c33e642b660c 100644 (file)
--- a/src/theory/strings/regexp_entail.h
+++ b/src/theory/strings/regexp_entail.h
@@ -122,7 +122,7 @@ class RegExpEntail
    * regular expression n. Return null if a constant bound cannot be determined.
    * This method will always worst case return 0 as a lower bound.
    */
-  Node getConstantBoundLengthForRegexp(TNode n, bool isLower = true) const;
+  Node getConstantBoundLengthForRegexp(TNode n, bool isLower) const;
   /**
    * Returns true if we can show that the regular expression `r1` includes
    * the regular expression `r2` (i.e. `r1` matches a superset of sequences

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index d4f6a2dadf22f49dfa5b713c7d283dc1f23f1759..606f37d44f3332a116374cbc365ccf17abcdb72e 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1381,6 +1381,8 @@ set(regress_0_tests
   regress0/strings/issue7974-incomplete-neg-member.smt2
   regress0/strings/issue8295-star-union-char.smt2
   regress0/strings/issue8346-idof-max.smt2
+  regress0/strings/issue8481.smt2
+  regress0/strings/issue8481-2.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/cli/regress0/strings/issue8481-2.smt2 b/test/regress/cli/regress0/strings/issue8481-2.smt2
new file mode 100644 (file)
index 0000000..e6e07c5
--- /dev/null
+++ b/test/regress/cli/regress0/strings/issue8481-2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-eager-len-re
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun v () String)
+(assert (str.in_re (str.++ v v) (re.++ (str.to_re "a") (re.opt (str.to_re "a")))))
+(assert (str.in_re v (re.range "a" "u")))
+(check-sat)

diff --git a/test/regress/cli/regress0/strings/issue8481.smt2 b/test/regress/cli/regress0/strings/issue8481.smt2
new file mode 100644 (file)
index 0000000..d75a50f
--- /dev/null
+++ b/test/regress/cli/regress0/strings/issue8481.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-eager-len-re
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in_re (str.replace b a "") (re.++ (str.to_re "u") (re.union (str.to_re "b") (str.to_re "")))))
+(assert (= (str.to_int (str.++ a a)) 0))
+(check-sat)