Adds regular expression support, it is actually CFL because of variables.

5 files changed, 33 insertions, 7 deletions

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)