diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/array_card.smt2 | 18 | ||||
| -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 |
12 files changed, 135 insertions, 8 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 601d65799..bfbc851ef 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -19,6 +19,7 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + array_card.smt2 \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ @@ -29,7 +30,7 @@ TESTS = \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 + bug0909.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/array_card.smt2 b/test/regress/regress0/fmf/array_card.smt2 new file mode 100644 index 000000000..9ee00d13a --- /dev/null +++ b/test/regress/regress0/fmf/array_card.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic AUFLIA) +(set-option :produce-models true) +(declare-sort U 0) +(declare-fun f () (Array U U)) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) + +(assert (distinct a b c)) + +(assert (distinct (select f a) (select f b))) + +(assert (forall ((x U)) (or (= (select f x) c) (= (select f x) b)))) + +(check-sat) 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)
+
|