News for hackers. Stuff that matters.

A comment on A DSL for peephole transformation rules of integer operations in the PyPy JIT. Parent comment

Re:A DSL for peephole transformation rules of integer operat... by cfbolztereick on Wednesday October 23, 2024 @02:53PM (#41928178)
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)

[ Parent | on HN ]
Re:A DSL for peephole transformation rules of integer operat... by westurner on Friday October 25, 2024 @06:54AM (#41944043)
Does 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.)

[ Parent | on HN ]