Overloading Rust operators for some of the `Ast` functions

prove-rs / z3.rs

Rust bindings for the Z3 solver.

347 stars 110 forks source link

Overloading Rust operators for some of the `Ast` functions #10

Open Armavica opened 5 years ago

Armavica commented 5 years ago

How would you feel about overloading Rust operators, as syntactic sugar for some of the functions in Ast? We can't do all of them, but at least some of the most useful ones like add, sub, mul, div, mod, minus, and, or, xor, not (I may have missed some).

I am happy to work on a PR if this is okay.

waywardmonkeys commented 5 years ago

I'm interested in this ... but a couple of things have stopped me from working on it so far:

I wasn't happy that not all operators would work, especially boolean ones.
I'd like for this to be more type safe, instead of just having an Ast type, having Rust types for the various sorts, so that we can be sure to dispatch to the correct underlying operation.
Perhaps having a macro that parses SMT-LIB or a simple expression language could be nice. (And this would allow all operators to work...)

But that shouldn't stop you!

A good first step might be having some additional types and then creating the operators for them?

I'm happy to see a PR! I'm also happy to have a big discussion here. :)