diff options
Diffstat (limited to 'test/regress/regress0/strings')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/fmf001.smt2 | 19 | ||||
-rw-r--r-- | test/regress/regress0/strings/fmf002.smt2 | 16 | ||||
-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/loop009.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/regexp001.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress0/strings/regexp002.smt2 | 19 | ||||
-rw-r--r-- | test/regress/regress0/strings/str006.smt2 | 14 |
10 files changed, 115 insertions, 7 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 9b9fdef7a..c98f37958 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -25,15 +25,22 @@ TESTS = \ str003.smt2 \ str004.smt2 \ str005.smt2 \ + str006.smt2 \ + fmf001.smt2 \ + fmf002.smt2 \ model001.smt2 \ substr001.smt2 \ + regexp001.smt2 \ + regexp002.smt2 \ loop001.smt2 \ loop002.smt2 \ loop003.smt2 \ loop004.smt2 \ loop005.smt2 \ loop006.smt2 \ - loop007.smt2 + loop007.smt2 \ + loop008.smt2 \ + loop009.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2 new file mode 100644 index 000000000..a8874b59f --- /dev/null +++ b/test/regress/regress0/strings/fmf001.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_S)
+(set-option :fmf-strings true)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (str.in.re x
+ (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+ ))
+
+(assert (str.in.re y
+ (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+ ))
+
+(assert (not (= x y)))
+(assert (= (str.len x) (str.len y)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2 new file mode 100644 index 000000000..14f50c710 --- /dev/null +++ b/test/regress/regress0/strings/fmf002.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_S)
+(set-option :fmf-strings true)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (str.in.re x
+ (re.+ (re.range "a" "c"))
+ ))
+
+(assert (= x (str.++ y "c" z "b")))
+(assert (> (str.len z) 1))
+
+(check-sat)
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/loop009.smt2 b/test/regress/regress0/strings/loop009.smt2 new file mode 100644 index 000000000..41eab0f35 --- /dev/null +++ b/test/regress/regress0/strings/loop009.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+
+(assert (= (str.++ x "aa") (str.++ "aa" x)))
+(assert (= (str.len x) 7))
+
+(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)
diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2 new file mode 100644 index 000000000..e2a44a9ab --- /dev/null +++ b/test/regress/regress0/strings/regexp002.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (str.in.re x
+ (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+ ))
+
+(assert (str.in.re y
+ (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+ ))
+
+(assert (not (= x y)))
+(assert (= (str.len x) (str.len y)))
+(assert (= (str.len y) 3))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2 new file mode 100644 index 000000000..592ef6a7f --- /dev/null +++ b/test/regress/regress0/strings/str006.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+;plandowski p469 1
+(assert (= (str.++ x "ab" y) (str.++ y "ba" z)))
+(assert (= z (str.++ x y)))
+(assert (not (= (str.++ x "a") (str.++ "a" x))))
+
+(check-sat)
+
|