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.
Hi,
Thank you for the neat package. I've been a long time user of Z3 through Python, and am now looking into switching to Rust for more performance. One hurdle I encountered is mathematical operations with
Int
and i32. E.g., I would like to do the following:This would fail, because by default integers in Rust are i32 and
ast::Int
can currently only be created from i64 or u64. As constantly writingas i64
is tedious, I open this MR to (1) allow generatingast::Int
from i32, and (2) to support automatically converting i32 to Int in binops.Implementation-wise, it's really nothing special: cast the i32 to i64 and use
from_i64
. Not sure if this fits within the Rust ideology, but from Z3's point of view it doesn't matter anyway. Is this something that would be useful?