summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-04-01 00:30:44 -0500
committerGitHub <noreply@github.com>2020-03-31 22:30:44 -0700
commit936e9c442443799c866a65c6ca3fbdcd3ac9aab8 (patch)
treeb953269087d78261c6a5d81e4d32e4cce70d5f41 /test
parent6d43ef828f5cc84f05b2c52a1991f3fb8505db84 (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.txt1
-rw-r--r--test/regress/regress0/strings/char-representations.smt222
-rw-r--r--test/regress/regress0/strings/unicode-esc.smt22
-rw-r--r--test/unit/api/solver_black.h12
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback