Average Error: 0.1 → 0.1
Time: 4.4s
Precision: 64
\[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z\]
↓
\[x - \mathsf{fma}\left(\log y, 0.5 + y, z - y\right)\]
\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z
↓
x - \mathsf{fma}\left(\log y, 0.5 + y, z - y\right)
double f(double x, double y, double z) {
        double r245366 = x;
        double r245367 = y;
        double r245368 = 0.5;
        double r245369 = r245367 + r245368;
        double r245370 = log(r245367);
        double r245371 = r245369 * r245370;
        double r245372 = r245366 - r245371;
        double r245373 = r245372 + r245367;
        double r245374 = z;
        double r245375 = r245373 - r245374;
        return r245375;
}
↓
double f(double x, double y, double z) {
        double r245376 = x;
        double r245377 = y;
        double r245378 = log(r245377);
        double r245379 = 0.5;
        double r245380 = r245379 + r245377;
        double r245381 = z;
        double r245382 = r245381 - r245377;
        double r245383 = fma(r245378, r245380, r245382);
        double r245384 = r245376 - r245383;
        return r245384;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original0.1
Target0.1
Herbie0.1
\[\left(\left(y + x\right) - z\right) - \left(y + 0.5\right) \cdot \log y\]

Derivation

  1. Initial program 0.1

    \[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z\]

  2. Simplified0.1

    \[\leadsto \color{blue}{x - \left(\mathsf{fma}\left(\log y, y + 0.5, z\right) - y\right)}\]
  3. Using strategy rm

  4. Applied fma-udef0.1

    \[\leadsto x - \left(\color{blue}{\left(\log y \cdot \left(y + 0.5\right) + z\right)} - y\right)\]

  5. Simplified0.1

    \[\leadsto x - \left(\left(\color{blue}{\log y \cdot \left(0.5 + y\right)} + z\right) - y\right)\]
  6. Using strategy rm

  7. Applied *-un-lft-identity0.1

    \[\leadsto x - \color{blue}{1 \cdot \left(\left(\log y \cdot \left(0.5 + y\right) + z\right) - y\right)}\]

  8. Applied *-un-lft-identity0.1

    \[\leadsto \color{blue}{1 \cdot x} - 1 \cdot \left(\left(\log y \cdot \left(0.5 + y\right) + z\right) - y\right)\]

  9. Applied distribute-lft-out--0.1

    \[\leadsto \color{blue}{1 \cdot \left(x - \left(\left(\log y \cdot \left(0.5 + y\right) + z\right) - y\right)\right)}\]

  10. Simplified0.1

    \[\leadsto 1 \cdot \color{blue}{\left(x - \mathsf{fma}\left(\log y, 0.5 + y, z - y\right)\right)}\]

  11. Final simplification0.1

    \[\leadsto x - \mathsf{fma}\left(\log y, 0.5 + y, z - y\right)\]

Reproduce

herbie shell --seed 2020018 +o rules:numerics
(FPCore (x y z)
  :name "Numeric.SpecFunctions:stirlingError from math-functions-0.1.5.2"
  :precision binary64

  :herbie-target
  (- (- (+ y x) z) (* (+ y 0.5) (log y)))

  (- (+ (- x (* (+ y 0.5) (log y))) y) z))