Skip to content

Conversation

@KpwnZ
Copy link
Contributor

@KpwnZ KpwnZ commented Jul 22, 2025

This PR exposes the Z3_mk_fpa_to_fp_bv() API which is useful for interpreter memory model.

@toolCHAINZ
Copy link
Member

Thanks for the contribution! Could you add some unit tests for these new APIs? I think it would be particularly helpful for library users to see the usage of from_ieee_bv. I'm a little on the fence about that one; it is good to support the full bredth of floating point types Z3 can operate on, but I think most users will be using the 32 or 64 bit variants. So I worry a little about which one people will find first. I wish that there was a way to tighten the types on that API (e.g. the Sort has to be a Float Sort), but that doesn't seem possible with how z3.rs currently represents Sorts.

For the other two APIs, I think it would be pretty slick to show a round-trip betwen Floats and BVs using the existing Float::to_ieee_bv impl and as_f64.

@toolCHAINZ toolCHAINZ added the enhancement New feature or request label Aug 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants