Random Jason Timeout Test 002

Average Error: 0.0 → 0.3

Time: 4.3s

Precision: 64

• could not determine a ground truth for program body

  1. c = 1.0551194375545526e+290

Math

\[\left(\left(\sinh c\right) \bmod \left(c - {\left( -2.98073076018121927 \cdot 10^{165} \right)}^{2}\right)\right)\]

↓

\[\left(\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\sinh c\right)\right)\right) \bmod \left(c - {\left( -2.98073076018121927 \cdot 10^{165} \right)}^{2}\right)\right)\]

C

double f(double c) {
        double r20059 = c;
        double r20060 = sinh(r20059);
        double r20061 = -2.9807307601812193e+165;
        double r20062 = 2.0;
        double r20063 = pow(r20061, r20062);
        double r20064 = r20059 - r20063;
        double r20065 = fmod(r20060, r20064);
        return r20065;
}

↓

double f(double c) {
        double r20066 = c;
        double r20067 = sinh(r20066);
        double r20068 = log1p(r20067);
        double r20069 = expm1(r20068);
        double r20070 = -2.9807307601812193e+165;
        double r20071 = 2.0;
        double r20072 = pow(r20070, r20071);
        double r20073 = r20066 - r20072;
        double r20074 = fmod(r20069, r20073);
        return r20074;
}

Error

Bits error versus c

Derivation

1. Initial program 0.0

   \[\left(\left(\sinh c\right) \bmod \left(c - {\left( -2.98073076018121927 \cdot 10^{165} \right)}^{2}\right)\right)\]
2. Using strategy rm

3. Applied expm1-log1p-u 0.3

   \[\leadsto \left(\color{blue}{\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\sinh c\right)\right)\right)} \bmod \left(c - {\left( -2.98073076018121927 \cdot 10^{165} \right)}^{2}\right)\right)\]

4. Final simplification 0.3

   \[\leadsto \left(\left(\mathsf{expm1}\left(\mathsf{log1p}\left(\sinh c\right)\right)\right) \bmod \left(c - {\left( -2.98073076018121927 \cdot 10^{165} \right)}^{2}\right)\right)\]

Reproduce

herbie shell --seed 2020060 +o rules:numerics
(FPCore (c)
  :name "Random Jason Timeout Test 002"
  :precision binary64
  (fmod (sinh c) (- c (pow -2.9807307601812193e+165 2))))