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

Real approx functions #304

Merged
merged 4 commits into from
Jul 26, 2024
Merged

Real approx functions #304

merged 4 commits into from
Jul 26, 2024

Conversation

dragazo
Copy link
Contributor

@dragazo dragazo commented Jul 25, 2024

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:

  • Real::approx(&self, precision: usize) -> ::std::string::String, which gives a string approximation of the real value up to precision correct digits after the decimal (via Z3_get_numeral_decimal_string).
  • Real::approx_f64(&self) -> f64, which is just a convenience wrapper for self.approx(17).parse().unwrap() to get a full-precision f64 approximation of the real number.

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
Copy link
Contributor

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

@waywardmonkeys
Copy link
Contributor

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

@dragazo
Copy link
Contributor Author

dragazo commented Jul 25, 2024

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

@waywardmonkeys waywardmonkeys merged commit 42bae5f into prove-rs:master Jul 26, 2024
11 checks passed
@waywardmonkeys
Copy link
Contributor

Thanks!

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 this pull request may close these issues.

2 participants