Skip to content

Commit 9cc096b

Browse files
Strings: Clean up the documentation
Strings in SMTLIB may contain Unicode characters from planes 0-2
1 parent 2265152 commit 9cc096b

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

src/org/sosy_lab/java_smt/api/StringFormulaManager.java

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,9 @@ public interface StringFormulaManager {
2323
* Creates a {@link StringFormula} representing the given constant String.
2424
*
2525
* <p>This method accepts plain Java Strings with Unicode characters from the Basic Multilingual
26-
* Plane (BMP) (codepoints in range [0x00000, 0x2FFFF]). JavaSMT handles escaping internally, as
27-
* some solvers follow the SMTLIB standard and escape Unicode characters with curly braces.
26+
* Plane (BMP) or planes 1 and 2 (codepoints in range [0x00000, 0x2FFFF]). JavaSMT handles
27+
* escaping internally, as some solvers follow the SMTLIB standard and escape Unicode characters
28+
* with curly braces.
2829
*
2930
* <p>Additionally, you can use SMTLIB escaping like "\\u{1234}" to represent Unicode characters
3031
* directly.
@@ -246,8 +247,8 @@ default RegexFormula concat(RegexFormula... parts) {
246247

247248
/**
248249
* Returns a String formula representing the single character with the given code point, if it is
249-
* a valid Unicode code point within the Basic Multilingual Plane (BMP) (codepoints in range
250-
* [0x00000, 0x2FFFF]). Otherwise, returns the empty string.
250+
* a valid Unicode code point within the Basic Multilingual Plane (BMP) or planes 1 and 2
251+
* (codepoints in range [0x00000, 0x2FFFF]). Otherwise, returns the empty string.
251252
*/
252253
StringFormula fromCodePoint(IntegerFormula codePoint);
253254
}

0 commit comments

Comments
 (0)