diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-21 13:36:01 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-21 11:36:00 -0800 |
commit | 18eb247c3f14761dc0e1981d4faf11833f069b9d (patch) | |
tree | d29f8b299a61509d9ffeb9db51137371135731c8 /test | |
parent | be7ed89f137f4d0d64cf66ec40880370fbff2d4d (diff) |
Simple changes towards unicode string standard (#3791)
This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
The next steps will be to address the more invasive changes required to support the standard.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/code-eval.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/strings/code-perf.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/code-sat-neg-one.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/re-syntax.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/replaceall-eval.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/strings/std2.6.1.smt2 | 4 |
7 files changed, 29 insertions, 5 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 159f87037..d61203ac2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -884,6 +884,7 @@ set(regress_0_tests regress0/strings/bug002.smt2 regress0/strings/bug612.smt2 regress0/strings/bug613.smt2 + regress0/strings/code-eval.smt2 regress0/strings/code-perf.smt2 regress0/strings/code-sat-neg-one.smt2 regress0/strings/escchar.smt2 @@ -907,6 +908,7 @@ set(regress_0_tests regress0/strings/norn-simp-rew.smt2 regress0/strings/parser-syms.cvc regress0/strings/re.all.smt2 + regress0/strings/re-syntax.smt2 regress0/strings/regexp-native-simple.cvc regress0/strings/regexp_inclusion.smt2 regress0/strings/regexp_inclusion_reduction.smt2 diff --git a/test/regress/regress0/strings/code-eval.smt2 b/test/regress/regress0/strings/code-eval.smt2 new file mode 100644 index 000000000..faa5c174c --- /dev/null +++ b/test/regress/regress0/strings/code-eval.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(assert (< (str.to_code "A") (str.to_code "Z"))) +(assert (= (- 1) (str.to_code "AAA"))) +(assert (= (- 1) (str.to_code ""))) + +(check-sat) diff --git a/test/regress/regress0/strings/code-perf.smt2 b/test/regress/regress0/strings/code-perf.smt2 index 39cab48ce..4d7e22bd3 100644 --- a/test/regress/regress0/strings/code-perf.smt2 +++ b/test/regress/regress0/strings/code-perf.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: sat +(set-info :smt-lib-version 2.5) (set-logic QF_SLIA) (declare-const x0 String) (declare-const x1 String) diff --git a/test/regress/regress0/strings/code-sat-neg-one.smt2 b/test/regress/regress0/strings/code-sat-neg-one.smt2 index c69276a4f..403319d02 100644 --- a/test/regress/regress0/strings/code-sat-neg-one.smt2 +++ b/test/regress/regress0/strings/code-sat-neg-one.smt2 @@ -1,3 +1,4 @@ +(set-info :smt-lib-version 2.5) (set-logic QF_SLIA) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/re-syntax.smt2 b/test/regress/regress0/strings/re-syntax.smt2 new file mode 100644 index 000000000..4c25a65a4 --- /dev/null +++ b/test/regress/regress0/strings/re-syntax.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) + +(assert (or (str.in_re x re.none) (not (str.in_re x re.all)))) + +(check-sat) diff --git a/test/regress/regress0/strings/replaceall-eval.smt2 b/test/regress/regress0/strings/replaceall-eval.smt2 index 924515901..c118a7dc4 100644 --- a/test/regress/regress0/strings/replaceall-eval.smt2 +++ b/test/regress/regress0/strings/replaceall-eval.smt2 @@ -1,10 +1,11 @@ -(set-info :smt-lib-version 2.5) +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) -(assert (= x (str.replaceall "AABAABBC" "B" "def"))) -(assert (= y (str.replaceall "AABAABBC" "AB" "BA"))) +(assert (= x (str.replace_all "AABAABBC" "B" "def"))) +(assert (= y (str.replace_all "AABAABBC" "AB" "BA"))) (check-sat) diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2 index 3302a29e5..d30cfc83c 100644 --- a/test/regress/regress0/strings/std2.6.1.smt2 +++ b/test/regress/regress0/strings/std2.6.1.smt2 @@ -3,7 +3,7 @@ (set-logic QF_UFSLIA) (set-info :status sat) (declare-fun x () String) -(assert (str.in-re x (str.to-re "A"))) +(assert (str.in_re x (str.to_re "A"))) (declare-fun y () Int) -(assert (= (str.to-int (str.from-int y)) y)) +(assert (= (str.to_int (str.from_int y)) y)) (check-sat) |