Data.HashTable.ST.Basic:computeOverhead from hashtables-1.2.0.2

Average Error: 8.9 → 0.1

Time: 22.1s

Precision: 64

Math

\[\frac{x}{y} + \frac{2.0 + \left(z \cdot 2.0\right) \cdot \left(1.0 - t\right)}{t \cdot z}\]

↓

\[\frac{x}{y} + \left(\left(\frac{\sqrt{\sqrt{2.0}}}{\frac{t}{\frac{\sqrt{2.0}}{z}}} \cdot \sqrt{\sqrt{2.0}} + \frac{2.0}{t}\right) - 2.0\right)\]

C

double f(double x, double y, double z, double t) {
        double r40518968 = x;
        double r40518969 = y;
        double r40518970 = r40518968 / r40518969;
        double r40518971 = 2.0;
        double r40518972 = z;
        double r40518973 = r40518972 * r40518971;
        double r40518974 = 1.0;
        double r40518975 = t;
        double r40518976 = r40518974 - r40518975;
        double r40518977 = r40518973 * r40518976;
        double r40518978 = r40518971 + r40518977;
        double r40518979 = r40518975 * r40518972;
        double r40518980 = r40518978 / r40518979;
        double r40518981 = r40518970 + r40518980;
        return r40518981;
}

↓

double f(double x, double y, double z, double t) {
        double r40518982 = x;
        double r40518983 = y;
        double r40518984 = r40518982 / r40518983;
        double r40518985 = 2.0;
        double r40518986 = sqrt(r40518985);
        double r40518987 = sqrt(r40518986);
        double r40518988 = t;
        double r40518989 = z;
        double r40518990 = r40518986 / r40518989;
        double r40518991 = r40518988 / r40518990;
        double r40518992 = r40518987 / r40518991;
        double r40518993 = r40518992 * r40518987;
        double r40518994 = r40518985 / r40518988;
        double r40518995 = r40518993 + r40518994;
        double r40518996 = r40518995 - r40518985;
        double r40518997 = r40518984 + r40518996;
        return r40518997;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	8.9
Target	0.1
Herbie	0.1

\[\frac{\frac{2.0}{z} + 2.0}{t} - \left(2.0 - \frac{x}{y}\right)\]

Derivation

1. Initial program 8.9

   \[\frac{x}{y} + \frac{2.0 + \left(z \cdot 2.0\right) \cdot \left(1.0 - t\right)}{t \cdot z}\]

2. Taylor expanded around 0 0.1

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

3. Simplified 0.1

   \[\leadsto \frac{x}{y} + \color{blue}{\left(\frac{2.0}{z \cdot t} + \left(\frac{2.0}{t} - 2.0\right)\right)}\]

4. Taylor expanded around 0 0.1

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

5. Simplified 0.1

   \[\leadsto \frac{x}{y} + \color{blue}{\left(\left(\frac{2.0}{t} + \frac{\frac{2.0}{z}}{t}\right) - 2.0\right)}\]
6. Using strategy rm

7. Applied *-un-lft-identity 0.1

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

8. Applied add-sqr-sqrt 0.3

   \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\color{blue}{\sqrt{2.0} \cdot \sqrt{2.0}}}{1 \cdot z}}{t}\right) - 2.0\right)\]

9. Applied times-frac 0.2

   \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\color{blue}{\frac{\sqrt{2.0}}{1} \cdot \frac{\sqrt{2.0}}{z}}}{t}\right) - 2.0\right)\]

10. Applied associate-/l* 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \color{blue}{\frac{\frac{\sqrt{2.0}}{1}}{\frac{t}{\frac{\sqrt{2.0}}{z}}}}\right) - 2.0\right)\]
11. Using strategy rm

12. Applied *-un-lft-identity 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{2.0}}{1}}{\frac{t}{\frac{\sqrt{2.0}}{\color{blue}{1 \cdot z}}}}\right) - 2.0\right)\]

