diff options
author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
---|---|---|
committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
commit | dea679ce032c130d210d54c2e5482f95db1ff04a (patch) | |
tree | 6c36f68150172b20717f7d504274ab0bf82791b0 /test/regress/regress0/strings | |
parent | d95fe7675e20eaee86b8e804469e6db83265a005 (diff) |
A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).
Diffstat (limited to 'test/regress/regress0/strings')
20 files changed, 288 insertions, 288 deletions
diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2 index 616189d96..2ecbcc993 100644 --- a/test/regress/regress0/strings/at001.smt2 +++ b/test/regress/regress0/strings/at001.smt2 @@ -1,12 +1,12 @@ -(set-logic QF_S)
-(set-info :status sat)
-
-(declare-fun x () String)
-(declare-fun i () Int)
-
-(assert (= (str.at x i) "b"))
-(assert (and (>= i 4) (< i (str.len x))))
-(assert (< (str.len x) 7))
-(assert (> (str.len x) 2))
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun i () Int) + +(assert (= (str.at x i) "b")) +(assert (and (>= i 4) (< i (str.len x)))) +(assert (< (str.len x) 7)) +(assert (> (str.len x) 2)) + +(check-sat) diff --git a/test/regress/regress0/strings/bug001.smt2 b/test/regress/regress0/strings/bug001.smt2 index 49568329e..cdeebd20b 100644 --- a/test/regress/regress0/strings/bug001.smt2 +++ b/test/regress/regress0/strings/bug001.smt2 @@ -1,15 +1,15 @@ -(set-logic QF_S)
-(set-info :status sat)
-
-(declare-fun x () String)
-(declare-fun y () String)
-(declare-fun z () String)
-
-(assert (= "\x4a" x))
-(assert (= "\x6a" y))
-
-(assert (= "\x4A" z))
-
-(assert (= x z))
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +(assert (= "\x4a" x)) +(assert (= "\x6a" y)) + +(assert (= "\x4A" z)) + +(assert (= x z)) + +(check-sat) diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2 index 15d1ea5a2..f8a481e14 100644 --- a/test/regress/regress0/strings/bug002.smt2 +++ b/test/regress/regress0/strings/bug002.smt2 @@ -1,10 +1,10 @@ -(set-logic ASLIA)
-(set-info :smt-lib-version 2.0)
-(set-option :strings-exp true)
-(set-info :status sat)
-
-; regex = [\*-,\t\*-\|](.{6,}()?)+
-(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) ) ) )
-(assert (not (strinre "6O\1\127\n?")))
-
+(set-logic ASLIA) +(set-info :smt-lib-version 2.0) +(set-option :strings-exp true) +(set-info :status sat) + +; regex = [\*-,\t\*-\|](.{6,}()?)+ +(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) ) ) ) +(assert (not (strinre "6O\1\127\n?"))) + (check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/escchar.smt2 b/test/regress/regress0/strings/escchar.smt2 index aa2afb7e4..67a184ade 100644 --- a/test/regress/regress0/strings/escchar.smt2 +++ b/test/regress/regress0/strings/escchar.smt2 @@ -1,12 +1,12 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-info :smt-lib-version 2.0)
-
-(declare-fun x () String)
-(declare-const I Int)
-
-(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\\"\t\a\b"))
-(assert (= I (str.len x)))
-
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) +(set-info :smt-lib-version 2.0) + +(declare-fun x () String) +(declare-const I Int) + +(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\\"\t\a\b")) +(assert (= I (str.len x))) + + +(check-sat) diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2 index f48995344..af93a7ae5 100644 --- a/test/regress/regress0/strings/escchar_25.smt2 +++ b/test/regress/regress0/strings/escchar_25.smt2 @@ -1,12 +1,12 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-info :smt-lib-version 2.5)
-
-(declare-fun x () String)
-(declare-const I Int)
-
-(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b"))
-(assert (= I (str.len x)))
-
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) +(set-info :smt-lib-version 2.5) + +(declare-fun x () String) +(declare-const I Int) + +(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b")) +(assert (= I (str.len x))) + + +(check-sat) diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2 index 05bbab586..6081c8e06 100644 --- a/test/regress/regress0/strings/fmf001.smt2 +++ b/test/regress/regress0/strings/fmf001.smt2 @@ -1,20 +1,20 @@ -(set-logic QF_S)
-(set-option :strings-exp true)
-(set-option :strings-fmf 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)
+(set-logic QF_S) +(set-option :strings-exp true) +(set-option :strings-fmf 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 index 1d41b1085..d52dae2d2 100644 --- a/test/regress/regress0/strings/fmf002.smt2 +++ b/test/regress/regress0/strings/fmf002.smt2 @@ -1,17 +1,17 @@ -(set-logic QF_S)
-(set-option :strings-exp true)
-(set-option :strings-fmf 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)
+(set-logic QF_S) +(set-option :strings-exp true) +(set-option :strings-fmf 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/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2 index ae61b5f5b..2889348c1 100644 --- a/test/regress/regress0/strings/leadingzero001.smt2 +++ b/test/regress/regress0/strings/leadingzero001.smt2 @@ -1,11 +1,11 @@ -(set-logic QF_S)
-(set-option :strings-exp true)
-(set-info :status sat)
-
-(declare-fun Y () String)
-
-(assert (= Y "0001"))
-;(assert (= (str.to.int Y) (- 1)))
-(assert (= (str.to.int Y) 1))
-
-(check-sat)
+(set-logic QF_S) +(set-option :strings-exp true) +(set-info :status sat) + +(declare-fun Y () String) + +(assert (= Y "0001")) +;(assert (= (str.to.int Y) (- 1))) +(assert (= (str.to.int Y) 1)) + +(check-sat) diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2 index 113577e48..f84ba442b 100644 --- a/test/regress/regress0/strings/loop008.smt2 +++ b/test/regress/regress0/strings/loop008.smt2 @@ -1,10 +1,10 @@ -(set-logic QF_S)
-(set-option :strings-exp true)
-(set-info :status sat)
-
-(declare-fun x () String)
-
-(assert (= (str.++ x "ab") (str.++ "ba" x)))
-(assert (> (str.len x) 5))
-
-(check-sat)
+(set-logic QF_S) +(set-option :strings-exp true) +(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 index 9ccc6de6e..30fc6cebc 100644 --- a/test/regress/regress0/strings/loop009.smt2 +++ b/test/regress/regress0/strings/loop009.smt2 @@ -1,10 +1,10 @@ -(set-logic QF_S)
-(set-option :strings-exp true)
-(set-info :status sat)
-
-(declare-fun x () String)
-
-(assert (= (str.++ x "aa") (str.++ "aa" x)))
-(assert (= (str.len x) 7))
-
-(check-sat)
+(set-logic QF_S) +(set-option :strings-exp true) +(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 index 6a2044ea8..62c142d1d 100644 --- a/test/regress/regress0/strings/regexp001.smt2 +++ b/test/regress/regress0/strings/regexp001.smt2 @@ -1,13 +1,13 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-option :strings-exp true)
-
-(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)
+(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(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 index 8c29ccb38..a8bd2187a 100644 --- a/test/regress/regress0/strings/regexp002.smt2 +++ b/test/regress/regress0/strings/regexp002.smt2 @@ -1,24 +1,24 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-option :strings-exp true)
-; this option requires user to check whether the constraint is in the fragment
-; currently we do not provide only positive membership constraint checking
-; if users use this option but the constraint is not in this fragment, the result will fail
-(set-option :strings-inm true)
-
-(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)
+(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) +; this option requires user to check whether the constraint is in the fragment +; currently we do not provide only positive membership constraint checking +; if users use this option but the constraint is not in this fragment, the result will fail +(set-option :strings-inm true) + +(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/regexp003.smt2 b/test/regress/regress0/strings/regexp003.smt2 index 601689958..7696838fe 100644 --- a/test/regress/regress0/strings/regexp003.smt2 +++ b/test/regress/regress0/strings/regexp003.smt2 @@ -1,13 +1,13 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-option :strings-exp true)
-
-(declare-const s String)
-
-(assert (str.in.re s (re.inter
- (re.++ (str.to.re "a") (re.* (str.to.re "b"))
- (re.inter (str.to.re "c") (re.* (str.to.re "c"))))
- (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))
- )))
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-const s String) + +(assert (str.in.re s (re.inter + (re.++ (str.to.re "a") (re.* (str.to.re "b")) + (re.inter (str.to.re "c") (re.* (str.to.re "c")))) + (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c"))) + ))) + +(check-sat) diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2 index 39b2b76b1..9915504ae 100644 --- a/test/regress/regress0/strings/reloop.smt2 +++ b/test/regress/regress0/strings/reloop.smt2 @@ -1,18 +1,18 @@ -(set-logic QF_S)
-(set-option :strings-exp true)
-(set-info :status sat)
-
-(declare-fun x () String)
-(declare-fun y () String)
-(declare-fun z () String)
-(declare-fun w () String)
-
-(assert (str.in.re x (re.loop (str.to.re "a") 5)))
-(assert (str.in.re y (re.loop (str.to.re "b") 2 5)))
-(assert (str.in.re z (re.loop (str.to.re "c") 5)))
-(assert (> (str.len z) 7))
-(assert (str.in.re w (re.loop (str.to.re "b") 2 7)))
-(assert (> (str.len w) 2))
-(assert (< (str.len w) 5))
-
-(check-sat)
+(set-logic QF_S) +(set-option :strings-exp true) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun w () String) + +(assert (str.in.re x (re.loop (str.to.re "a") 5))) +(assert (str.in.re y (re.loop (str.to.re "b") 2 5))) +(assert (str.in.re z (re.loop (str.to.re "c") 5))) +(assert (> (str.len z) 7)) +(assert (str.in.re w (re.loop (str.to.re "b") 2 7))) +(assert (> (str.len w) 2)) +(assert (< (str.len w) 5)) + +(check-sat) diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2 index 592ef6a7f..2bdf9b1b5 100644 --- a/test/regress/regress0/strings/str006.smt2 +++ b/test/regress/regress0/strings/str006.smt2 @@ -1,14 +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)
-
+(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) + diff --git a/test/regress/regress0/strings/str007.smt2 b/test/regress/regress0/strings/str007.smt2 index 0ca2ec4c3..a7173701a 100644 --- a/test/regress/regress0/strings/str007.smt2 +++ b/test/regress/regress0/strings/str007.smt2 @@ -1,13 +1,13 @@ -(set-logic QF_S)
-(set-info :status unsat)
-
-(declare-fun x () String)
-(declare-fun y () String)
-
-
-(assert (or (= x y) (= x y)))
-
-(assert (= (str.++ x "ba") (str.++ "ab" x)))
-(assert (= (str.++ y "ab") (str.++ "ab" y)))
-
-(check-sat)
+(set-logic QF_S) +(set-info :status unsat) + +(declare-fun x () String) +(declare-fun y () String) + + +(assert (or (= x y) (= x y))) + +(assert (= (str.++ x "ba") (str.++ "ab" x))) +(assert (= (str.++ y "ab") (str.++ "ab" y))) + +(check-sat) diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 index bdfa33afb..78f3ffee7 100644 --- a/test/regress/regress0/strings/substr001.smt2 +++ b/test/regress/regress0/strings/substr001.smt2 @@ -1,16 +1,16 @@ -(set-logic QF_S)
-(set-info :status sat)
-
-(declare-fun x () String)
-(declare-fun i1 () Int)
-(declare-fun i2 () Int)
-(declare-fun i3 () Int)
-(declare-fun i4 () Int)
-
-(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x))))
-(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x))))
-(assert (= "efg" (str.substr x i1 i2) ) )
-(assert (= "bef" (str.substr x i3 i4) ) )
-(assert (> (str.len x) 5))
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun i1 () Int) +(declare-fun i2 () Int) +(declare-fun i3 () Int) +(declare-fun i4 () Int) + +(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x)))) +(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x)))) +(assert (= "efg" (str.substr x i1 i2) ) ) +(assert (= "bef" (str.substr x i3 i4) ) ) +(assert (> (str.len x) 5)) + +(check-sat) diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2 index ca93b00e5..77eabcccc 100644 --- a/test/regress/regress0/strings/type001.smt2 +++ b/test/regress/regress0/strings/type001.smt2 @@ -1,21 +1,21 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-option :strings-exp true)
-
-(declare-fun x () String)
-(declare-fun y () String)
-(declare-fun i () Int)
-(declare-fun j () Int)
-(declare-fun z () String)
-
-;big num test
-(assert (= x (int.to.str 4785582390527685649)))
-;should be ""
-(assert (= y (int.to.str (- 9))))
-
-;big num
-(assert (= i (str.to.int "783914785582390527685649")))
-;should be -1
-(assert (= j (str.to.int "-783914785582390527685649")))
-
+(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun i () Int) +(declare-fun j () Int) +(declare-fun z () String) + +;big num test +(assert (= x (int.to.str 4785582390527685649))) +;should be "" +(assert (= y (int.to.str (- 9)))) + +;big num +(assert (= i (str.to.int "783914785582390527685649"))) +;should be -1 +(assert (= j (str.to.int "-783914785582390527685649"))) + (check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2 index cbad2226a..296057a76 100644 --- a/test/regress/regress0/strings/type002.smt2 +++ b/test/regress/regress0/strings/type002.smt2 @@ -1,18 +1,18 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-option :strings-exp true)
-
-(declare-fun x () String)
-(declare-fun y () String)
-(declare-fun z () String)
-(declare-fun i () Int)
-
-(assert (>= i 420))
-(assert (= x (u16.to.str i)))
-(assert (= x (str.++ y "0" z)))
-(assert (not (= y "")))
-(assert (not (= z "")))
-
-
-
+(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) +(declare-fun i () Int) + +(assert (>= i 420)) +(assert (= x (u16.to.str i))) +(assert (= x (str.++ y "0" z))) +(assert (not (= y ""))) +(assert (not (= z ""))) + + + (check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/type003.smt2 b/test/regress/regress0/strings/type003.smt2 index b8f0ac5ae..c2d4792cc 100644 --- a/test/regress/regress0/strings/type003.smt2 +++ b/test/regress/regress0/strings/type003.smt2 @@ -1,12 +1,12 @@ -(set-logic QF_S)
-(set-info :status sat)
-(set-option :strings-exp true)
-
-(declare-fun i () Int)
-(declare-fun s () String)
-
-(assert (< 67 (str.to.int s)))
-(assert (= (str.len s) 2))
-(assert (not (= s "68")))
-
-(check-sat)
+(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun i () Int) +(declare-fun s () String) + +(assert (< 67 (str.to.int s))) +(assert (= (str.len s) 2)) +(assert (not (= s "68"))) + +(check-sat) |