Implemented missing methods to the C++ API

[mikhailramalho]

(inspired by PR #5234)

I've added the following methods to the C++ API:

• std::ostream & operator<<(std::ostream & out, sort const & s) to print sorts
• mk_is_normal checks if a fp is normal
• mk_is_subnormal checks if a fp is subnormal
• mk_is_zero checks if a fp is zero
• sbv_to_fpa converts from signed bv to fp
• ubv_to_fpa converts from unsigned bv to fp
• fpa_to_fpa converts from fp to fp
• round_fpa_to_closest_integer rounds fp to closest fp
• mk_from_ieee_bv converts from bv (in IEEE format) to fp
• bvredor calls bv reduction or
• bvredand calls bv reduction and
• fp_eq calls fp.eq
• fpa_nan creates a fp NaN
• fpa_inf creates a fp +/-inf

[ghost]

All CLA requirements met.

[mikhailramalho]

I still have a couple of methods that I want in the C++ API but I'm not sure how to implement them properly:

• Z3_mk_fpa_rounding_mode_sort, Z3_mk_fpa_rna (and the others rounding mode ones)

There is context::fpa_rounding_mode which also returns a rounding mode sort, however, it calls Z3_mk_fpa_rna (and the others) directly.

My question is here is that Z3_mk_fpa_rna and the others return Z3_ast but the C++ API is creating a sort out of it. Is that the expected behaviour?

The documentation states that it is indeed returning a sort Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode even though it returns a Z3_ast, but I have been using it for the past few years... I always thought that, e.g., Z3_mk_fpa_rna creates an expression which has sort Z3_mk_fpa_rounding_mode_sort.

[wintersteiger]

Thanks for pointing out these issues! Those definitions in the C++ API are indeed wrong. As you suggest, Z3_mk_fpa_rounding_mode_sort returns a rounding-mode sort and Z3_mk_fpa_rna and friends return a numeral of rounding-mode sort. I think that for pretty much all of these and similar issues, when in doubt, rely on the C API and assume that the C++ is wrong.

m_rounding_mode is the default rounding mode that's applied in the overloaded operators (so you can use +, -, ... without specifying a rounding mode every time). To be honest, I don't like those overloads for floats, but as long as users understand the semantics it's convenient for them. Speaking of which, the default rounding mode in the C++ API is apparently RNA, while many users would expect RNE (see also #4673).

Please go ahead and add those fixes, I'm happy to take another look at this PR or answer more questions after that!

[mikhailramalho]

To be honest, I don't like those overloads for floats, but as long as users understand the semantics it's convenient for them.

I'm not a fan either, especially because you have to set the rounding mode for every operation in SMT... BUT it follows what most programming languages expect you to do, right? Either you explicitly set the rounding mode before the operation(s) or you go with what is already set.

Please go ahead and add those fixes, I'm happy to take another look at this PR or answer more questions after that!

Cool, I've just updated the PR.

I removed expr::fpa_rounding_mode since all operations get the rounding mode from the context, please let me know if it makes sense for you.

[NikolajBjorner]

@wintersteiger I am under the impression that you would comment on this and merge when ready.

I'm happy to take another look at this PR or answer more questions after that!

[wintersteiger]

Yep, that all looks good to me, many thanks for cleaning this up!

[wintersteiger]

@NikolajBjorner the logs of the failed CI builds are not available anymore. Are those expected and be ignored?

[NikolajBjorner]

Seems build retention timeout was met. Since change is to add new code mostly and the main breaking change is rounding mode, which is discussed above, I will merge.

[NikolajBjorner]

Also, I couldn't successfully restart the failed builds. Probably because of retention. As there is no obvious way to start a new build I merged.

[wintersteiger]

Yes, I saw that too. You can manually submit jobs in the pipeline UI, but I forgot why that didn't work for me last week (maybe permission problems, SC-alt accounts etc).

[NikolajBjorner]

The build failures were due to breaks in Julia bindings. I ended up addressing one of the issues by removing the method that broke from Julia. I am not familiar with the use case for floating points from Julia bindings and guessing that it is very low opted for this approach to move forward.