13. Applied *-un-lft-identity 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{2.0}}{1}}{\frac{t}{\frac{\color{blue}{1 \cdot \sqrt{2.0}}}{1 \cdot z}}}\right) - 2.0\right)\]

14. Applied times-frac 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{2.0}}{1}}{\frac{t}{\color{blue}{\frac{1}{1} \cdot \frac{\sqrt{2.0}}{z}}}}\right) - 2.0\right)\]

15. Applied *-un-lft-identity 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{2.0}}{1}}{\frac{\color{blue}{1 \cdot t}}{\frac{1}{1} \cdot \frac{\sqrt{2.0}}{z}}}\right) - 2.0\right)\]

16. Applied times-frac 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{2.0}}{1}}{\color{blue}{\frac{1}{\frac{1}{1}} \cdot \frac{t}{\frac{\sqrt{2.0}}{z}}}}\right) - 2.0\right)\]

17. Applied add-sqr-sqrt 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{2.0}}{\color{blue}{\sqrt{1} \cdot \sqrt{1}}}}{\frac{1}{\frac{1}{1}} \cdot \frac{t}{\frac{\sqrt{2.0}}{z}}}\right) - 2.0\right)\]

18. Applied add-sqr-sqrt 0.2

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\sqrt{\color{blue}{\sqrt{2.0} \cdot \sqrt{2.0}}}}{\sqrt{1} \cdot \sqrt{1}}}{\frac{1}{\frac{1}{1}} \cdot \frac{t}{\frac{\sqrt{2.0}}{z}}}\right) - 2.0\right)\]

19. Applied sqrt-prod 0.1

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\frac{\color{blue}{\sqrt{\sqrt{2.0}} \cdot \sqrt{\sqrt{2.0}}}}{\sqrt{1} \cdot \sqrt{1}}}{\frac{1}{\frac{1}{1}} \cdot \frac{t}{\frac{\sqrt{2.0}}{z}}}\right) - 2.0\right)\]

20. Applied times-frac 0.1

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \frac{\color{blue}{\frac{\sqrt{\sqrt{2.0}}}{\sqrt{1}} \cdot \frac{\sqrt{\sqrt{2.0}}}{\sqrt{1}}}}{\frac{1}{\frac{1}{1}} \cdot \frac{t}{\frac{\sqrt{2.0}}{z}}}\right) - 2.0\right)\]

21. Applied times-frac 0.1

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \color{blue}{\frac{\frac{\sqrt{\sqrt{2.0}}}{\sqrt{1}}}{\frac{1}{\frac{1}{1}}} \cdot \frac{\frac{\sqrt{\sqrt{2.0}}}{\sqrt{1}}}{\frac{t}{\frac{\sqrt{2.0}}{z}}}}\right) - 2.0\right)\]

22. Simplified 0.1

    \[\leadsto \frac{x}{y} + \left(\left(\frac{2.0}{t} + \color{blue}{\frac{\sqrt{\sqrt{2.0}}}{\sqrt{1}}} \cdot \frac{\frac{\sqrt{\sqrt{2.0}}}{\sqrt{1}}}{\frac{t}{\frac{\sqrt{2.0}}{z}}}\right) - 2.0\right)\]

23. Final simplification 0.1

    \[\leadsto \frac{x}{y} + \left(\left(\frac{\sqrt{\sqrt{2.0}}}{\frac{t}{\frac{\sqrt{2.0}}{z}}} \cdot \sqrt{\sqrt{2.0}} + \frac{2.0}{t}\right) - 2.0\right)\]

Reproduce

herbie shell --seed 2019158 
(FPCore (x y z t)
  :name "Data.HashTable.ST.Basic:computeOverhead from hashtables-1.2.0.2"

  :herbie-target
  (- (/ (+ (/ 2.0 z) 2.0) t) (- 2.0 (/ x y)))

  (+ (/ x y) (/ (+ 2.0 (* (* z 2.0) (- 1.0 t))) (* t z))))