From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 5 Sep 2018 14:49:59 +0000 (-0700)
Subject: Add regex grammar to rewriter verification tests (#2426)
X-Git-Tag: cvc5-1.0.0~4680
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1752aeb263a986bf437bb04029474b41987450d2;p=cvc5.git

Add regex grammar to rewriter verification tests (#2426)
---

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 39a7a4f4d..b8b047e6d 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1401,6 +1401,7 @@ REG1_TESTS = \
 	regress1/rr-verify/bool-crci.sy \
 	regress1/rr-verify/bv-term-32.sy \
 	regress1/rr-verify/bv-term.sy \
+	regress1/rr-verify/regex.sy \
 	regress1/rr-verify/string-term.sy \
 	regress1/sep/chain-int.smt2 \
 	regress1/sep/crash1220.smt2 \
diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress1/rr-verify/regex.sy
new file mode 100644
index 000000000..6c6da3dd2
--- /dev/null
+++ b/test/regress/regress1/rr-verify/regex.sy
@@ -0,0 +1,32 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic SLIA)
+
+(synth-fun f ((x String) (y String)) Bool (
+
+(Start Bool (
+  true
+  false
+  (= StartStr StartStr)
+  (str.in.re StartStr StartRe)
+))
+
+(StartRe RegLan (
+  re.allchar
+  (re.++ StartRe StartRe)
+  (re.union StartRe StartRe)
+  (re.* StartRe)
+  (str.to.re StartStr)
+))
+
+(StartStr String (
+  x y "A" "B" ""
+  (str.++ StartStr StartStr)
+))
+
+))
+
+(check-synth)