diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2019-08-29 19:38:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-29 19:38:17 -0700 |
| commit | 974fc1d23c2b6091c26cf316964c4c16c5e2733f (patch) | |
| tree | b8e4b597ffc46194ee37687a56248309a63235b1 /test/regress/regress0/strings | |
| parent | cc7546ff0a4e418de9a21c03ef12b1d5e8801bb8 (diff) | |
Infer conflicts based on regular expression inclusion (#3234)
We have a conflict if we have `str.in.re(x, R1)` and `~str.in.re(x, R2)`
and `R2` includes `R1` because there is no possible value for `x` that
satisfies both memberships. This commit adds code to detect regular
expression inclusion for a small fragment of regular expressions: string
literals with single char (`re.allchar`) and multichar wildcards
(`re.*(re.allchar)`).
Signed-off-by: Andres Noetzli <anoetzli@amazon.com>
Diffstat (limited to 'test/regress/regress0/strings')
| -rw-r--r-- | test/regress/regress0/strings/regexp_inclusion.smt2 | 13 | ||||
| -rw-r--r-- | test/regress/regress0/strings/regexp_inclusion_reduction.smt2 | 14 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/regexp_inclusion.smt2 b/test/regress/regress0/strings/regexp_inclusion.smt2 new file mode 100644 index 000000000..c5c68a408 --- /dev/null +++ b/test/regress/regress0/strings/regexp_inclusion.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strings-exp --no-re-elim +(set-info :status unsat) +(set-logic ALL) +(declare-const actionName String) + +(assert +(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (str.to.re "foobar") (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar)))) + +(assert (not +(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (re.++ (str.to.re "foo") re.allchar (str.to.re "ar")) (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar))) +)) + +(check-sat) diff --git a/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 new file mode 100644 index 000000000..c10c287bb --- /dev/null +++ b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --strings-exp --no-re-elim +(set-info :status sat) +(set-logic QF_SLIA) +(declare-const x String) +(declare-const y String) + +(assert (str.in.re x (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar")))) +(assert (str.in.re x (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar")))) + +(assert (not (str.in.re y (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar"))))) +(assert (not (str.in.re y (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar"))))) +(assert (not (= y ""))) + +(check-sat) |