diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-10 12:50:52 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-10 12:50:52 -0700 |
commit | 2da2646dd65e0458311a2dccfb04850c0b7d9e3c (patch) | |
tree | 00d31835b3ad0c00064ae2b43a2a59844f418dd0 /test/regress/regress2/strings | |
parent | 05c099890ae908e495ceaf26509b87896fd0ad54 (diff) |
Add support for str.replace_re/str.replace_re_all (#4594)
This commit adds support for the last remaining string operators from
the new SMT-LIB standard for the theory of strings. The commit adds the
kinds, type checking, reductions, and evaluation rewrites for
`str.replace_re` and `str.replace_re_all`.
Diffstat (limited to 'test/regress/regress2/strings')
-rw-r--r-- | test/regress/regress2/strings/replace_re.smt2 | 42 | ||||
-rw-r--r-- | test/regress/regress2/strings/replace_re_all.smt2 | 31 |
2 files changed, 73 insertions, 0 deletions
diff --git a/test/regress/regress2/strings/replace_re.smt2 b/test/regress/regress2/strings/replace_re.smt2 new file mode 100644 index 000000000..1f9b2a2ee --- /dev/null +++ b/test/regress/regress2/strings/replace_re.smt2 @@ -0,0 +1,42 @@ +; COMMAND-LINE: --strings-exp +(set-option :incremental true) +(set-logic SLIA) +(declare-const x String) + +(push) +(assert (= "AFOOE" (str.replace_re x (re.++ (str.to_re "B") re.allchar (str.to_re "C")) "FOO"))) +(assert (not (= x "AFOOE"))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= "FOOA" (str.replace_re x re.all "FOO"))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= "FOOA" (str.replace_re x (re.++ (str.to_re "A") re.all) "FOO"))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= "FOOA" (str.replace_re x (re.++ (str.to_re "A") re.all) "FOO"))) +(assert (> (str.len x) 2)) +(set-info :status unsat) +(check-sat) +(pop) + +(push) +(assert (= "FOOA" (str.replace_re "A" re.all "FOO"))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (not (= "A" (str.replace_re "A" re.none "FOO")))) +(set-info :status unsat) +(check-sat) +(pop) diff --git a/test/regress/regress2/strings/replace_re_all.smt2 b/test/regress/regress2/strings/replace_re_all.smt2 new file mode 100644 index 000000000..cf2b674c3 --- /dev/null +++ b/test/regress/regress2/strings/replace_re_all.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --strings-exp +(set-option :incremental true) +(set-logic SLIA) +(declare-const x String) +(declare-const y String) + +(push) +(assert (= x (str.replace_re_all "ZABCZACZADDC" (re.++ (str.to_re "A") re.all (str.to_re "C")) y))) +(assert (= x "ZFOOZFXOZFOO")) +(set-info :status unsat) +(check-sat) +(pop) + +(push) +(assert (= "ZFOOZFXOZFOO" (str.replace_re_all x (re.++ (str.to_re "A") re.all (str.to_re "C")) "FOO"))) +(assert (not (= x "ZFOOZFXOZFOO"))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= "ZFOOZZFOO" (str.replace_re_all (str.++ "ZACZ" x "ZADDC") (re.++ (str.to_re "A") re.all (str.to_re "C")) "FOO"))) +(set-info :status sat) +(check-sat) +(pop) + +(push) +(assert (= "ZFOOZZFOO" (str.replace_re_all (str.++ "ZACXZ" x "ZADDC") (re.++ (str.to_re "A") re.all (str.to_re "C")) "FOO"))) +(set-info :status unsat) +(check-sat) +(pop) |