From 7aebe3a327f1075f1489384b7e4e2808250ae344 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 8 Oct 2019 10:00:48 -0700 Subject: [CVC Parser] Add support for regular expressions (#3346) --- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/regexp-native-simple.cvc | 13 +++++++++++++ 2 files changed, 14 insertions(+) create mode 100644 test/regress/regress0/strings/regexp-native-simple.cvc (limited to 'test/regress') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 194dbd663..4b7e9d7ce 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -869,6 +869,7 @@ set(regress_0_tests regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 regress0/strings/re.all.smt2 + regress0/strings/regexp-native-simple.cvc regress0/strings/regexp_inclusion.smt2 regress0/strings/regexp_inclusion_reduction.smt2 regress0/strings/repl-rewrites2.smt2 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; -- cgit v1.2.3