Average Error: 2.6 → 0.3
Time: 20.8s
Precision: 64
\[\frac{x \cdot \frac{\sin y}{y}}{z}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \cdot \frac{\sin y}{y} \le -5.896648462014593463455576898766456041476 \cdot 10^{-216} \lor \neg \left(x \cdot \frac{\sin y}{y} \le 2.194855497661910616106210683903194501758 \cdot 10^{-180}\right):\\ \;\;\;\;\frac{\frac{x}{\frac{y}{\sin y}}}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{y}{\frac{\sin y}{z}}}\\ \end{array}\]
\frac{x \cdot \frac{\sin y}{y}}{z}
↓
\begin{array}{l}
\mathbf{if}\;x \cdot \frac{\sin y}{y} \le -5.896648462014593463455576898766456041476 \cdot 10^{-216} \lor \neg \left(x \cdot \frac{\sin y}{y} \le 2.194855497661910616106210683903194501758 \cdot 10^{-180}\right):\\
\;\;\;\;\frac{\frac{x}{\frac{y}{\sin y}}}{z}\\

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

\end{array}
double f(double x, double y, double z) {
        double r379199 = x;
        double r379200 = y;
        double r379201 = sin(r379200);
        double r379202 = r379201 / r379200;
        double r379203 = r379199 * r379202;
        double r379204 = z;
        double r379205 = r379203 / r379204;
        return r379205;
}
↓
double f(double x, double y, double z) {
        double r379206 = x;
        double r379207 = y;
        double r379208 = sin(r379207);
        double r379209 = r379208 / r379207;
        double r379210 = r379206 * r379209;
        double r379211 = -5.896648462014593e-216;
        bool r379212 = r379210 <= r379211;
        double r379213 = 2.1948554976619106e-180;
        bool r379214 = r379210 <= r379213;
        double r379215 = !r379214;
        bool r379216 = r379212 || r379215;
        double r379217 = r379207 / r379208;
        double r379218 = r379206 / r379217;
        double r379219 = z;
        double r379220 = r379218 / r379219;
        double r379221 = r379208 / r379219;
        double r379222 = r379207 / r379221;
        double r379223 = r379206 / r379222;
        double r379224 = r379216 ? r379220 : r379223;
        return r379224;
}

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

Original2.6
Target0.3
Herbie0.3
\[\begin{array}{l} \mathbf{if}\;z \lt -4.217372020342714661850238929213415773451 \cdot 10^{-29}:\\ \;\;\;\;\frac{x \cdot \frac{1}{\frac{y}{\sin y}}}{z}\\ \mathbf{elif}\;z \lt 4.446702369113811028051510715777703865332 \cdot 10^{64}:\\ \;\;\;\;\frac{x}{z \cdot \frac{y}{\sin y}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot \frac{1}{\frac{y}{\sin y}}}{z}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if (* x (/ (sin y) y)) < -5.896648462014593e-216 or 2.1948554976619106e-180 < (* x (/ (sin y) y))

    1. Initial program 0.2

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

    3. Applied clear-num0.2

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

    5. Applied pow10.2

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

    6. Applied pow10.2

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

    7. Applied pow-prod-down0.2

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

    8. Simplified0.2

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

    if -5.896648462014593e-216 < (* x (/ (sin y) y)) < 2.1948554976619106e-180

    1. Initial program 7.8

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

    3. Applied associate-/l*0.3

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

    4. Simplified0.5

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

  4. Final simplification0.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot \frac{\sin y}{y} \le -5.896648462014593463455576898766456041476 \cdot 10^{-216} \lor \neg \left(x \cdot \frac{\sin y}{y} \le 2.194855497661910616106210683903194501758 \cdot 10^{-180}\right):\\ \;\;\;\;\frac{\frac{x}{\frac{y}{\sin y}}}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{\frac{y}{\frac{\sin y}{z}}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019304 
(FPCore (x y z)
  :name "Linear.Quaternion:$ctanh from linear-1.19.1.3"
  :precision binary64

  :herbie-target
  (if (< z -4.21737202034271466e-29) (/ (* x (/ 1 (/ y (sin y)))) z) (if (< z 4.44670236911381103e64) (/ x (* z (/ y (sin y)))) (/ (* x (/ 1 (/ y (sin y)))) z)))

  (/ (* x (/ (sin y) y)) z))