Linear.Quaternion:$ctanh from linear-1.19.1.3

Average Error: 2.7 → 3.0

Time: 6.2s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z) {
        double r558391 = x;
        double r558392 = y;
        double r558393 = sin(r558392);
        double r558394 = r558393 / r558392;
        double r558395 = r558391 * r558394;
        double r558396 = z;
        double r558397 = r558395 / r558396;
        return r558397;
}

↓

double f(double x, double y, double z) {
        double r558398 = y;
        double r558399 = sin(r558398);
        double r558400 = r558399 / r558398;
        double r558401 = z;
        double r558402 = x;
        double r558403 = r558401 / r558402;
        double r558404 = r558400 / r558403;
        return r558404;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	2.7
Target	0.3
Herbie	3.0

\[\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. Initial program 2.7

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

3. Applied pow1 2.7

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

4. Applied pow1 2.7

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

5. Applied pow-prod-down 2.7

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

7. Applied clear-num 3.2

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

8. Simplified 3.3

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

10. Applied *-un-lft-identity 3.3

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

11. Applied *-un-lft-identity 3.3

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

12. Applied times-frac 3.3

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

13. Applied *-un-lft-identity 3.3

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

14. Applied *-un-lft-identity 3.3

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

15. Applied times-frac 3.3

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

16. Applied times-frac 3.3

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

17. Applied add-sqr-sqrt 3.3

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

18. Applied times-frac 3.3

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

19. Simplified 3.3

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

20. Simplified 3.0

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

21. Final simplification 3.0

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

Reproduce

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

  :herbie-target
  (if (< z -4.2173720203427147e-29) (/ (* x (/ 1 (/ y (sin y)))) z) (if (< z 4.446702369113811e+64) (/ x (* z (/ y (sin y)))) (/ (* x (/ 1 (/ y (sin y)))) z)))

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