diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/gen-esc-seq.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/model-code-point.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress0/strings/model-friendly.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/unicode-esc.smt2 | 30 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 6 |
6 files changed, 68 insertions, 3 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8fab16b44..8382e40fc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -922,6 +922,7 @@ set(regress_0_tests regress0/strings/escchar.smt2 regress0/strings/escchar_25.smt2 regress0/strings/from_code.smt2 + regress0/strings/gen-esc-seq.smt2 regress0/strings/hconst-092618.smt2 regress0/strings/idof-rewrites.smt2 regress0/strings/idof-sem.smt2 @@ -939,6 +940,8 @@ set(regress_0_tests regress0/strings/leadingzero001.smt2 regress0/strings/loop001.smt2 regress0/strings/model001.smt2 + regress0/strings/model-code-point.smt2 + regress0/strings/model-friendly.smt2 regress0/strings/ncontrib-rewrites.smt2 regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 @@ -967,6 +970,7 @@ set(regress_0_tests regress0/strings/tolower-rrs.smt2 regress0/strings/tolower-simple.smt2 regress0/strings/type001.smt2 + regress0/strings/unicode-esc.smt2 regress0/strings/unsound-0908.smt2 regress0/strings/unsound-repl-rewrite.smt2 regress0/sygus/General_plus10.sy diff --git a/test/regress/regress0/strings/gen-esc-seq.smt2 b/test/regress/regress0/strings/gen-esc-seq.smt2 new file mode 100644 index 000000000..59f66046f --- /dev/null +++ b/test/regress/regress0/strings/gen-esc-seq.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --produce-models --lang=smt2.6.1 +; EXPECT: sat +; EXPECT: ((x "\u{5c}u1000")) +(set-logic ALL) +(set-info :status sat) +(declare-const x String) +(assert (= x (str.++ "\u" "1000"))) +(check-sat) +(get-value (x)) diff --git a/test/regress/regress0/strings/model-code-point.smt2 b/test/regress/regress0/strings/model-code-point.smt2 new file mode 100644 index 000000000..1200ae704 --- /dev/null +++ b/test/regress/regress0/strings/model-code-point.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --lang=smt2.6.1 --produce-models +; EXPECT: sat +; EXPECT: ((x "\u{a}")) +; EXPECT: ((y "\u{7f}")) +(set-logic ALL) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(assert (= (str.to_code x) 10)) +(assert (= (str.to_code y) 127)) +(check-sat) +(get-value (x)) +(get-value (y)) diff --git a/test/regress/regress0/strings/model-friendly.smt2 b/test/regress/regress0/strings/model-friendly.smt2 new file mode 100644 index 000000000..985ffaa62 --- /dev/null +++ b/test/regress/regress0/strings/model-friendly.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --lang=smt2.6.1 --produce-models +; EXPECT: sat +; EXPECT: ((x "AAAAA")) +(set-logic ALL) +(set-info :status sat) +(declare-fun x () String) +(assert (= (str.len x) 5)) +(check-sat) +(get-value (x)) diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2 new file mode 100644 index 000000000..01f5f30ab --- /dev/null +++ b/test/regress/regress0/strings/unicode-esc.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --strings-exp --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) + +(assert (= "\u{14}" "\u0014")) +(assert (= "\u{00}" "\u{0}")) +(assert (= "\u0000" "\u{0}")) +(assert (= (str.len "\u1234") 1)) +(assert (= (str.len "\u{1}") 1)) +(assert (= (str.len "\u{99}") 1)) +(assert (= (str.len "\u{779}") 1)) +(assert (= (str.len "\u{0779}") 1)) +(assert (= (str.len "\u{01779}") 1)) +(assert (= (str.len "\u{001779}") 10)) +(assert (= (str.len "\u{0vv79}") 9)) +(assert (= (str.len "\u{11\u1234}") 7)) +(assert (= (str.len "\u12345") 2)) +(assert (= (str.len "\uu") 3)) +(assert (= (str.len "\u{123}\u{567}") 2)) +(assert (= (str.len "\u{0017") 7)) +(assert (= (str.len "\\u00178") 3)) +(assert (= (str.len "2\u{}") 5)) +(assert (= (str.len "\uaaaa") 1)) +(assert (= (str.len "\uAAAA") 1)) +(assert (= (str.len "\u{0AbC}") 1)) +(assert (= (str.len "\u{E}") 1)) +(assert (= (str.len "\u{44444}") 9)) +(assert (= (str.len "\u") 2)) + +(check-sat) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 27f5aca12..0eefde700 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -556,9 +556,9 @@ void SolverBlack::testMkString() TS_ASSERT_THROWS_NOTHING(d_solver->mkString("")); TS_ASSERT_THROWS_NOTHING(d_solver->mkString("asdfasdf")); TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf").toString(), - "\"asdf\\\\nasdf\""); - TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf", true).toString(), - "\"asdf\\nasdf\""); + "\"asdf\\u{5c}nasdf\""); + TS_ASSERT_EQUALS(d_solver->mkString("asdf\\u{005c}nasdf", true).toString(), + "\"asdf\\u{5c}nasdf\""); } void SolverBlack::testMkTerm() |