Improve Python bindings

[Sh4rK]

Hi!
I just played a little with the FP support in the unstable branch (in Python), and while doing so, I noticed some things that I think could be improved:

• the fpTo* functions that convert FP values to something else return FPRefs instead of what they convert to. This is a problem because some functions and operators don't work correctly this way if for example both of their arguments are fpToIEEEBV(foo)
• there are fpTo* functions that actually convert from something to FP (like fpToFPUnsigned) and the naming makes this pretty confusing (something like UBVToFp would be much clearer, mirroring fpToUBV)
• this is mostly the expansion of the previous item; it would be nice if all the conversion functions would be consistently named.

That is all for now, If I notice anything else I'll add it. If I'm wrong about something, please do tell me :)

[wintersteiger]

Thanks for the feedback, it's good to see that people are starting to use floats!

The expression types in fpTo* were indeed wrong, this is now fixed in unstable.

Regarding the naming scheme: "fp" is a general prefix for all floating-point things, avoiding possible clashes with other theories (e.g., fpAdd vs bvAdd vs "+"). The idea was to be mimic the function names defined in the SMT theory FP, in the case of to_fp this is consistent, but indeed a bit unfortunate.

[Sh4rK]

Thanks for the fix.
As for the conversions, there could be a higher-level api, like the operators are overloaded too for the different types. I'm thinking of methods on the different Ref types, for example foo.toSBV(). What do you think about that?

[wintersteiger]

That sounds like a good idea. Does Python support operator overloading of this kind so that expressions are converted automagically? The conversion functions are global because that's the convention that was used for all the other theories (see e.g., ToReal, ToInt, BV2Int), so I'd rather keep that global too, but if think automatic casting would be a nice feature.

[Sh4rK]

I'm not talking about "automagical" stuff, just having methods on the types. The global functions wouldn't change anything, this would be just an addition, a (in my opinion) more pleasant way to do these conversions (for all types, not only for FP).

[wintersteiger]

Aha, I see! Are there Python editors that pop up a list of members e.g., like in Visual Studio or Eclipse?

[Sh4rK]

There's PyCharm which does pretty much everything, but I think there are others too.