diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-11 16:54:22 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-11 16:54:22 -0500 |
commit | c388e89e5253aa6fbde7685fc53126872f578f0b (patch) | |
tree | 0ace860103f2ad2da266e1f639d170baac73b4da /test/regress/regress0/strings | |
parent | 7c190dcead07d797d475a07522c595f97c7ef2db (diff) |
Adds regular expression support, it is actually CFL because of variables.
Diffstat (limited to 'test/regress/regress0/strings')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop005.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop008.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/regexp001.smt2 | 12 |
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)
|