search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
347 stars 110 forks source link

Floating point ast Subtype #74

Open pascalkuthe opened 4 years ago

pascalkuthe commented 4 years ago

May I suggest adding an high lvl api for floating point numbers? I am currently writing a compiler for a DSL whose static analysis heavily relies on making floating point assertions. I was considering just writing my own abstraction but I guess it makes more sense to just add it upstream.

Is there any interest in me writing this abstraction or would some already involved be willing to write it ( I do not have much experience with this project but from looking at sources I guess I should manage)?

fitzgen commented 4 years ago

A floating point AST type would be very welcome!

Maybe makes sense to specialize to just 16/32/64/128 floats, rather than expose the configurable knobs for significand and exponent?