[CVC Parser] Add support for regular expressions (#3346)

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;