Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

No way to access the raw Z3_sort from Sort<'ctx> or Z3_context from Context #290

Closed
Dessix opened this issue May 5, 2024 · 0 comments · Fixed by #298
Closed

No way to access the raw Z3_sort from Sort<'ctx> or Z3_context from Context #290

Dessix opened this issue May 5, 2024 · 0 comments · Fixed by #298

Comments

@Dessix
Copy link

Dessix commented May 5, 2024

Most functionality around Float types is unbound. Adding bindings without editing or forking this library is impossible without the extreme hack of declaring copies of the structs and transmuting references between them to trick Rust into accessing the private fields z3_sort or z3_ctx.

I was attempting to invoke z3_sys's Z3_mk_fpa_to_fp_real, but it requires raw access to the Z3_sort values, as well as a rounding mode, but functions like z3_sys::Z3_mk_fpa_rne require an instance of the raw Z3_context, which lack a high-level wrapper.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant