Linear.Projection:inverseInfinitePerspective from linear-1.19.1.3

Average Error: 7.0 → 0.7

Time: 15.6s

Precision: 64

Math

\[\left(x \cdot y - z \cdot y\right) \cdot t\]

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot y = -\infty:\\ \;\;\;\;\left(x - z\right) \cdot \left(y \cdot t\right)\\ \mathbf{elif}\;x \cdot y - z \cdot y \le -3.01969332327813176444211385258576648371 \cdot 10^{-143}:\\ \;\;\;\;t \cdot \left(x \cdot y - z \cdot y\right)\\ \mathbf{elif}\;x \cdot y - z \cdot y \le 4.552477462007026790110651568839259465513 \cdot 10^{-277}:\\ \;\;\;\;\left(x - z\right) \cdot \left(y \cdot t\right)\\ \mathbf{elif}\;x \cdot y - z \cdot y \le 3.076120724133642014381167424823289378764 \cdot 10^{147}:\\ \;\;\;\;t \cdot \left(x \cdot y - z \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - z\right) \cdot \left(y \cdot t\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r22422366 = x;
        double r22422367 = y;
        double r22422368 = r22422366 * r22422367;
        double r22422369 = z;
        double r22422370 = r22422369 * r22422367;
        double r22422371 = r22422368 - r22422370;
        double r22422372 = t;
        double r22422373 = r22422371 * r22422372;
        return r22422373;
}

↓

double f(double x, double y, double z, double t) {
        double r22422374 = x;
        double r22422375 = y;
        double r22422376 = r22422374 * r22422375;
        double r22422377 = z;
        double r22422378 = r22422377 * r22422375;
        double r22422379 = r22422376 - r22422378;
        double r22422380 = -inf.0;
        bool r22422381 = r22422379 <= r22422380;
        double r22422382 = r22422374 - r22422377;
        double r22422383 = t;
        double r22422384 = r22422375 * r22422383;
        double r22422385 = r22422382 * r22422384;
        double r22422386 = -3.0196933232781318e-143;
        bool r22422387 = r22422379 <= r22422386;
        double r22422388 = r22422383 * r22422379;
        double r22422389 = 4.552477462007027e-277;
        bool r22422390 = r22422379 <= r22422389;
        double r22422391 = 3.076120724133642e+147;
        bool r22422392 = r22422379 <= r22422391;
        double r22422393 = r22422392 ? r22422388 : r22422385;
        double r22422394 = r22422390 ? r22422385 : r22422393;
        double r22422395 = r22422387 ? r22422388 : r22422394;
        double r22422396 = r22422381 ? r22422385 : r22422395;
        return r22422396;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	7.0
Target	3.2
Herbie	0.7

\[\begin{array}{l} \mathbf{if}\;t \lt -9.231879582886776938073886590448747944753 \cdot 10^{-80}:\\ \;\;\;\;\left(y \cdot t\right) \cdot \left(x - z\right)\\ \mathbf{elif}\;t \lt 2.543067051564877116200336808272775217995 \cdot 10^{83}:\\ \;\;\;\;y \cdot \left(t \cdot \left(x - z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y \cdot \left(x - z\right)\right) \cdot t\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (- (* x y) (* z y)) < -inf.0 or -3.0196933232781318e-143 < (- (* x y) (* z y)) < 4.552477462007027e-277 or 3.076120724133642e+147 < (- (* x y) (* z y))

   1. Initial program 21.4

      \[\left(x \cdot y - z \cdot y\right) \cdot t\]

   2. Simplified 1.6

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

   if -inf.0 < (- (* x y) (* z y)) < -3.0196933232781318e-143 or 4.552477462007027e-277 < (- (* x y) (* z y)) < 3.076120724133642e+147

   1. Initial program 0.2

      \[\left(x \cdot y - z \cdot y\right) \cdot t\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot y = -\infty:\\ \;\;\;\;\left(x - z\right) \cdot \left(y \cdot t\right)\\ \mathbf{elif}\;x \cdot y - z \cdot y \le -3.01969332327813176444211385258576648371 \cdot 10^{-143}:\\ \;\;\;\;t \cdot \left(x \cdot y - z \cdot y\right)\\ \mathbf{elif}\;x \cdot y - z \cdot y \le 4.552477462007026790110651568839259465513 \cdot 10^{-277}:\\ \;\;\;\;\left(x - z\right) \cdot \left(y \cdot t\right)\\ \mathbf{elif}\;x \cdot y - z \cdot y \le 3.076120724133642014381167424823289378764 \cdot 10^{147}:\\ \;\;\;\;t \cdot \left(x \cdot y - z \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - z\right) \cdot \left(y \cdot t\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019174 +o rules:numerics
(FPCore (x y z t)
  :name "Linear.Projection:inverseInfinitePerspective from linear-1.19.1.3"

  :herbie-target
  (if (< t -9.231879582886777e-80) (* (* y t) (- x z)) (if (< t 2.543067051564877e+83) (* y (* t (- x z))) (* (* y (- x z)) t)))

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