diff options
Diffstat (limited to 'test/regress/regress1')
6 files changed, 100 insertions, 0 deletions
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) |