Enhancement: Use operator overloading in the .NET API about z3 HOT 7 CLOSED

I agree, that would be nice, but C# doesn't allow overloading of && and ||. Given that we can't have a complete set of operators, we decided not to go there at all.

from z3.

I think C# does allow overloading of & and |. Booth are listed as overloadable operators in the documentation as well:
https://msdn.microsoft.com/en-us/library/8edha89s.aspx?f=255&MSPPError=-2147217396

Some solvers (Gurobi for example) do provide those overloads and I find them very useful.

from z3.

Yes, it does, but it doesn't allow overloading of && and ||, which would clearly be the most useful. Note that we also have bit-vectors, so if we use & for Booleans, we can't use it for bv_and anymore.

from z3.

&& and || are evaluated by calls to & and |, respectively. Shouldn't it all just work, if you implement it this way (examples for &):

• BoolExpr & BoolExpr --> BoolExpr
• BitVecExpr & BitVecExpr --> BitVecExpr

Similar to the regular use of & in C#, it should just work for both, bitwise and boolean, scenarios and just return the respective type as result.

I'm probably not thinking properly...

from z3.

Yes, that would be possible, but it would be inconsistent with the C++ and Python APIs, and the Java API as well (Java doesn't support overloading). Note that & and && are not the same in C++ (or any other language), specifically, if their result is used in an if-condition, the result of & will silently be cast to an int and compared to zero, but in Z3 there are no silent casts. If things were the other way around (&& overloadable, not &), we could think about adding just the Boolean case (not everybody needs BitVectors, but everybody needs Booleans), but that isn't the case. So after re-evaluating the situation, I'm still opposed to adding this.

from z3.

I personally don't see the value of API consistency across programming languages. But it's ok.

from z3.

Granted for new end-users there is little benefit. It does make it a lot easier to maintain all the different APIs though, because we can basically apply patches to all of them at the same time with little chance of introducing new bugs (e.g., the Java API started as a literal copy of the .NET library with a couple of sed commands run over it)..

from z3.