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.

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