Allow creating Int from i32

[Salt-Factory]

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:

let s = ast::Int::new_const(&ctx, "s");
let o = ast::Int::new_const(&ctx, "o");
let mult = &s * 10;
solver.assert(&s._eq(&o));

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 writing as i64 is tedious, I open this MR to (1) allow generating ast::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?

[Pat-Lafon]

What about converting from_i64 to accept anything that satisfies Into<i64>? Would that still work but also support more integer types?

[Salt-Factory]

What about converting from_i64 to accept anything that satisfies Into<i64>? Would that still work but also support more integer types?

Sure, if that's feasible it would definitely work. :-) My rust knowledge is a bit limited though, and I couldn't figure out how to make it work with the impl_binary_mult_op_number_raw! macros. You would still need a macro per integer type, right? So while a generic from_int would work, you would still be limited in what types you allow in your macro.

[Pat-Lafon]

Hmmm, this is doable except that there needs to have extra handling for the impl's because Into<i64> will also work u64 which is currently implemented separately and uses Z3_mk_unsigned_int64 instead. I'm think those are suppose to be kept distinct? I'm not sure what sign-ness means on the z3 c side.

It's a bit hacky to work around, maybe leveraging TryInto<u64> to see if the value fits in an unsigned value? I'm not sure when the number being sign/unsigned matters.

 macro_rules! impl_binary_op_number_raw {
     ($ty:ty, $other:ty, $other_fn:ident, $output:ty, $base_trait:ident, $base_fn:ident, $function:ident, $construct_constant:ident) => {
-        impl<'ctx> $base_trait<$other> for $ty {
+        impl<'ctx, T : Into<$other>> $base_trait<T> for $ty {
             type Output = $output;

-            fn $base_fn(self, rhs: $other) -> Self::Output {
+            fn $base_fn(self, rhs: T) -> Self::Output {
                 let c;
-                $construct_constant!(c, $other_fn, rhs, self);
+                $construct_constant!(c, $other_fn, rhs.into(), self);
                 $base_trait::$base_fn(self, c)
             }
         }

[waywardmonkeys]

Maybe there's room here to use num or num-traits?

[Pat-Lafon]

Maybe there's room here to use num or num-traits?

Sort of? So num_traits::Signed/Unsigned is what we want here, but my attempt currently doesn't work because (I think) we haven't proven to the compiler that they aren't overlapping.

error[E0119]: conflicting implementations of trait `Div<_>` for type `ast::Int<'_>`

I think this is akin to https://stackoverflow.com/questions/39159226/conflicting-implementations-of-trait-in-rust. I think if they were Sealed traits this would work. Or Z3 could have it's own marker trait for this as mentioned in the comments of the above post.

impl<'ctx, T: Into<i64> + num_traits::Signed> Div<T> for Int<'ctx> {
    type Output = Int<'ctx>;
    fn div(self, rhs: T) -> Self::Output {
        let c;
        c = Int::from_i64(self.get_ctx(), (rhs.into()));
        Div::div(self, c)
    }
}
impl<'ctx, T: Into<u64> + num_traits::Unsigned> Div<T> for Int<'ctx> {
    type Output = Int<'ctx>;
    fn div(self, rhs: T) -> Self::Output {
        let c;
        c = Int::from_u64(self.get_ctx(), (rhs.into()));
        Div::div(self, c)
    }
}