4 ms·
I only support integer operations in the DSL so far. (but yes, turning the python expression x*y+z into an fma call would not be a legal optimization for the j
by cfbolztereick 2y ago
I only support integer operations in the DSL so far.
(but yes, turning the python expression x*y+z into an fma call would not be a legal optimization for the jit anyway. And Z3 would rightfully complain. The results must be bitwise identical before and after optimization)
- westurner 2y agoDoes Z3 distinguish between x*y+z and z+y*x, in terms of floating point output? math.fma() would be a different function call with the same or similar output. (deal-solver is a tool for verifying formal implementations in Python with Z3.)