Adding Custom Floating Point Support

[RafaeNoor]

Hello Emina and others.

I wanted to inquire how one would go about supporting floating point types for synthesis / verification in Rosette. It appears that IEEE floats are supported in Z3 as seen here. Reals are already supported in Rosette and that's great, but it would be useful to be able to model FP16, FP32 (even BF16?).

[emina]

You would have to replicate the support for other built-in types, such as integers, reals, or bitvectors. This is a lot of work. It involves building symbolic encodings and partial evaluation for the operators on the type you want to support; extending the code that translates Rosette terms to SMTLib; and extending the code that constructs Rosette values from SMTLib models.

As an example of implementing some of this, see here or here.

You’ll also need to be careful to account for any discrepancies between Z3’s floating point semantics and Racket’s floating point semantics.

[RafaeNoor]

I see, that definitely seems like significant work and even more so to ensure it's correct. I was scanning through the repo and found synthcl support for converting float_16 and other float types. Does this mean that some form of fp16 is already supported in Rosette?

[emina]

There is no support for floats in Rosette; synthcl is just approximating floats with integers.