Skip to content

Conversation

@jbransen
Copy link
Contributor

@jbransen jbransen commented Dec 8, 2025

While trying to work with Real values I encountered a couple of issues that this PR fixes:

  • format!("{:?}", self.abs()) might use scientific notation, e.g. 1e-2, which is not accepted by at least Z3. Instead, I fixed the precision to 10 digits, which is somewhat arbitrary, but at least it always leads to valid terms, and is likely enough for most applications.
  • Most conversions used Into instead of IntoWithStorage
  • There was no Decimal support, while those can be nicely formatted exactly. I did put this behind a feature flag because it induces an extra dependency
  • Division was using integer division instead of real division. Fixes Support Real Division #10

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.

Support Real Division

2 participants