diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-27 15:42:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-27 22:42:10 +0000 |
commit | 29f0b8f378377ed836bddaaf88883d0b2eeb545d (patch) | |
tree | 5d9edb57c60ab8c8a07dab52f18b72dd441d4fdf /test | |
parent | 631032b15327c28c44b51490dceb434a38f3419a (diff) |
Fix `str.replace_re` and `str.replace_re_all` (#6615)
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
Diffstat (limited to 'test')
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) |