diff options
Diffstat (limited to 'test/regress')
12 files changed, 165 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 35d2553de..422acd048 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1116,6 +1116,7 @@ set(regress_0_tests regress0/strings/idof-sem.smt2 regress0/strings/ilc-like.smt2 regress0/strings/indexof-sym-simp.smt2 + regress0/strings/indexof_re.smt2 regress0/strings/is_digit_simple.smt2 regress0/strings/issue1189.smt2 regress0/strings/issue2958.smt2 @@ -2047,6 +2048,7 @@ set(regress_1_tests regress1/strings/cmu-substr-rw.smt2 regress1/strings/code-sequence.smt2 regress1/strings/complement-test.smt2 + regress1/strings/indexof_re_red.smt2 regress1/strings/crash-1019.smt2 regress1/strings/csp-prefix-exp-bug.smt2 regress1/strings/double-replace.smt2 @@ -2089,6 +2091,8 @@ set(regress_1_tests regress1/strings/issue5692-infer-proxy.smt2 regress1/strings/issue5940-skc-len-conc.smt2 regress1/strings/issue5940-2-skc-len-conc.smt2 + regress1/strings/issue6057-replace-re.smt2 + regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 regress1/strings/issue6072-inc-no-const-reg.smt2 regress1/strings/issue6075-repl-len-one-rr.smt2 regress1/strings/issue6132-non-unique-skolem.smt2 @@ -2096,12 +2100,15 @@ set(regress_1_tests regress1/strings/issue6191-replace-all.smt2 regress1/strings/issue6203-1-substr-ctn-strip.smt2 regress1/strings/issue6203-2-re-ccache.smt2 + regress1/strings/issue6203-6-replace-re.smt2 regress1/strings/issue6214-2-sym-re-inc.smt2 regress1/strings/issue6214-3-sym-re-inc.smt2 regress1/strings/issue6214-4-sym-re-inc.smt2 regress1/strings/issue6270.smt2 regress1/strings/issue6271-rnf.smt2 regress1/strings/issue6271-2-rnf.smt2 + regress1/strings/issue6337-replace-re-all.smt2 + regress1/strings/issue6337-replace-re.smt2 regress1/strings/issue6567-empty-re-range.smt2 regress1/strings/issue6604-2.smt2 regress1/strings/kaluza-fl.smt2 @@ -2441,6 +2448,8 @@ set(regress_2_tests regress2/strings/issue3203.smt2 regress2/strings/issue5381.smt2 regress2/strings/issue6483.smt2 + regress2/strings/issue6057-replace-re-all.smt2 + regress2/strings/issue6057-replace-re-all-simplified.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/range-perf.smt2 @@ -2532,6 +2541,7 @@ set(regress_3_tests regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 regress3/strings-any-term.sy regress3/strings/extf_d_perf.smt2 + regress3/strings/indexof_re_red.smt2 regress3/strings/norn-dis-0707-3.smt2 regress3/strings/replace_re_all.smt2 regress3/unbdd_inv_gen_ex7.sy diff --git a/test/regress/regress0/strings/indexof_re.smt2 b/test/regress/regress0/strings/indexof_re.smt2 new file mode 100644 index 000000000..72c5d7ee7 --- /dev/null +++ b/test/regress/regress0/strings/indexof_re.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-const x String) +(assert (or + (not (= (str.indexof_re "abc" re.allchar (- 1)) (- 1))) + (not (= (str.indexof_re "abc" re.allchar (- 2)) (- 1))) + (not (= (str.indexof_re "abc" re.allchar 5) (- 1))) + (not (= (str.indexof_re "abc" re.allchar 0) 0)) + (not (= (str.indexof_re "abc" re.allchar 1) 1)) + (not (= (str.indexof_re "abc" re.allchar 2) 2)) + (not (= (str.indexof_re "abc" re.allchar 3) (- 1))) + (not (= (str.indexof_re "abc" (re.++ re.allchar re.allchar) 2) (- 1))) + (not (= (str.indexof_re "abc" (re.union (str.to_re "") re.allchar) 3) 3)) + (not (= (str.indexof_re (str.++ "abc" x) (re.union (str.to_re "") re.allchar) 3) 3)) + (not (= (str.indexof_re "cbabc" (re.union (str.to_re "a") (str.to_re "bab")) 0) 1)) +)) +(set-info :status unsat) +(check-sat) diff --git a/test/regress/regress1/strings/indexof_re_red.smt2 b/test/regress/regress1/strings/indexof_re_red.smt2 new file mode 100644 index 000000000..f32a6723b --- /dev/null +++ b/test/regress/regress1/strings/indexof_re_red.smt2 @@ -0,0 +1,52 @@ +; COMMAND-LINE: --strings-exp --incremental +(set-logic QF_SLIA) +(declare-const x String) +(declare-const i Int) + +(push) +(assert (= i (str.indexof_re (str.++ x "abc") (re.++ re.allchar (str.to_re "b")) 0))) +(assert (= i (str.len x))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= i (str.indexof_re (str.++ x "abc") (re.++ re.allchar (str.to_re "b")) 0))) +(assert (= i (+ (str.len x) 1))) +(set-info :status unsat) +(check-sat) +(pop) + +(push) +(assert (= i (str.indexof_re x (re.++ re.all (str.to_re "a") re.all) 0))) +(assert (= i 0)) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= i (str.indexof_re x (re.++ re.all (str.to_re "a") re.all) 0))) +(assert (= i (- 1))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= 2 (str.indexof_re x (str.to_re "a") 1))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= i (str.indexof_re x (str.to_re "") 0))) +(assert (= i (str.len x))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= i (str.indexof_re x (re.comp (str.to_re "")) 0))) +(assert (= i (str.len x))) +(set-info :status unsat) +(check-sat) +(pop) diff --git a/test/regress/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 b/test/regress/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 new file mode 100644 index 000000000..c9d93d024 --- /dev/null +++ b/test/regress/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun a () String) +; A complicated way of saying a = "b" +(assert (str.in_re a (re.++ (re.* (re.opt (str.to_re a))) (str.to_re "b")))) +; Corresponds to replace_re_all("ab", a*b, "") contains "a" +(assert (str.contains (str.replace_re_all (str.++ "a" a) (re.++ (re.* (str.to_re "a")) (str.to_re "b")) "") "a")) +(set-info :status unsat) +(check-sat) diff --git a/test/regress/regress1/strings/issue6057-replace-re.smt2 b/test/regress/regress1/strings/issue6057-replace-re.smt2 new file mode 100644 index 000000000..192b244b4 --- /dev/null +++ b/test/regress/regress1/strings/issue6057-replace-re.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_SLIA) +(declare-fun a () String) +(assert (str.suffixof "a" a)) +(assert (str.in_re a (re.* (re.union (str.to_re (str.replace_re a (re.++ (re.* (str.to_re "a")) (str.to_re "ba")) "")) (str.to_re "b"))))) +(assert (str.in_re a (re.++ (re.* (str.to_re (ite (str.in_re a (re.* (str.to_re "b"))) "" "u"))) (re.* (str.to_re a))))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress1/strings/issue6203-6-replace-re.smt2 b/test/regress/regress1/strings/issue6203-6-replace-re.smt2 new file mode 100644 index 000000000..d5e6acd45 --- /dev/null +++ b/test/regress/regress1/strings/issue6203-6-replace-re.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun a () String) +(assert (not (str.in_re (str.replace_re a (re.++ (re.* (re.union (str.to_re "a") (str.to_re ""))) (str.to_re "b")) "") (str.to_re "")))) +(assert (ite (str.in_re a (re.diff (re.* (re.union (str.to_re "a") (str.to_re "b"))) (re.range "a" "u"))) + (str.in_re a (re.diff (re.* (re.union (str.to_re "a") (str.to_re "b"))) (re.range "a" "u"))) + (str.<= a "b"))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress1/strings/issue6337-replace-re-all.smt2 b/test/regress/regress1/strings/issue6337-replace-re-all.smt2 new file mode 100644 index 000000000..9ae168b63 --- /dev/null +++ b/test/regress/regress1/strings/issue6337-replace-re-all.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun str3 () String) +(declare-fun str8 () String) +(declare-fun str12 () String) +(declare-fun str14 () String) +(declare-fun str15 () String) +(assert (distinct str15 (str.++ str14 str3 str8 str14) (str.replace_re_all str12 (re.comp (str.to_re str15)) (str.++ str14 str3 str8 str14)) str12)) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress1/strings/issue6337-replace-re.smt2 b/test/regress/regress1/strings/issue6337-replace-re.smt2 new file mode 100644 index 000000000..78895b24e --- /dev/null +++ b/test/regress/regress1/strings/issue6337-replace-re.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun a () String) +(declare-fun b () String) +(assert + (str.in_re + (str.replace_re (str.++ a "zb") + (re.union (str.to_re "z") (str.to_re "a") + (re.++ (re.* (str.to_re a)) + (re.union (str.to_re "z") (str.to_re "a")))) b) + (re.opt (str.to_re "bb")))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress2/strings/issue6057-replace-re-all-simplified.smt2 b/test/regress/regress2/strings/issue6057-replace-re-all-simplified.smt2 new file mode 100644 index 000000000..83860ef86 --- /dev/null +++ b/test/regress/regress2/strings/issue6057-replace-re-all-simplified.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun literal_5 () String) +(assert (not (= + literal_5 + (str.replace_re_all + literal_5 + (re.++ (re.* re.allchar) (str.to_re "\u{5c}\u{3c}\u{53}\u{43}\u{52}\u{49}\u{50}\u{54}") (re.* re.allchar)) + literal_5)))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress2/strings/issue6057-replace-re-all.smt2 b/test/regress/regress2/strings/issue6057-replace-re-all.smt2 new file mode 100644 index 000000000..9819b75dd --- /dev/null +++ b/test/regress/regress2/strings/issue6057-replace-re-all.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-fun literal_0 () String) +(assert (and (str.<= (str.++ literal_0 "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}") +(str.replace_re_all (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0) (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0))) +(str.<= (str.++ literal_0 "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}") (str.replace_re_all (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0) (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) (str.replace_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}" (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\u{65}\u{76}\u{69}\u{6c}") (re.* re.allchar))) literal_0))))) +(assert (not (str.<= "\u{2f}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2f}\u{74}\u{79}\u{70}\u{65}\u{2f}\u{6e}\u{75}\u{6d}\u{65}\u{72}\u{69}\u{63}\u{61}\u{6c}\u{2f}\u{65}\u{64}\u{69}\u{74}\u{71}\u{75}\u{65}\u{73}\u{74}\u{69}\u{6f}\u{6e}\u{2e}\u{68}\u{74}\u{6d}\u{6c}" "\u{2f}\u{65}\u{76}\u{69}\u{6c}"))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress2/strings/replace_re.smt2 b/test/regress/regress2/strings/replace_re.smt2 index 1f9b2a2ee..a58314150 100644 --- a/test/regress/regress2/strings/replace_re.smt2 +++ b/test/regress/regress2/strings/replace_re.smt2 @@ -40,3 +40,11 @@ (set-info :status unsat) (check-sat) (pop) + +(push) +(assert (= "FOO" (str.replace_re x (re.union (str.to_re "A") (str.to_re "ABC")) "FOO"))) +(assert (not (= x "FOO"))) +(assert (> (str.len x) 1)) +(set-info :status unsat) +(check-sat) +(pop) diff --git a/test/regress/regress3/strings/indexof_re_red.smt2 b/test/regress/regress3/strings/indexof_re_red.smt2 new file mode 100644 index 000000000..0e115cfd3 --- /dev/null +++ b/test/regress/regress3/strings/indexof_re_red.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-const x String) +(declare-const i Int) + +(assert (= i (str.indexof_re x (re.++ re.all (str.to_re "a")) 0))) +(assert (not (or (= i 0) (= i (- 1))))) +(set-info :status unsat) +(check-sat) |