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

C++ API add missing FP methods (#5199)

Browse source 
* added is_nan and is_inf to API

* added support to to_ieee_bv
This commit is contained in:
Zachary Wimer 2021-04-19 15:24:09 -07:00 • committed by GitHub
parent 542878dea3
commit 10e9345cd7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 30 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -870,6 +870,36 @@ 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
*/
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 \brief Return string representation of numeral or algebraic number
This method assumes the expression is numeral or algebraic This method assumes the expression is numeral or algebraic