From a09b8344565f359560e796e11f8902bd4f59e5b2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Mar 2022 09:06:28 -0500 Subject: [PATCH] Fix lower vs upper bound issue for eager RE conflicts (#8482) Fixes #8481. --- src/theory/strings/eager_solver.cpp | 8 +++++++- src/theory/strings/regexp_entail.cpp | 3 +++ src/theory/strings/regexp_entail.h | 2 +- test/regress/cli/CMakeLists.txt | 2 ++ test/regress/cli/regress0/strings/issue8481-2.smt2 | 7 +++++++ test/regress/cli/regress0/strings/issue8481.smt2 | 8 ++++++++ 6 files changed, 28 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/strings/issue8481-2.smt2 create mode 100644 test/regress/cli/regress0/strings/issue8481.smt2 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(); + 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) -- 2.30.2