diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-06 13:26:03 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-06 13:26:03 +0200 |
commit | 6343fbb0c9b238aeb1addca6449f95a01071c1ac (patch) | |
tree | 60f872134b3697a88d639ffa5adf73c5db02c5d1 /test | |
parent | 645aaaa186269c26d96a60c8df3350a2de9b6acb (diff) |
More improvements to strings rewriter for regexps, contains, indexof, replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/idof-rewrites.smt2 | 13 | ||||
-rwxr-xr-x | test/regress/regress0/strings/kaluza-fl.smt2 | 97 | ||||
-rwxr-xr-x | test/regress/regress0/strings/norn-ab.smt2 | 25 |
4 files changed, 140 insertions, 4 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 894e2546a..a8a8e968f 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -62,11 +62,13 @@ TESTS = \ 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 + bug615.smt2 \ + kaluza-fl.smt2 \ + norn-ab.smt2 \ + idof-rewrites.smt2 FAILING_TESTS = @@ -74,8 +76,7 @@ EXTRA_DIST = $(TESTS) \ fmf001.smt2 \ type002.smt2 -# slow after changes on Nov 20 : artemis-0512-nonterm.smt2 -# slow after decision engine respects requirePhase: type003.smt2 loop007.smt2 +# somewhat slow after changes on Oct 6: idof-handg.smt2 # and make sure to distribute it EXTRA_DIST += diff --git a/test/regress/regress0/strings/idof-rewrites.smt2 b/test/regress/regress0/strings/idof-rewrites.smt2 new file mode 100644 index 000000000..f52f0c9f3 --- /dev/null +++ b/test/regress/regress0/strings/idof-rewrites.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) +(declare-fun s () String) +(declare-fun t () String) + +; all of these should rewrite to true +(assert (= (str.indexof (str.++ s "abc") "ab" 0) (str.indexof (str.++ s "ab") "ab" 0))) +(assert (= (str.indexof (str.++ s "abc" t "a") t 2) (str.indexof (str.++ s "abc" t "c") t 2))) +(assert (= (str.indexof (str.++ "ddd" s "abc") "ab" 2) (+ 1 (str.indexof (str.++ "ed" s "ab") "ab" 1)))) +(assert (= (str.indexof (str.++ "dd" s "dd") "ab" 0) (str.indexof (str.++ "dd" s "ee") "ab" 0))) +(assert (= (str.indexof (str.++ "dd" s "dabd") "ab" 1) (+ 2 (str.indexof (str.++ s "dab" t) "ab" 0)))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/kaluza-fl.smt2 b/test/regress/regress0/strings/kaluza-fl.smt2 new file mode 100755 index 000000000..ce3af9e74 --- /dev/null +++ b/test/regress/regress0/strings/kaluza-fl.smt2 @@ -0,0 +1,97 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun I0_15 () Int)
+(declare-fun I0_18 () Int)
+(declare-fun I0_2 () Int)
+(declare-fun I0_4 () Int)
+(declare-fun I0_6 () Int)
+(declare-fun PCTEMP_LHS_1 () Int)
+(declare-fun PCTEMP_LHS_2 () Int)
+(declare-fun PCTEMP_LHS_3 () Int)
+(declare-fun PCTEMP_LHS_4 () Int)
+(declare-fun PCTEMP_LHS_5 () Int)
+(declare-fun T0_15 () String)
+(declare-fun T0_18 () String)
+(declare-fun T0_2 () String)
+(declare-fun T0_4 () String)
+(declare-fun T0_6 () String)
+(declare-fun T1_15 () String)
+(declare-fun T1_18 () String)
+(declare-fun T1_2 () String)
+(declare-fun T1_4 () String)
+(declare-fun T1_6 () String)
+(declare-fun T2_15 () String)
+(declare-fun T2_18 () String)
+(declare-fun T2_2 () String)
+(declare-fun T2_4 () String)
+(declare-fun T2_6 () String)
+(declare-fun T3_15 () String)
+(declare-fun T3_18 () String)
+(declare-fun T3_2 () String)
+(declare-fun T3_4 () String)
+(declare-fun T3_6 () String)
+(declare-fun T4_15 () String)
+(declare-fun T4_18 () String)
+(declare-fun T4_2 () String)
+(declare-fun T4_4 () String)
+(declare-fun T4_6 () String)
+(declare-fun T5_15 () String)
+(declare-fun T5_18 () String)
+(declare-fun T5_2 () String)
+(declare-fun T5_4 () String)
+(declare-fun T5_6 () String)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun T_6 () Bool)
+(declare-fun T_7 () Bool)
+(declare-fun T_8 () Bool)
+(declare-fun T_9 () Bool)
+(declare-fun T_SELECT_1 () Bool)
+(declare-fun T_SELECT_2 () Bool)
+(declare-fun T_SELECT_3 () Bool)
+(declare-fun T_SELECT_4 () Bool)
+(declare-fun T_SELECT_5 () Bool)
+(declare-fun T_a () Bool)
+(declare-fun T_c () Bool)
+(declare-fun T_e () Bool)
+(declare-fun var_0xINPUT_12454 () String)
+
+(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))
+(assert (ite T_SELECT_1
+ (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))
+ (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))))
+(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))
+(assert (ite T_SELECT_2
+ (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))
+ (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1)))))
+(assert (ite T_SELECT_3
+ (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))
+ (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_4 (<= 0 PCTEMP_LHS_1)))
+(assert T_4)
+(assert (= T_5 (<= 0 PCTEMP_LHS_2)))
+(assert T_5)
+(assert (= T_6 (<= 0 PCTEMP_LHS_3)))
+(assert T_6)
+(assert (= T_7 (= "" var_0xINPUT_12454)))
+(assert (= T_8 (not T_7)))
+(assert T_8)
+(assert (= T_9 (= var_0xINPUT_12454 "")))
+(assert (= T_a (not T_9)))
+(assert T_a)
+(assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1)))))
+(assert (ite T_SELECT_4
+ (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))
+ (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_c (< (- 1) PCTEMP_LHS_4)))
+(assert T_c)
+(assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1)))))
+(assert (ite T_SELECT_5
+ (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";"))))
+ (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";"))))))
+(assert (= T_e (< PCTEMP_LHS_5 0)))
+(assert T_e)
+
+(check-sat)
diff --git a/test/regress/regress0/strings/norn-ab.smt2 b/test/regress/regress0/strings/norn-ab.smt2 new file mode 100755 index 000000000..db7aac732 --- /dev/null +++ b/test/regress/regress0/strings/norn-ab.smt2 @@ -0,0 +1,25 @@ +(set-logic QF_SLIA)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(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 var_4 (re.++ (str.to.re "a") (re.* (str.to.re "b")))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
+(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
+(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
+(assert (and (<= 0 (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
+(check-sat)
\ No newline at end of file |