diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 24547891e..51654abd5 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -895,7 +895,7 @@ namespace z3 { */ expr mk_to_ieee_bv() const { assert(is_fpa()); - Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast), + Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast); check_error(); return expr(ctx(), r); } @@ -1307,6 +1307,19 @@ namespace z3 { */ friend expr fma(expr const& a, expr const& b, expr const& c, expr const& rm); + /** + \brief Create an expression of FloatingPoint sort from three bit-vector expressions. + */ + friend expr fpa_fp(expr const& rm, expr const& fp, unsigned bv_len); + /** + \brief Conversion of a floating-point term into a signed bit-vector + */ + friend expr fpa_to_sbv(sort const& rm, expr const& fp, unsigned bv_len); + /** + \brief Conversion of a floating-point term into a unsigned bit-vector + */ + friend expr fpa_to_ubv(sort const& rm, expr const& fp, unsigned bv_len); + /** \brief sequence and regular expression operations. + is overloaded as sequence concatenation and regular expression union. @@ -1804,6 +1817,27 @@ namespace z3 { return expr(a.ctx(), r); } + inline expr fpa_fp(expr const& sgn, expr const& exp, expr const & sig) { + check_context(sgn, exp); check_context(exp, sig); + Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig); + sgn.check_error(); + return expr(sgn.ctx(), r); + } + inline expr fpa_to_sbv(sort const& rm, expr const& fp, unsigned bv_len) { + check_context(rm, fp); + assert(fp.is_fpa()); + Z3_ast r = Z3_mk_fpa_to_sbv(fp.ctx(), rm.m_ast, fp.m_ast, bv_len); + fp.check_error(); + return expr(fp.ctx(), r); + } + inline expr fpa_to_ubv(sort const& rm, expr const& fp, unsigned bv_len) { + check_context(rm, fp); + assert(fp.is_fpa()); + Z3_ast r = Z3_mk_fpa_to_ubv(fp.ctx(), rm.m_ast, fp.m_ast, bv_len); + fp.check_error(); + return expr(fp.ctx(), r); + } + /** \brief Create the if-then-else expression ite(c, t, e)