Suggestion: Overload operator % in C++ API

[linkret]

Currently I have to use z3::mod(expr_a, expr_b), which is okay, but if all the other operators got overloaded, this one could (should?) be as well.

Also, it's currently possible to just type (expr_a) % (expr_b), and it compiles, but this won't return an z3::expr, but a number, I think? And it won't be the correct number, but some junk? In my opinion overloading operator% with z3::mod(a,b) would be better, so that people don't accidentally do this.

I'm using stable build 4.8.5 for Windows x64.

[NikolajBjorner]

sounds reasonable. There is both a 'mod' and a 'rem'. Conventions should be similar for python, thus mod in python is %. For arithmetic it translates to mod, for bit-vectors to bvsmod, and for floating points to fpRem. Perhaps this is arbitrary.

[wintersteiger]

I think that C++ does not provide a default implementation for % on floats/doubles, because it wouldn't be clear which flavor of mod it should be (fmod, remainder*, FPREM1). So, I don't think we should provide one either. For ints and bit-vectors I think it would be fine too.