Average Error: 6.2 → 1.9
Time: 5.9s
Precision: 64
\[\frac{x \cdot y}{z}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \cdot y \le -1.926622627642983907222823390598358692722 \cdot 10^{158}:\\ \;\;\;\;x \cdot \frac{y}{z}\\ \mathbf{elif}\;x \cdot y \le -1.247759449621090803465755159668841719159 \cdot 10^{-277} \lor \neg \left(x \cdot y \le 1.137508288798888459719974341598011528755 \cdot 10^{-219}\right):\\ \;\;\;\;\left(x \cdot y\right) \cdot \frac{1}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{\frac{z}{x}}\\ \end{array}\]
\frac{x \cdot y}{z}
↓
\begin{array}{l}
\mathbf{if}\;x \cdot y \le -1.926622627642983907222823390598358692722 \cdot 10^{158}:\\
\;\;\;\;x \cdot \frac{y}{z}\\

\mathbf{elif}\;x \cdot y \le -1.247759449621090803465755159668841719159 \cdot 10^{-277} \lor \neg \left(x \cdot y \le 1.137508288798888459719974341598011528755 \cdot 10^{-219}\right):\\
\;\;\;\;\left(x \cdot y\right) \cdot \frac{1}{z}\\

\mathbf{else}:\\
\;\;\;\;\frac{y}{\frac{z}{x}}\\

\end{array}
double f(double x, double y, double z) {
        double r595134 = x;
        double r595135 = y;
        double r595136 = r595134 * r595135;
        double r595137 = z;
        double r595138 = r595136 / r595137;
        return r595138;
}
↓
double f(double x, double y, double z) {
        double r595139 = x;
        double r595140 = y;
        double r595141 = r595139 * r595140;
        double r595142 = -1.926622627642984e+158;
        bool r595143 = r595141 <= r595142;
        double r595144 = z;
        double r595145 = r595140 / r595144;
        double r595146 = r595139 * r595145;
        double r595147 = -1.2477594496210908e-277;
        bool r595148 = r595141 <= r595147;
        double r595149 = 1.1375082887988885e-219;
        bool r595150 = r595141 <= r595149;
        double r595151 = !r595150;
        bool r595152 = r595148 || r595151;
        double r595153 = 1.0;
        double r595154 = r595153 / r595144;
        double r595155 = r595141 * r595154;
        double r595156 = r595144 / r595139;
        double r595157 = r595140 / r595156;
        double r595158 = r595152 ? r595155 : r595157;
        double r595159 = r595143 ? r595146 : r595158;
        return r595159;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original6.2
Target6.0
Herbie1.9
\[\begin{array}{l} \mathbf{if}\;z \lt -4.262230790519428958560619200129306371776 \cdot 10^{-138}:\\ \;\;\;\;\frac{x \cdot y}{z}\\ \mathbf{elif}\;z \lt 1.704213066065047207696571404603247573308 \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) < -1.926622627642984e+158

    1. Initial program 20.0

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

    3. Applied *-un-lft-identity20.0

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

    4. Applied times-frac2.1

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

    5. Simplified2.1

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

    if -1.926622627642984e+158 < (* x y) < -1.2477594496210908e-277 or 1.1375082887988885e-219 < (* x y)

    1. Initial program 2.3

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

    3. Applied div-inv2.4

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

    if -1.2477594496210908e-277 < (* x y) < 1.1375082887988885e-219

    1. Initial program 13.6

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

    3. Applied clear-num14.0

      \[\leadsto \color{blue}{\frac{1}{\frac{z}{x \cdot y}}}\]
    4. Using strategy rm

    5. Applied add-cube-cbrt14.0

      \[\leadsto \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{\frac{z}{x \cdot y}}\]

    6. Applied associate-/l*14.0

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

    7. Simplified14.0

      \[\leadsto \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\color{blue}{\frac{z}{y \cdot x}}}\]
    8. Using strategy rm

    9. Applied *-un-lft-identity14.0

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

    10. Applied times-frac1.1

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

    11. Applied associate-/r*0.4

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

    12. Simplified0.3

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

  4. Final simplification1.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \le -1.926622627642983907222823390598358692722 \cdot 10^{158}:\\ \;\;\;\;x \cdot \frac{y}{z}\\ \mathbf{elif}\;x \cdot y \le -1.247759449621090803465755159668841719159 \cdot 10^{-277} \lor \neg \left(x \cdot y \le 1.137508288798888459719974341598011528755 \cdot 10^{-219}\right):\\ \;\;\;\;\left(x \cdot y\right) \cdot \frac{1}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{\frac{z}{x}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019212 
(FPCore (x y z)
  :name "Diagrams.Solve.Tridiagonal:solveCyclicTriDiagonal from diagrams-solve-0.1, A"
  :precision binary64

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

  (/ (* x y) z))