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

cw review comments #5200

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-20 09:27:46 -07:00
parent 770c79a939
commit 44d77a978a
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -871,9 +871,9 @@ namespace z3 {
bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; } 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 \brief Return Boolean expression to test whether expression is inf
*/ */
expr is_inf() const { expr mk_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();
@ -881,9 +881,9 @@ namespace z3 {
} }
/** /**
\brief Return true if this expression is an fpa and is NaN \brief Return Boolean expression to test for whether expression is a NaN
*/ */
expr is_nan() const { expr mk_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
*/ */
expr to_ieee_bv() const { expr mk_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();