From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Mar 2022 14:06:28 +0000 (-0500)
Subject: Fix lower vs upper bound issue for eager RE conflicts (#8482)
X-Git-Tag: cvc5-1.0.0~97
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a09b8344565f359560e796e11f8902bd4f59e5b2;p=cvc5.git

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 6de587a81..4b815b3f9 100644
--- 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 e8b2c28f2..5686a1aee 100644
--- 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 3e5946b7d..d36ab1d24 100644
--- 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 d4f6a2dad..606f37d44 100644
--- 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
index 000000000..e6e07c584
--- /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
index 000000000..d75a50fc9
--- /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)