Diagrams.Solve.Tridiagonal:solveCyclicTriDiagonal from diagrams-solve-0.1, A

Average Error: 6.2 → 0.5

Time: 12.9s

Precision: 64

Math

\[\frac{x \cdot y}{z}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot y \le -9.54515020118302937 \cdot 10^{238}:\\ \;\;\;\;x \cdot \frac{y}{z}\\ \mathbf{elif}\;x \cdot y \le -4.4678431735909085 \cdot 10^{-156} \lor \neg \left(x \cdot y \le 1.3818627530073868 \cdot 10^{-285}\right) \land x \cdot y \le 4.523491092627816 \cdot 10^{178}:\\ \;\;\;\;\frac{x \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{z}{y}}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r498377 = x;
        double r498378 = y;
        double r498379 = r498377 * r498378;
        double r498380 = z;
        double r498381 = r498379 / r498380;
        return r498381;
}

↓

double f(double x, double y, double z) {
        double r498382 = x;
        double r498383 = y;
        double r498384 = r498382 * r498383;
        double r498385 = -9.545150201183029e+238;
        bool r498386 = r498384 <= r498385;
        double r498387 = z;
        double r498388 = r498383 / r498387;
        double r498389 = r498382 * r498388;
        double r498390 = -4.4678431735909085e-156;
        bool r498391 = r498384 <= r498390;
        double r498392 = 1.3818627530073868e-285;
        bool r498393 = r498384 <= r498392;
        double r498394 = !r498393;
        double r498395 = 4.523491092627816e+178;
        bool r498396 = r498384 <= r498395;
        bool r498397 = r498394 && r498396;
        bool r498398 = r498391 || r498397;
        double r498399 = r498384 / r498387;
        double r498400 = r498387 / r498383;
        double r498401 = r498382 / r498400;
        double r498402 = r498398 ? r498399 : r498401;
        double r498403 = r498386 ? r498389 : r498402;
        return r498403;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	6.2
Target	6.2
Herbie	0.5

\[\begin{array}{l} \mathbf{if}\;z \lt -4.262230790519429 \cdot 10^{-138}:\\ \;\;\;\;\frac{x \cdot y}{z}\\ \mathbf{elif}\;z \lt 1.70421306606504721 \cdot 10^{-164}:\\ \;\;\;\;\frac{x}{\frac{z}{y}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{z} \cdot y\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if (* x y) < -9.545150201183029e+238

   1. Initial program 36.6

      \[\frac{x \cdot y}{z}\]
   2. Using strategy rm

   3. Applied *-un-lft-identity 36.6

      \[\leadsto \frac{x \cdot y}{\color{blue}{1 \cdot z}}\]

   4. Applied times-frac 0.8

      \[\leadsto \color{blue}{\frac{x}{1} \cdot \frac{y}{z}}\]

   5. Simplified 0.8

      \[\leadsto \color{blue}{x} \cdot \frac{y}{z}\]

   if -9.545150201183029e+238 < (* x y) < -4.4678431735909085e-156 or 1.3818627530073868e-285 < (* x y) < 4.523491092627816e+178

   1. Initial program 0.2

      \[\frac{x \cdot y}{z}\]
   2. Using strategy rm

   3. Applied associate-/l* 9.0

      \[\leadsto \color{blue}{\frac{x}{\frac{z}{y}}}\]

   4. Taylor expanded around 0 0.2

      \[\leadsto \color{blue}{\frac{x \cdot y}{z}}\]

   if -4.4678431735909085e-156 < (* x y) < 1.3818627530073868e-285 or 4.523491092627816e+178 < (* x y)

   1. Initial program 13.5

      \[\frac{x \cdot y}{z}\]
   2. Using strategy rm

   3. Applied associate-/l* 1.0

      \[\leadsto \color{blue}{\frac{x}{\frac{z}{y}}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \le -9.54515020118302937 \cdot 10^{238}:\\ \;\;\;\;x \cdot \frac{y}{z}\\ \mathbf{elif}\;x \cdot y \le -4.4678431735909085 \cdot 10^{-156} \lor \neg \left(x \cdot y \le 1.3818627530073868 \cdot 10^{-285}\right) \land x \cdot y \le 4.523491092627816 \cdot 10^{178}:\\ \;\;\;\;\frac{x \cdot y}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{z}{y}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019198 +o rules:numerics
(FPCore (x y z)
  :name "Diagrams.Solve.Tridiagonal:solveCyclicTriDiagonal from diagrams-solve-0.1, A"

  :herbie-target
  (if (< z -4.262230790519429e-138) (/ (* x y) z) (if (< z 1.7042130660650472e-164) (/ x (/ z y)) (* (/ x z) y)))

  (/ (* x y) z))