diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-08 01:11:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-07 23:11:28 -0700 |
| commit | 2cddf7e216d3d2015a42246ef7a76b75ccaf6462 (patch) | |
| tree | 3cc8b7189be241c0999e73f3f05dec593001e800 | |
| parent | 7e9e71c7bd2bcbdcb2cef0d8f99bf34082bf4081 (diff) | |
Fix str.update reduction (#6696)
Fixes the 2nd benchmark from #6653.
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 6 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6653-2-update-c-len.smt2 | 7 |
3 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 152a3e180..b0d538064 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -163,8 +163,9 @@ Node StringsPreprocess::reduce(Node t, Node a2 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, sk3, sk2)); // length of first skolem is second argument Node a3 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); + Node a4 = nm->mkNode(STRING_LENGTH, rs).eqNode(nm->mkNode(STRING_LENGTH, sk3)); - Node b1 = nm->mkNode(AND, a1, a2, a3); + Node b1 = nm->mkNode(AND, {a1, a2, a3, a4}); Node b2 = skt.eqNode(s); Node lemma = nm->mkNode(ITE, cond, b1, b2); @@ -172,7 +173,8 @@ Node StringsPreprocess::reduce(Node t, // IF n >=0 AND n < len( s ) // THEN: skt = sk1 ++ substr(r,0,len(s)-n) ++ sk2 AND // s = sk1 ++ sk3 ++ sk2 AND - // len( sk1 ) = n + // len( sk1 ) = n AND + // len( substr(r,0,len(s)-n) ) = len( sk3 ) // ELSE: skt = s // We use an optimization where r is used instead of substr(r,0,len(s)-n) // if r is a constant of length one. diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 207840516..d112bdf1d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2125,6 +2125,7 @@ set(regress_1_tests regress1/strings/issue6337-replace-re.smt2 regress1/strings/issue6567-empty-re-range.smt2 regress1/strings/issue6604-2.smt2 + regress1/strings/issue6653-2-update-c-len.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 b/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 new file mode 100644 index 000000000..88a89b725 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(set-option :check-unsat-cores true) +(declare-fun s () String) +(assert (not (= "A" (str.substr (str.update "AAAAAA" 1 s) 5 1)))) +(check-sat) |