Infer conflicts based on regular expression inclusion (#3234)
authorAndres Noetzli <noetzli@stanford.edu>
Fri, 30 Aug 2019 02:38:17 +0000 (19:38 -0700)
committerGitHub <noreply@github.com>
Fri, 30 Aug 2019 02:38:17 +0000 (19:38 -0700)
commit974fc1d23c2b6091c26cf316964c4c16c5e2733f
treeb8e4b597ffc46194ee37687a56248309a63235b1
parentcc7546ff0a4e418de9a21c03ef12b1d5e8801bb8
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>
12 files changed:
cmake/FindCxxTest.cmake
src/theory/strings/regexp_operation.cpp
src/theory/strings/regexp_operation.h
src/theory/strings/regexp_solver.cpp
src/theory/strings/regexp_solver.h
src/theory/strings/theory_strings_utils.cpp
src/theory/strings/theory_strings_utils.h
test/regress/CMakeLists.txt
test/regress/regress0/strings/regexp_inclusion.smt2 [new file with mode: 0644]
test/regress/regress0/strings/regexp_inclusion_reduction.smt2 [new file with mode: 0644]
test/unit/theory/CMakeLists.txt
test/unit/theory/regexp_operation_black.h [new file with mode: 0644]