Linear.Quaternion:$ctanh from linear-1.19.1.3

Average Error: 2.7 → 3.0

Time: 6.6s

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 r499182 = x;
        double r499183 = y;
        double r499184 = sin(r499183);
        double r499185 = r499184 / r499183;
        double r499186 = r499182 * r499185;
        double r499187 = z;
        double r499188 = r499186 / r499187;
        return r499188;
}

↓

double f(double x, double y, double z) {
        double r499189 = y;
        double r499190 = sin(r499189);
        double r499191 = r499190 / r499189;
        double r499192 = z;
        double r499193 = x;
        double r499194 = r499192 / r499193;
        double r499195 = r499191 / r499194;
        return r499195;
}

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 +o rules:numerics
(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))