diff options
Diffstat (limited to 'test/regress/regress0/strings')
8 files changed, 34 insertions, 42 deletions
diff --git a/test/regress/regress0/strings/parser-syms.cvc b/test/regress/regress0/strings/parser-syms.cvc deleted file mode 100644 index 20c37cf52..000000000 --- a/test/regress/regress0/strings/parser-syms.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: sat - -x : STRING; -y : STRING; - -ASSERT CONCAT( REVERSE("abc"), "d") = x; -ASSERT CONCAT( TOLOWER("ABC"), TOUPPER("abc")) = y; - -CHECKSAT; diff --git a/test/regress/regress0/strings/parser-syms.cvc.smt2 b/test/regress/regress0/strings/parser-syms.cvc.smt2 new file mode 100644 index 000000000..b71360c2c --- /dev/null +++ b/test/regress/regress0/strings/parser-syms.cvc.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () String) +(declare-fun y () String) +(assert (= (str.++ (str.rev "abc") "d") x)) +(assert (= (str.++ (str.tolower "ABC") (str.toupper "abc")) y)) +(check-sat) diff --git a/test/regress/regress0/strings/regexp-native-simple.cvc b/test/regress/regress0/strings/regexp-native-simple.cvc deleted file mode 100644 index 49d6f3d64..000000000 --- a/test/regress/regress0/strings/regexp-native-simple.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: sat - -x : STRING; - -ASSERT x IS_IN RE_CONCAT(RE_OPT(RE_STAR(RE_UNION(RE_RANGE("i", "j"), RE_RANGE("k", "l")))), - RE_PLUS(STRING_TO_REGEXP("abc")), - RE_LOOP(STRING_TO_REGEXP("def"), 1, 2), - RE_SIGMA); -ASSERT NOT(x IS_IN RE_INTER(RE_STAR(RE_SIGMA), RE_EMPTY)); - -ASSERT x = "ikljabcabcdefe"; - -CHECKSAT; diff --git a/test/regress/regress0/strings/regexp-native-simple.cvc.smt2 b/test/regress/regress0/strings/regexp-native-simple.cvc.smt2 new file mode 100644 index 000000000..c1c0087af --- /dev/null +++ b/test/regress/regress0/strings/regexp-native-simple.cvc.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () String) +(assert (str.in_re x (re.++ (re.opt (re.* (re.union (re.range "i" "j") (re.range "k" "l")))) (re.+ (str.to_re "abc")) ((_ re.loop 1 2) (str.to_re "def")) re.allchar ))) +(assert (not (str.in_re x (re.inter (re.* re.allchar ) re.none )))) +(assert (= x "ikljabcabcdefe")) +(check-sat) diff --git a/test/regress/regress0/strings/strings-charat.cvc b/test/regress/regress0/strings/strings-charat.cvc deleted file mode 100644 index 76c686dbf..000000000 --- a/test/regress/regress0/strings/strings-charat.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% COMMAND-LINE: --strings-exp -% EXPECT: unsat - -x : STRING; -y : STRING; - -ASSERT x = CONCAT( "abcd", y ); -ASSERT CHARAT(x,0) = CHARAT(x,2); - -CHECKSAT; diff --git a/test/regress/regress0/strings/strings-charat.cvc.smt2 b/test/regress/regress0/strings/strings-charat.cvc.smt2 new file mode 100644 index 000000000..440172172 --- /dev/null +++ b/test/regress/regress0/strings/strings-charat.cvc.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () String) +(declare-fun y () String) +(assert (= x (str.++ "abcd" y))) +(assert (= (str.at x 0) (str.at x 2))) +(check-sat) diff --git a/test/regress/regress0/strings/strings-native-simple.cvc b/test/regress/regress0/strings/strings-native-simple.cvc deleted file mode 100644 index 568452e12..000000000 --- a/test/regress/regress0/strings/strings-native-simple.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat - -x : STRING; -y : STRING; - -ASSERT x = CONCAT( "abcd", y ); -ASSERT LENGTH( x ) >= 6; -ASSERT LENGTH( y ) < 5; - -CHECKSAT; diff --git a/test/regress/regress0/strings/strings-native-simple.cvc.smt2 b/test/regress/regress0/strings/strings-native-simple.cvc.smt2 new file mode 100644 index 000000000..d40e9db7e --- /dev/null +++ b/test/regress/regress0/strings/strings-native-simple.cvc.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () String) +(declare-fun y () String) +(assert (= x (str.++ "abcd" y))) +(assert (>= (str.len x) 6)) +(assert (< (str.len y) 5)) +(check-sat) |