diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-01-15 23:15:27 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-15 21:15:27 -0800 |
| commit | 534a9b73dae2c0a3b6040f6a51f824ca69850c4b (patch) | |
| tree | 972b5b80d446a5ccd2629357bec37c7c52dbcfc7 | |
| parent | 3018455b424fc61e140be665a813cb6a8fac6320 (diff) | |
Fix constant contains ITOS rewrite (#2799)
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/itos-entail.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/strings/rewrites-v2.smt2 | 6 |
4 files changed, 16 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 57a99532e..b4c80e55b 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -3234,7 +3234,7 @@ bool TheoryStringsRewriter::canConstantContainConcat( Node c, Node n, int& first pos = new_pos + s.size(); } } - else if (n[i].getKind() == kind::STRING_ITOS) + else if (n[i].getKind() == kind::STRING_ITOS && checkEntailArith(n[i][0])) { // find the first occurrence of a digit starting at pos while (pos < tvec.size() && !String::isDigit(tvec[pos])) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index dbefe3af2..15dbf0df8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -822,6 +822,7 @@ set(regress_0_tests regress0/strings/ilc-like.smt2 regress0/strings/indexof-sym-simp.smt2 regress0/strings/issue1189.smt2 + regress0/strings/itos-entail.smt2 regress0/strings/leadingzero001.smt2 regress0/strings/loop001.smt2 regress0/strings/model001.smt2 diff --git a/test/regress/regress0/strings/itos-entail.smt2 b/test/regress/regress0/strings/itos-entail.smt2 new file mode 100644 index 000000000..f9dcf4c77 --- /dev/null +++ b/test/regress/regress0/strings/itos-entail.smt2 @@ -0,0 +1,11 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(declare-fun x () Int) +(declare-fun y () String) +(declare-fun z () String) + +(assert (str.contains "ABCD" (str.++ y (int.to.str x) z))) + +(check-sat) diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2 index ce2f140ae..15954525f 100644 --- a/test/regress/regress0/strings/rewrites-v2.smt2 +++ b/test/regress/regress0/strings/rewrites-v2.smt2 @@ -5,12 +5,12 @@ (set-info :status unsat) (declare-fun x () String) (declare-fun y () String) -(declare-fun z () Int) +(declare-fun z () String) ; these should all rewrite to false (assert (or -(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str z) x "a" y (int.to.str (+ z 1)))) -(str.contains "abc23cd" (str.++ (int.to.str z) (int.to.str z) (int.to.str z))) +(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str (str.len z)) x "a" y (int.to.str (+ (str.len z) 1)))) +(str.contains "abc23cd" (str.++ (int.to.str (str.len z)) (int.to.str (str.len z)) (int.to.str (str.len z)))) (not (str.contains (str.++ x "ab" y) (str.++ "b" (str.substr y 0 4)))) (not (str.contains (str.++ x "ab" y) (str.++ (str.substr x 5 (str.len x)) "a"))) (str.contains (str.++ x y) (str.++ x "a" y)) |