mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

#5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-23 18:21:51 +02:00
parent 7f41d6140f
commit 3a3cef8fce
3 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_seq.cpp
View file

@ -198,7 +198,7 @@ extern "C" {
svector<char> buff; svector<char> buff;
for (unsigned i = 0; i < str.length(); ++i) { for (unsigned i = 0; i < str.length(); ++i) {
unsigned ch = str[i]; unsigned ch = str[i];
if (ch <= 32 || ch >= 127 || (ch == '\\' && i + 1 < str.length() && str[i+1] == 'u')) { if (ch == 0 || ch >= 256 || (ch == '\\' && i + 1 < str.length() && str[i+1] == 'u')) {
buff.reset(); buff.reset();
buffer.push_back('\\'); buffer.push_back('\\');
buffer.push_back('u'); buffer.push_back('u');

7
src/api/c++/z3++.h
View file

@ -1120,12 +1120,9 @@ namespace z3 {
std::u32string get_u32string() const { std::u32string get_u32string() const {
assert(is_string_value()); assert(is_string_value());
unsigned n = Z3_get_string_length(ctx(), m_ast); unsigned n = Z3_get_string_length(ctx(), m_ast);
std::vector<unsigned> buffer;
buffer.resize(n);
Z3_get_string_contents(ctx(), m_ast, n, buffer.data());
std::u32string s; std::u32string s;
for (auto ch : buffer) s.resize(n);
s.push_back(ch); Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
return s; return s;
} }

11
src/api/z3_api.h
View file

@ -3480,6 +3480,11 @@ extern "C" {
/** /**
\brief Create a string constant out of the string that is passed in \brief Create a string constant out of the string that is passed in
The string may contain escape encoding for non-printable characters
or characters outside of the basic printable ASCII range. For example,
the escape encoding \u{0} represents the character 0 and the encoding
\u{100} represents the character 256.
def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING))) def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING)))
*/ */
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s); Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
@ -3487,7 +3492,8 @@ extern "C" {
/** /**
\brief Create a string constant out of the string that is passed in \brief Create a string constant out of the string that is passed in
It takes the length of the string as well to take into account It takes the length of the string as well to take into account
0 characters. The string is unescaped. 0 characters. The string is treated as if it is unescaped so a sequence
of characters \u{0} is treated as 5 characters and not the character 0.
def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING))) def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING)))
*/ */
@ -3511,6 +3517,7 @@ extern "C" {
/** /**
\brief Retrieve the string constant stored in \c s. \brief Retrieve the string constant stored in \c s.
Characters outside the basic printiable ASCII range are escaped.
\pre Z3_is_string(c, s) \pre Z3_is_string(c, s)
@ -3520,6 +3527,8 @@ extern "C" {
/** /**
\brief Retrieve the string constant stored in \c s. The string can contain escape sequences. \brief Retrieve the string constant stored in \c s. The string can contain escape sequences.
Characters in the range 1 to 255 are literal.
Characters in the range 0, and 256 above are escaped.
\pre Z3_is_string(c, s) \pre Z3_is_string(c, s)