From 10e9345cd79a66c4fffd513d153a68abdd3568e4 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Mon, 19 Apr 2021 15:24:09 -0700 Subject: [PATCH] C++ API add missing FP methods (#5199) * added is_nan and is_inf to API * added support to to_ieee_bv --- src/api/c++/z3++.h | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index aecffc31d..f4991817d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -870,6 +870,36 @@ namespace z3 { */ bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; } + /** + \brief Return true if this expression is an fpa and is inf + */ + bool is_inf() const { + assert(is_fpa()); + Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast); + check_error(); + return expr(ctx(), r); + } + + /** + \brief Return true if this expression is an fpa and is NaN + */ + bool is_nan() const { + assert(is_fpa()); + Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast); + check_error(); + return expr(ctx(), r); + } + + /** + \brief Convert this fpa into an IEEE BV + */ + bool to_ieee_bv() const { + assert(is_fpa()); + Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast), + check_error(); + return expr(ctx(), r); + } + /** \brief Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic