Average Error: 0.1 → 0.1
Time: 4.3s
Precision: 64
\[\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z\]
↓
\[x - \mathsf{fma}\left(\log y, y + 0.5, z - y\right)\]
\left(\left(x - \left(y + 0.5\right) \cdot \log y\right) + y\right) - z
↓
x - \mathsf{fma}\left(\log y, y + 0.5, z - y\right)
double f(double x, double y, double z) {
        double r376710 = x;
        double r376711 = y;
        double r376712 = 0.5;
        double r376713 = r376711 + r376712;
        double r376714 = log(r376711);
        double r376715 = r376713 * r376714;
        double r376716 = r376710 - r376715;
        double r376717 = r376716 + r376711;
        double r376718 = z;
        double r376719 = r376717 - r376718;
        return r376719;
}
↓
double f(double x, double y, double z) {
        double r376720 = x;
        double r376721 = y;
        double r376722 = log(r376721);
        double r376723 = 0.5;
        double r376724 = r376721 + r376723;
        double r376725 = z;
        double r376726 = r376725 - r376721;
        double r376727 = fma(r376722, r376724, r376726);
        double r376728 = r376720 - r376727;
        return r376728;
}

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. Applied associate--l+0.1

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

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

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

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

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

  9. Applied distribute-lft-out--0.1

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

  10. Simplified0.1

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

  11. Final simplification0.1

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

Reproduce

herbie shell --seed 2020060 +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))