From c388e89e5253aa6fbde7685fc53126872f578f0b Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 11 Oct 2013 16:54:22 -0500
Subject: Adds regular expression support, it is actually CFL because of
 variables.

---
 test/regress/regress0/strings/Makefile.am    |  4 +++-
 test/regress/regress0/strings/loop005.smt2   | 10 ++++++----
 test/regress/regress0/strings/loop007.smt2   |  5 +++--
 test/regress/regress0/strings/loop008.smt2   |  9 +++++++++
 test/regress/regress0/strings/regexp001.smt2 | 12 ++++++++++++
 5 files changed, 33 insertions(+), 7 deletions(-)
 create mode 100644 test/regress/regress0/strings/loop008.smt2
 create mode 100644 test/regress/regress0/strings/regexp001.smt2

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 9b9fdef7a..daa817c4f 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -27,13 +27,15 @@ TESTS =	\
   str005.smt2 \
   model001.smt2 \
   substr001.smt2 \
+  regexp001.smt2 \
   loop001.smt2 \
   loop002.smt2 \
   loop003.smt2 \
   loop004.smt2 \
   loop005.smt2 \
   loop006.smt2 \
-  loop007.smt2
+  loop007.smt2 \
+  loop008.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2
index 4401ef794..039409ea6 100644
--- a/test/regress/regress0/strings/loop005.smt2
+++ b/test/regress/regress0/strings/loop005.smt2
@@ -5,11 +5,13 @@
 (declare-fun y () String)
 (declare-fun z () String)
 (declare-fun w () String)
-(declare-fun w1 () String)
-(declare-fun w2 () String)
 
-(assert (= (str.++ x y z) (str.++ x z y)))
-(assert (= (str.++ x w z) (str.++ x z w)))
+;(assert (= (str.++ x y z) (str.++ x z y)))
+;(assert (= (str.++ x w z) (str.++ x z w)))
+
+(assert (= (str.++ y z) (str.++ z y)))
+(assert (= (str.++ w z) (str.++ z w)))
+
 (assert (not (= y w)))
 (assert (> (str.len z) 0))
 
diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2
index bea4037d1..b292de512 100644
--- a/test/regress/regress0/strings/loop007.smt2
+++ b/test/regress/regress0/strings/loop007.smt2
@@ -5,6 +5,7 @@
 (declare-fun y () String)
 
 (assert (= (str.++ x y "aa") (str.++ "aa" y x)))
-(assert (= (str.len x) 1))
+(assert (= (str.len x) (* 2 (str.len y))))
+(assert (> (str.len x) 0))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2
new file mode 100644
index 000000000..91ed8cdf0
--- /dev/null
+++ b/test/regress/regress0/strings/loop008.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+
+(assert (= (str.++ x "ab") (str.++ "ba" x)))
+(assert (> (str.len x) 5))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/regexp001.smt2 b/test/regress/regress0/strings/regexp001.smt2
new file mode 100644
index 000000000..41aefbd41
--- /dev/null
+++ b/test/regress/regress0/strings/regexp001.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+
+(assert (str.in.re x
+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+	))
+
+(assert (= (str.len x) 3))
+
+(check-sat)
-- 
cgit v1.2.3