diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 701381176..9d1006e2a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -745,6 +745,7 @@ namespace z3 { bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; } bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; } bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; } + /** \brief Return true if this expression is an application. */ @@ -895,18 +896,27 @@ namespace z3 { return expr(ctx(),r); } + + /** + \brief Return true if this expression is a string literal. + The string can be accessed using \c get_string() and \c get_escaped_string() + */ + bool is_string_value() const { return Z3_is_string(ctx(), m_ast); } + /** \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 { + std::string get_escaped_string() const { + assert(is_string_value()); char const* s = Z3_get_string(ctx(), m_ast); check_error(); return std::string(s); } std::string get_string() const { + assert(is_string_value()); unsigned n; char const* s = Z3_get_lstring(ctx(), m_ast, &n); check_error();