Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B

Average Error: 5.7 → 0.5

Time: 26.5s

Precision: 64

Math

\[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

↓

\[\begin{array}{l} \mathbf{if}\;z \cdot \left(\left(0.0007936500793651 + y\right) \cdot z - 0.0027777777777778\right) \le -1.61040270274943 \cdot 10^{+287}:\\ \;\;\;\;\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467\right) + \left(\frac{z}{\frac{x}{z}} \cdot \left(0.0007936500793651 + y\right) - \frac{z}{x} \cdot 0.0027777777777778\right)\\ \mathbf{elif}\;z \cdot \left(\left(0.0007936500793651 + y\right) \cdot z - 0.0027777777777778\right) \le 130.85740699996094:\\ \;\;\;\;\frac{0.083333333333333 + z \cdot \left(\left(0.0007936500793651 + y\right) \cdot z - 0.0027777777777778\right)}{x} + \left(0.91893853320467 + \left(\left(\sqrt{\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)} \cdot \sqrt{\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)} - x\right) + \log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467\right) + \left(\frac{z}{\frac{x}{z}} \cdot \left(0.0007936500793651 + y\right) - \frac{z}{x} \cdot 0.0027777777777778\right)\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r21523059 = x;
        double r21523060 = 0.5;
        double r21523061 = r21523059 - r21523060;
        double r21523062 = log(r21523059);
        double r21523063 = r21523061 * r21523062;
        double r21523064 = r21523063 - r21523059;
        double r21523065 = 0.91893853320467;
        double r21523066 = r21523064 + r21523065;
        double r21523067 = y;
        double r21523068 = 0.0007936500793651;
        double r21523069 = r21523067 + r21523068;
        double r21523070 = z;
        double r21523071 = r21523069 * r21523070;
        double r21523072 = 0.0027777777777778;
        double r21523073 = r21523071 - r21523072;
        double r21523074 = r21523073 * r21523070;
        double r21523075 = 0.083333333333333;
        double r21523076 = r21523074 + r21523075;
        double r21523077 = r21523076 / r21523059;
        double r21523078 = r21523066 + r21523077;
        return r21523078;
}

↓

