mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Revert "Cpp api fp to bv (#5218)" (#5221)

Browse source 
This reverts commit fa2d593739.
This commit is contained in:
Nikolaj Bjorner 2021-04-27 08:44:15 -07:00 • committed by GitHub
parent fa2d593739
commit d731ec7cba
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 35 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 {
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,19 +1307,6 @@ 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.
@ -1817,27 +1804,6 @@ 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 <tt>ite(c, t, e)</tt>