search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
640 stars 74 forks source link

Adding Custom Floating Point Support #257

Open RafaeNoor opened 1 year ago

RafaeNoor commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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