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

add get_lstring per #2286

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-22 10:31:12 +04:00
parent b2845d888e
commit 082a0f4df4
2 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
examples/c++/example.cpp
View file

@ -1213,6 +1213,14 @@ void recfun_example() {
prove(f(x,c.bool_val(false)) > x); prove(f(x,c.bool_val(false)) > x);
} }
static void string_values() {
context c;
expr s = c.string_val("abc\n\n\0\0", 7);
std::cout << s << "\n";
std::string s1 = s.get_string();
std::cout << s1 << "\n";
}
int main() { int main() {
try { try {
@ -1263,6 +1271,7 @@ int main() {
parse_string(); std::cout << "\n"; parse_string(); std::cout << "\n";
mk_model_example(); std::cout << "\n"; mk_model_example(); std::cout << "\n";
recfun_example(); std::cout << "\n"; recfun_example(); std::cout << "\n";
string_values(); std::cout << "\n";
std::cout << "done\n"; std::cout << "done\n";
} }
catch (exception & ex) { catch (exception & ex) {

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

@ -358,6 +358,7 @@ namespace z3 {
expr fpa_val(float n); expr fpa_val(float n);
expr string_val(char const* s); expr string_val(char const* s);
expr string_val(char const* s, unsigned n);
expr string_val(std::string const& s); expr string_val(std::string const& s);
expr num_val(int n, sort const & s); expr num_val(int n, sort const & s);
@ -793,6 +794,7 @@ namespace z3 {
assert(is_numeral() || is_algebraic()); assert(is_numeral() || is_algebraic());
return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision)); return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
} }
/** /**
\brief retrieve unique identifier for expression. \brief retrieve unique identifier for expression.
@ -892,6 +894,24 @@ namespace z3 {
return expr(ctx(),r); return expr(ctx(),r);
} }
/**
\brief for a string value expression return an escaped or unescaped string value.
\pre expression is for a string value.
*/
std::string get_escaped_string() const {
char const* s = Z3_get_string(ctx(), m_ast);
check_error();
return std::string(s);
}
std::string get_string() const {
unsigned n;
char const* s = Z3_get_lstring(ctx(), m_ast, &n);
check_error();
return std::string(s, n);
}
operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); } operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
/** /**
@ -3029,6 +3049,7 @@ namespace z3 {
inline expr context::fpa_val(double n) { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); } inline expr context::fpa_val(double n) { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::fpa_val(float n) { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); } inline expr context::fpa_val(float n) { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::string_val(char const* s, unsigned n) { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); } inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); } inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }