More conversions between types

[PhilippWendler]

Currently the API does not offer a possibility to convert for example between bitvector formulas and integer formulas, although at least MathSAT has support for this. The only type conversions offered are between floats and anything else via FloatingPointFormulaManager.cast* (but only conversions between floats and bitvectors are actually implemented), and between integers and rationals (because integers can be used in place of rationals).

We should

• provide a more general API for type conversions
• systematically go through and implement all cases that are supported for each solver

[kfriedberger]

Possible conversions are defined by SMTlib. We might need to check whether or how far the solvers support them.

I would suggest to allow the following conversions:

from \ to	Int	Real	FP	BV
Int	:heavy_check_mark:=	:heavy_check_mark:=	real2fp	:heavy_check_mark:nat2bv
Real	:heavy_check_mark:floor	:heavy_check_mark:=	real2fp	via Int or FP?
FP	via Real?	fp2real, NaN/Inf?	fp2fp	:heavy_check_mark:ieee_fp2bv
BV	:heavy_check_mark:bv2nat	:heavy_check_mark:bv2nat	:heavy_check_mark:ieee_bv2fp	:heavy_check_mark:extend/extract

and lets ignore Bool and Array theory. Some conversions are lossless, others use rounding and lose information.

Related commits:

• 26627bd9015dd592345dbd27ece605c62b20adc7 : adding new method 'FLOOR' into API.
• afa63b47e74583cfdcb3fdba61033872eecccdd0 : add new method to convert formulas from BV to INT.

[kfriedberger]

This seems to be sufficiently supported until now. Lets close this issue until we need more conversions.