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/unit/theory/CMakeLists.txt | |
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/unit/theory/CMakeLists.txt')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 963466b09..02ca5d8b5 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -1,3 +1,4 @@ +cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) |