From ae3a80b9d36e84b6dfa1cde5fdb3ac421cc88159 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 15 Sep 2022 23:44:09 +0200 Subject: [PATCH] improve unit test for allChar. --- .../java_smt/test/StringFormulaManagerTest.java | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index 07e1977027..6a0f946ae6 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -148,23 +148,24 @@ public void testRegexAllChar() throws SolverException, InterruptedException { public void testRegexAllCharUnicode() throws SolverException, InterruptedException { RegexFormula regexAllChar = smgr.allChar(); - if (solverUnderTest == Solvers.CVC4) { - // CVC4 does not support Unicode characters - assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isUnsatisfiable(); + // Single characters. + assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isSatisfiable(); + assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable(); - } else { + // Combining characters are not matched as one character. + assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable(); + assertThatFormula(smgr.in(smgr.makeString("\\n"), regexAllChar)).isUnsatisfiable(); + + if (solverUnderTest != Solvers.CVC4) { + // CVC4 does not support Unicode characters. // Z3 and other solvers support Unicode characters in the theory of strings. - assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isSatisfiable(); - assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable(); assertThatFormula( smgr.in( smgr.makeVariable("x"), smgr.intersection(smgr.range('a', 'Δ'), regexAllChar))) .isSatisfiable(); // Combining characters are not matched as one character. - assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable(); // Non-ascii non-printable characters should use the codepoint representation assertThatFormula(smgr.in(smgr.makeString("Δ"), regexAllChar)).isUnsatisfiable(); - assertThatFormula(smgr.in(smgr.makeString("\\n"), regexAllChar)).isUnsatisfiable(); } }