From 2cddf7e216d3d2015a42246ef7a76b75ccaf6462 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Jun 2021 01:11:28 -0500 Subject: [PATCH] Fix str.update reduction (#6696) Fixes the 2nd benchmark from #6653. --- src/theory/strings/theory_strings_preprocess.cpp | 6 ++++-- test/regress/CMakeLists.txt | 1 + .../regress/regress1/strings/issue6653-2-update-c-len.smt2 | 7 +++++++ 3 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/strings/issue6653-2-update-c-len.smt2 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) -- 2.30.2