Improvements to rewriter for regexp, contains, indexof. Improvements and fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.

8 files changed, 122 insertions, 1 deletions

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 09dbdf08f..894e2546a 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -59,7 +59,14 @@ TESTS = \
   idof-triv.smt2 \
   chapman150408.smt2 \
   pierre150331.smt2 \
-  norn-360.smt2
+  norn-360.smt2 \
+  norn-simp-rew.smt2 \
+  norn-simp-rew-sat.smt2 \
+  idof-handg.smt2 \
+  idof-nconst-index.smt2 \
+  idof-neg-index.smt2 \
+  bug612.smt2 \
+  bug615.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/bug612.smt2 b/test/regress/regress0/strings/bug612.smt2
new file mode 100644
index 000000000..b627e2064
--- /dev/null
+++ b/test/regress/regress0/strings/bug612.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status unsat)
+
+(declare-fun s () String)
+
+(assert (not (str.contains s "x")))
+(assert (str.contains s "xy"))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/bug615.smt2 b/test/regress/regress0/strings/bug615.smt2
new file mode 100644
index 000000000..86cc592fb
--- /dev/null
+++ b/test/regress/regress0/strings/bug615.smt2
@@ -0,0 +1,26 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+(declare-fun s () String)
+;(assert (= s "</script><script>alert(1);</script><script>"))
+
+(declare-fun joined () String)
+(assert (= joined (str.++ "<script>console.log('" s "');</script>")))
+(assert (str.contains joined "<script>alert(1);</script>"))
+
+; (<script>[^<]*</script>)+
+(assert (str.in.re joined
+            (re.+ (re.++
+                    (str.to.re "<script>")
+                    (re.*
+                        (re.union
+                            (re.range " " ";")
+                            (re.range "=" "~")
+                        )
+                    )
+                    (str.to.re "</script>")
+            ))
+  ))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/idof-handg.smt2 b/test/regress/regress0/strings/idof-handg.smt2
new file mode 100644
index 000000000..40aff3168
--- /dev/null
+++ b/test/regress/regress0/strings/idof-handg.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun s () String)
+(assert (str.contains s "Hello and goodbye!"))
+(assert (> (str.indexof s "goodbye" 0) (str.indexof s "Hello" 0)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/idof-nconst-index.smt2 b/test/regress/regress0/strings/idof-nconst-index.smt2
new file mode 100644
index 000000000..eba492220
--- /dev/null
+++ b/test/regress/regress0/strings/idof-nconst-index.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun s () String)
+(assert (str.contains s "Hello and goodbye!"))
+(declare-fun x () Int)
+(assert (<= (str.len s) x))
+(assert (not (= (str.indexof s "goodbye" (- x 30)) (- 1))))
+(check-sat)
diff --git a/test/regress/regress0/strings/idof-neg-index.smt2 b/test/regress/regress0/strings/idof-neg-index.smt2
new file mode 100644
index 000000000..c24fcc00a
--- /dev/null
+++ b/test/regress/regress0/strings/idof-neg-index.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status unsat)
+(declare-fun s () String)
+(declare-fun x () Int)
+(assert (< x 0))
+(assert (>= (str.indexof s "goodbye" x) 0))
+(check-sat)
diff --git a/test/regress/regress0/strings/norn-simp-rew-sat.smt2 b/test/regress/regress0/strings/norn-simp-rew-sat.smt2
new file mode 100644
index 000000000..01a102bf9
--- /dev/null
+++ b/test/regress/regress0/strings/norn-simp-rew-sat.smt2
@@ -0,0 +1,25 @@
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
+(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_4 (re.* (str.to.re "b"))))
+(assert (str.in.re var_3 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_3 (re.* (str.to.re "a"))))
+(assert (<= 0  (str.len var_4)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
new file mode 100755
index 000000000..d0cd69cb0
--- /dev/null
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -0,0 +1,29 @@
+(set-logic QF_SLIA)

+(set-option :strings-exp true)

+(set-info :status unsat)

+

+(declare-fun var_0 () String)

+(declare-fun var_1 () String)

+(declare-fun var_2 () String)

+(declare-fun var_3 () String)

+(declare-fun var_4 () String)

+(declare-fun var_5 () String)

+(declare-fun var_6 () String)

+(declare-fun var_7 () String)

+(declare-fun var_8 () String)

+(declare-fun var_9 () String)

+(declare-fun var_10 () String)

+(declare-fun var_11 () String)

+(declare-fun var_12 () String)

+

+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))

+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a")))))))

+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b")))))))

+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a")))))

+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b"))))))

+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))

+(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))

+(assert (str.in.re var_8 (re.* (re.range "a" "u"))))

+(assert (str.in.re var_7 (re.* (re.range "a" "u"))))

+(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))

+(check-sat)
\ No newline at end of file