prove-rs / z3.rs

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

Real approx functions #304

Closed dragazo closed 1 month ago

dragazo commented 1 month ago

It's a bit difficult to work with Real (in z3, not z3-sys) since the only provided way to get a value out at the end is Real::as_real(&self) -> Option<(i64, i64)>, which really only works for rational numbers. In this PR I've added two new functions to help:

I also noticed that tests/objectives.rs, tests/ops.rs, and tests/semver_tests.rs weren't actually having their tests executed since they weren't linked into the lib, so I declared them as (test) modules. It looks like some of those are failing, but that's not something that this PR caused.

waywardmonkeys commented 1 month ago

I'll fix that clippy error and then you can rebase.

waywardmonkeys commented 1 month ago

Oops, never mind ... that's in your code!

dragazo commented 1 month ago

Sure, I think I just fixed the last of the clippy issues.

waywardmonkeys commented 1 month ago

Thanks!