Skip to content

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

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

Rust Z3. How can I convert Float to f32/f64? #6958

Closed
FoxMakarov opened this issue Oct 21, 2023 · 1 comment · Fixed by prove-rs/z3.rs#252
Closed

Rust Z3. How can I convert Float to f32/f64? #6958

FoxMakarov opened this issue Oct 21, 2023 · 1 comment · Fixed by prove-rs/z3.rs#252

Comments

@FoxMakarov
Copy link

Hello, everyone!
I am learning to use z3-prover in my rust program. But i encountered some problems.

I am using Float like in the tutorial (https://docs.rs/z3/0.10.0/z3/ast/struct.Float.html). But I noticed that it only has functions that convert from f32/f64 to Float Without converting from Float to f32/f64 function.

 // Create a 32-bit (IEEE-754) Float [`Ast`](trait.Ast.html) from a rust f32
pub fn from_f32(ctx: &'ctx Context, value: f32) -> Float<'ctx> 

// Create a 64-bit (IEEE-754) Float [`Ast`](trait.Ast.html) from a rust f64
pub fn from_f64(ctx: &'ctx Context, value: f64) -> Float<'ctx> 

I want to know if there is a method that can be used like the as_i64 function of 'Int' structure which can convert 'Int' to the i64 variable of Rust.

How can I convert 'Float' to f32/f64?
Can you help me please?

z3 version : 0.10.0

@waywardmonkeys
Copy link
Contributor

I've created prove-rs/z3.rs#252 which would fix this ... I'll merge it into master over there within a day or so if I don't hear any reason not to ...

@Z3Prover Z3Prover locked and limited conversation to collaborators Oct 24, 2023
@NikolajBjorner NikolajBjorner converted this issue into discussion #6962 Oct 24, 2023
waywardmonkeys added a commit to prove-rs/z3.rs that referenced this issue Oct 25, 2023

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants