search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Add creating reals from any numeral and getting f64 from reals #287

Closed lucascool12 closed 1 month ago

lucascool12 commented 5 months ago

Adds the ability to create Reals from any numeral using Z3_mk_numeral. Also adds the method as_f64 to Real which uses Z3_get_numberal_double.

This is useful if you want to represent a real as a f64. Currently you would have to calculate the numerator and denominator in order to create a z3 real from a f64. With this merge request all you would need to do is create a string from your f64 and pass this to from_str.

lucascool12 commented 1 month ago

I fixed the relevant parts of the CI, and then accidentally clicked close pull request, whoops.

dragazo commented 1 month ago

Z3_get_numeral_double fails (by returning zero) if the result cannot be stored perfectly in a 64-bit floating-point value. For example, the irrational number sqrt(2) would have this issue. If that's the intended behavior in this PR, we might want to call it something like as_exact_f64 or exact_f64. As a user, I'd also want it to return Option<f64> instead of f64 with a default 0.0 for failure - although I don't know if Z3 exposes a way to check if that operation succeeds, at least not directly. But we could always check an integer or rational conversion to resolve the 0.0 ambiguous case after the fact.

But if that's not the intended behavior, I have a separate PR that works even for irrational numbers: #304, in which case we could drop the as_f64 from this PR and both PRs can be merged eventually.

lucascool12 commented 1 month ago

I didn't know Z3_get_numeral_double could fail. #304 is pretty much what I need for my use case. Except that it is missing the ability to create a Real from a numeral string, I'll put this in a different PR. Still we could keep this PR alive for exact f64 as you said. The documentation specifies that the precondition of Z3_get_numeral_double is Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || Z3_is_algebraic_number(c, a), I tried this but got unexpected results. The method @dragazo described does seem to work. I'll change to title of the PR.

lucascool12 commented 1 month ago

I'll change to title of the PR. Scratch that I'll close this one and create 2 new ones.