diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 10:00:48 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-08 12:00:48 -0500 |
commit | 7aebe3a327f1075f1489384b7e4e2808250ae344 (patch) | |
tree | b8bc4b07bb230ff758e0c20ef48526860c8b1ab3 /test/regress/regress0 | |
parent | 09af96d09c4cb90c976fee700daba8af34bed1e4 (diff) |
[CVC Parser] Add support for regular expressions (#3346)
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/strings/regexp-native-simple.cvc | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/regexp-native-simple.cvc b/test/regress/regress0/strings/regexp-native-simple.cvc new file mode 100644 index 000000000..49d6f3d64 --- /dev/null +++ b/test/regress/regress0/strings/regexp-native-simple.cvc @@ -0,0 +1,13 @@ +% EXPECT: sat + +x : STRING; + +ASSERT x IS_IN RE_CONCAT(RE_OPT(RE_STAR(RE_UNION(RE_RANGE("i", "j"), RE_RANGE("k", "l")))), + RE_PLUS(STRING_TO_REGEXP("abc")), + RE_LOOP(STRING_TO_REGEXP("def"), 1, 2), + RE_SIGMA); +ASSERT NOT(x IS_IN RE_INTER(RE_STAR(RE_SIGMA), RE_EMPTY)); + +ASSERT x = "ikljabcabcdefe"; + +CHECKSAT; |