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 | |
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')
-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 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 12 |
4 files changed, 37 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) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 9fd1b7789..7c9af1714 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -69,6 +69,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkRoundingMode(); void testMkSepNil(); void testMkString(); + void testMkChar(); void testMkTerm(); void testMkTermFromOp(); void testMkTrue(); @@ -560,6 +561,17 @@ void SolverBlack::testMkString() "\"asdf\\u{5c}nasdf\""); } +void SolverBlack::testMkChar() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->mkChar(std::string("0123"))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkChar("aA")); + TS_ASSERT_THROWS(d_solver->mkChar(nullptr), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkChar(""), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkChar("0g0"), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkChar("100000"), CVC4ApiException&); + TS_ASSERT_EQUALS(d_solver->mkChar("abc"), d_solver->mkChar("ABC")); +} + void SolverBlack::testMkTerm() { Sort bv32 = d_solver->mkBitVectorSort(32); |