diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-05 23:14:16 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-05 23:14:16 -0600 |
| commit | d72fcccb19e43d0140b8a6ac954c2858dd3a239a (patch) | |
| tree | fb09b00709495c3c6fd2a26169269843e989a060 /test | |
| parent | bfeedc822f39875c7d54dac0a744a63c5dc838bd (diff) | |
Improve rewriting for string contains part 2 (#1300)
* Generalize component contains, some infrastructure.
* Length entailment, substr for component contains, int.to.str for constant can contain concat.
* Disable rewrite.
* Fix, reenable length entailment for contains.
* Clang format, minor.
* Comment
* Minor fixes and improvements for comments.
* Improvements
* Clang format
* Fixes
* Clang format
* Fix, improve.
* Format
* Fix assertion
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/rewrites-v2.smt2 | 20 |
2 files changed, 22 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index e27a1bfcd..cd3351c59 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -90,7 +90,8 @@ TESTS = \ bug799-min.smt2 \ strings-charat.cvc \ issue1105.smt2 \ - issue1189.smt2 + issue1189.smt2 \ + rewrites-v2.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2 new file mode 100644 index 000000000..7e285b51a --- /dev/null +++ b/test/regress/regress0/strings/rewrites-v2.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic SLIA) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () Int) + +; 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))) +(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)) +(str.contains (str.++ x y) (str.++ y x x y "a")) +) +) + +(check-sat) |