mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #2837 - expose test function that determines whether an AST is a string literal
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ebc9b7fb4e
commit
2920ee56e9
|
@ -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();
|
||||
|
|
Loading…
Reference in a new issue