Average Error: 6.6 → 2.1
Time: 44.2s
Precision: 64
\[x + \frac{y \cdot \left(z - x\right)}{t}\]
\[\mathsf{fma}\left(z - x, \frac{y}{t}, x\right)\]
x + \frac{y \cdot \left(z - x\right)}{t}
\mathsf{fma}\left(z - x, \frac{y}{t}, x\right)
double f(double x, double y, double z, double t) {
        double r16957105 = x;
        double r16957106 = y;
        double r16957107 = z;
        double r16957108 = r16957107 - r16957105;
        double r16957109 = r16957106 * r16957108;
        double r16957110 = t;
        double r16957111 = r16957109 / r16957110;
        double r16957112 = r16957105 + r16957111;
        return r16957112;
}

double f(double x, double y, double z, double t) {
        double r16957113 = z;
        double r16957114 = x;
        double r16957115 = r16957113 - r16957114;
        double r16957116 = y;
        double r16957117 = t;
        double r16957118 = r16957116 / r16957117;
        double r16957119 = fma(r16957115, r16957118, r16957114);
        return r16957119;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original6.6
Target2.1
Herbie2.1
\[x - \left(x \cdot \frac{y}{t} + \left(-z\right) \cdot \frac{y}{t}\right)\]

Derivation

  1. Initial program 6.6

    \[x + \frac{y \cdot \left(z - x\right)}{t}\]
  2. Using strategy rm
  3. Applied *-un-lft-identity6.6

    \[\leadsto x + \color{blue}{1 \cdot \frac{y \cdot \left(z - x\right)}{t}}\]
  4. Applied *-un-lft-identity6.6

    \[\leadsto \color{blue}{1 \cdot x} + 1 \cdot \frac{y \cdot \left(z - x\right)}{t}\]
  5. Applied distribute-lft-out6.6

    \[\leadsto \color{blue}{1 \cdot \left(x + \frac{y \cdot \left(z - x\right)}{t}\right)}\]
  6. Simplified2.1

    \[\leadsto 1 \cdot \color{blue}{\mathsf{fma}\left(z - x, \frac{y}{t}, x\right)}\]
  7. Final simplification2.1

    \[\leadsto \mathsf{fma}\left(z - x, \frac{y}{t}, x\right)\]

Reproduce

herbie shell --seed 2019168 +o rules:numerics
(FPCore (x y z t)
  :name "Optimisation.CirclePacking:place from circle-packing-0.1.0.4, D"

  :herbie-target
  (- x (+ (* x (/ y t)) (* (- z) (/ y t))))

  (+ x (/ (* y (- z x)) t)))