mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 02:16:16 +00:00
Code Activity

Cpp api add missing fp methods (return type correction) (#5200)

Browse source 
* added is_nan and is_inf to API

* added support to to_ieee_bv

* bug fix
This commit is contained in:
Zachary Wimer 2021-04-19 17:55:23 -07:00 • committed by GitHub
parent 10e9345cd7
commit 831afa8124
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -873,7 +873,7 @@ namespace z3 {
/** /**
\brief Return true if this expression is an fpa and is inf \brief Return true if this expression is an fpa and is inf
*/ */
bool is_inf() const { expr is_inf() const {
assert(is_fpa()); assert(is_fpa());
Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast); Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
check_error(); check_error();
@ -883,7 +883,7 @@ namespace z3 {
/** /**
\brief Return true if this expression is an fpa and is NaN \brief Return true if this expression is an fpa and is NaN
*/ */
bool is_nan() const { expr is_nan() const {
assert(is_fpa()); assert(is_fpa());
Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast); Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
check_error(); check_error();
@ -893,7 +893,7 @@ namespace z3 {
/** /**
\brief Convert this fpa into an IEEE BV \brief Convert this fpa into an IEEE BV
*/ */
bool to_ieee_bv() const { expr to_ieee_bv() const {
assert(is_fpa()); 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(); check_error();