Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
It's a bit difficult to work with
Real
(inz3
, notz3-sys
) since the only provided way to get a value out at the end isReal::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 toprecision
correct digits after the decimal (viaZ3_get_numeral_decimal_string
).Real::approx_f64(&self) -> f64
, which is just a convenience wrapper forself.approx(17).parse().unwrap()
to get a full-precisionf64
approximation of the real number.I also noticed that
tests/objectives.rs
,tests/ops.rs
, andtests/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.