Adding new floating-point support

[akothen]

Hello,

I am trying to figure out how much effort it took to support floating-point (float-32) support in z3 and how much work it will be to support other floating-point types such as bfloat16, and other floating-point variants. Are there any plans to support more floating-point types?

Thanks.

[NikolajBjorner]

@wintersteiger developed FP support in Z3. It is based on the SMTLIB standard that follows IEEE semantics.
You can specify number of exponent and fraction bits (for bfloat it is 8 + 7) and specify rounding modes.
Do you say these knobs are insufficient to encode bfloat16?

[akothen]

Thanks for your response.
I did not realize that you could specify exponent and fraction bits to z3. How can that be done?

[NikolajBjorner]

http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml

[akothen]

Thanks! This is very helpful.