prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Real fn renames and Eq refactor #305

Open dragazo opened 1 month ago

dragazo commented 1 month ago

Note: this PR contains breaking changes, so if merged we should at least change the minor version number before next release

When using this crate, I thought it was confusing that operators are used for symbolic arithmetic but doing the same for checking equality is non-symbolic (ast comparison). To actually check symbolic equality, you need to use _eq(other), which looks weird compared to other symbolic inequality checks like le(other) or gt(other). So in this PR I've renamed _eq to eq, the only cost of which is removing the PartialEq trait impl from the concrete Ast types. Instead, I've added a new method to Ast called ast_eq(&self, other: &dyn Ast) -> bool that does this check explicitly. I think this is less likely to be used accidentally than ==, for which the user probably wants symbolic equality anyway.

Also, there were several functions for Real that take/return a fraction but use the term "real" (e.g., from_real(i32, i32)). I've renamed these to "rational".

Also, for the new from_rational function (replacing from_real), I changed the input types to i64 instead of i32, but the deprecated wrapper still uses i32. This is to match the return type of as_rational (new name for as_real but otherwise unchanged).

For all of the function renames, I kept a shallow wrapper with the old name and just marked it as deprecated. So the renames aren't a breaking change, but removing the PartialEq impl is.

waywardmonkeys commented 1 month ago

Thanks!

I think this sounds like an improvement!

If you could:

That would be great!

dragazo commented 1 month ago

Sure, I just merged and squashed it back down to one commit.