mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Cpp api fp to bv (#5218)

Browse source 
* fpa_to_ubv and fpa_to_sbv added to C++ API

* Bug fix

* fpa_fp method added to API

* Adjust types to prefer sort over expr and bug fix
This commit is contained in:
Zachary Wimer 2021-04-26 17:00:05 -07:00 • committed by GitHub
parent ecfbc1cc06
commit fa2d593739
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 35 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -895,7 +895,7 @@ namespace z3 {
*/ */
expr mk_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();
return expr(ctx(), r); 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); 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. \brief sequence and regular expression operations.
+ is overloaded as sequence concatenation and regular expression union. + is overloaded as sequence concatenation and regular expression union.
@ -1804,6 +1817,27 @@ namespace z3 {
return expr(a.ctx(), r); 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 <tt>ite(c, t, e)</tt> \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>