diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-01 00:30:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 22:30:44 -0700 |
| commit | 936e9c442443799c866a65c6ca3fbdcd3ac9aab8 (patch) | |
| tree | b953269087d78261c6a5d81e4d32e4cce70d5f41 /test/regress | |
| parent | 6d43ef828f5cc84f05b2c52a1991f3fb8505db84 (diff) | |
Support char smt-lib syntax (#4188)
Towards support for the strings standard.
Adds support to (_ char #x ... ) syntax for characters.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/char-representations.smt2 | 22 | ||||
| -rw-r--r-- | test/regress/regress0/strings/unicode-esc.smt2 | 2 |
3 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b9835d919..87bea4583 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -918,6 +918,7 @@ set(regress_0_tests regress0/strings/bug002.smt2 regress0/strings/bug612.smt2 regress0/strings/bug613.smt2 + regress0/strings/char-representations.smt2 regress0/strings/code-eval.smt2 regress0/strings/code-perf.smt2 regress0/strings/code-sat-neg-one.smt2 diff --git a/test/regress/regress0/strings/char-representations.smt2 b/test/regress/regress0/strings/char-representations.smt2 new file mode 100644 index 000000000..aaf119ab4 --- /dev/null +++ b/test/regress/regress0/strings/char-representations.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic SLIA) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +(assert (= x (_ char #x0D4))) +(assert (= x "\u00d4")) + + +(assert (= y (_ char #x1))) +(assert (= y "\u0001")) + +(assert (= z (_ char #xAF))) +(assert (= z (_ char #x0af))) +(assert (= z "\u{af}")) +(assert (= z "\u00af")) + +(check-sat) diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2 index 01f5f30ab..02b313d4a 100644 --- a/test/regress/regress0/strings/unicode-esc.smt2 +++ b/test/regress/regress0/strings/unicode-esc.smt2 @@ -26,5 +26,7 @@ (assert (= (str.len "\u{E}") 1)) (assert (= (str.len "\u{44444}") 9)) (assert (= (str.len "\u") 2)) +(assert (= (str.len "\u001") 5)) +(assert (= (str.len "\u0001") 1)) (check-sat) |