double f(double x, double y, double z) {
        double r21523079 = z;
        double r21523080 = 0.0007936500793651;
        double r21523081 = y;
        double r21523082 = r21523080 + r21523081;
        double r21523083 = r21523082 * r21523079;
        double r21523084 = 0.0027777777777778;
        double r21523085 = r21523083 - r21523084;
        double r21523086 = r21523079 * r21523085;
        double r21523087 = -1.61040270274943e+287;
        bool r21523088 = r21523086 <= r21523087;
        double r21523089 = x;
        double r21523090 = sqrt(r21523089);
        double r21523091 = log(r21523090);
        double r21523092 = 0.5;
        double r21523093 = r21523089 - r21523092;
        double r21523094 = r21523091 * r21523093;
        double r21523095 = r21523094 - r21523089;
        double r21523096 = r21523094 + r21523095;
        double r21523097 = 0.91893853320467;
        double r21523098 = r21523096 + r21523097;
        double r21523099 = r21523089 / r21523079;
        double r21523100 = r21523079 / r21523099;
        double r21523101 = r21523100 * r21523082;
        double r21523102 = r21523079 / r21523089;
        double r21523103 = r21523102 * r21523084;
        double r21523104 = r21523101 - r21523103;
        double r21523105 = r21523098 + r21523104;
        double r21523106 = 130.85740699996094;
        bool r21523107 = r21523086 <= r21523106;
        double r21523108 = 0.083333333333333;
        double r21523109 = r21523108 + r21523086;
        double r21523110 = r21523109 / r21523089;
        double r21523111 = sqrt(r21523094);
        double r21523112 = r21523111 * r21523111;
        double r21523113 = r21523112 - r21523089;
        double r21523114 = r21523113 + r21523094;
        double r21523115 = r21523097 + r21523114;
        double r21523116 = r21523110 + r21523115;
        double r21523117 = r21523107 ? r21523116 : r21523105;
        double r21523118 = r21523088 ? r21523105 : r21523117;
        return r21523118;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.7
Target	1.2
Herbie	0.5

\[\left(\left(\left(x - 0.5\right) \cdot \log x + \left(0.91893853320467 - x\right)\right) + \frac{0.083333333333333}{x}\right) + \frac{z}{x} \cdot \left(z \cdot \left(y + 0.0007936500793651\right) - 0.0027777777777778\right)\]

Derivation

1. Split input into 2 regimes

2. if (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) < -1.61040270274943e+287 or 130.85740699996094 < (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z)

   1. Initial program 18.6

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 18.6

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   4. Applied log-prod 18.6

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt{x}\right) + \log \left(\sqrt{x}\right)\right)} - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   5. Applied distribute-rgt-in 18.6

      \[\leadsto \left(\left(\color{blue}{\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)\right)} - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   6. Applied associate--l+ 18.7

      \[\leadsto \left(\color{blue}{\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right)} + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   7. Taylor expanded around inf 19.4

      \[\leadsto \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467\right) + \color{blue}{\left(\left(0.0007936500793651 \cdot \frac{{z}^{2}}{x} + \frac{{z}^{2} \cdot y}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)}\]

   8. Simplified 1.0

      \[\leadsto \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467\right) + \color{blue}{\left(\frac{z}{\frac{x}{z}} \cdot \left(0.0007936500793651 + y\right) - \frac{z}{x} \cdot 0.0027777777777778\right)}\]

   if -1.61040270274943e+287 < (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) < 130.85740699996094

   1. Initial program 0.2

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]
   2. Using strategy rm

   3. Applied add-sqr-sqrt 0.2

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)} - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   4. Applied log-prod 0.2

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt{x}\right) + \log \left(\sqrt{x}\right)\right)} - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   5. Applied distribute-rgt-in 0.2

      \[\leadsto \left(\left(\color{blue}{\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)\right)} - x\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   6. Applied associate--l+ 0.2

      \[\leadsto \left(\color{blue}{\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right)} + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]
   7. Using strategy rm

   8. Applied add-sqr-sqrt 0.3

      \[\leadsto \left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\color{blue}{\sqrt{\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)} \cdot \sqrt{\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)}} - x\right)\right) + 0.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot \left(\left(0.0007936500793651 + y\right) \cdot z - 0.0027777777777778\right) \le -1.61040270274943 \cdot 10^{+287}:\\ \;\;\;\;\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467\right) + \left(\frac{z}{\frac{x}{z}} \cdot \left(0.0007936500793651 + y\right) - \frac{z}{x} \cdot 0.0027777777777778\right)\\ \mathbf{elif}\;z \cdot \left(\left(0.0007936500793651 + y\right) \cdot z - 0.0027777777777778\right) \le 130.85740699996094:\\ \;\;\;\;\frac{0.083333333333333 + z \cdot \left(\left(0.0007936500793651 + y\right) \cdot z - 0.0027777777777778\right)}{x} + \left(0.91893853320467 + \left(\left(\sqrt{\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)} \cdot \sqrt{\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)} - x\right) + \log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt{x}\right) \cdot \left(x - 0.5\right) - x\right)\right) + 0.91893853320467\right) + \left(\frac{z}{\frac{x}{z}} \cdot \left(0.0007936500793651 + y\right) - \frac{z}{x} \cdot 0.0027777777777778\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019163 
(FPCore (x y z)
  :name "Numeric.SpecFunctions:$slogFactorial from math-functions-0.1.5.2, B"

  :herbie-target
  (+ (+ (+ (* (- x 0.5) (log x)) (- 0.91893853320467 x)) (/ 0.083333333333333 x)) (* (/ z x) (- (* z (+ y 0.0007936500793651)) 0.0027777777777778)))

  (+ (+ (- (* (- x 0.5) (log x)) x) 0.91893853320467) (/ (+ (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) 0.083333333333333) x)))