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

Average Error: 5.7 → 4.1

Time: 39.5s

Precision: 64

Math

\[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

↓

\[\begin{array}{l} \mathbf{if}\;\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z \le -2.23958461877665325 \cdot 10^{132} \lor \neg \left(\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z \le 1.19416898135989124 \cdot 10^{308}\right):\\ \;\;\;\;\left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right) + 0.91893853320467001\right) + \left(\frac{{z}^{2}}{x} \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(0.91893853320467001 + \left(\left(0.5 \cdot \left(-\log x\right) - x\right) + \left(\sqrt{x} \cdot \log x\right) \cdot \sqrt{x}\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r318022 = x;
        double r318023 = 0.5;
        double r318024 = r318022 - r318023;
        double r318025 = log(r318022);
        double r318026 = r318024 * r318025;
        double r318027 = r318026 - r318022;
        double r318028 = 0.91893853320467;
        double r318029 = r318027 + r318028;
        double r318030 = y;
        double r318031 = 0.0007936500793651;
        double r318032 = r318030 + r318031;
        double r318033 = z;
        double r318034 = r318032 * r318033;
        double r318035 = 0.0027777777777778;
        double r318036 = r318034 - r318035;
        double r318037 = r318036 * r318033;
        double r318038 = 0.083333333333333;
        double r318039 = r318037 + r318038;
        double r318040 = r318039 / r318022;
        double r318041 = r318029 + r318040;
        return r318041;
}

↓

double f(double x, double y, double z) {
        double r318042 = y;
        double r318043 = 0.0007936500793651;
        double r318044 = r318042 + r318043;
        double r318045 = z;
        double r318046 = r318044 * r318045;
        double r318047 = 0.0027777777777778;
        double r318048 = r318046 - r318047;
        double r318049 = r318048 * r318045;
        double r318050 = -2.2395846187766533e+132;
        bool r318051 = r318049 <= r318050;
        double r318052 = 1.1941689813598912e+308;
        bool r318053 = r318049 <= r318052;
        double r318054 = !r318053;
        bool r318055 = r318051 || r318054;
        double r318056 = x;
        double r318057 = cbrt(r318056);
        double r318058 = r318057 * r318057;
        double r318059 = log(r318058);
        double r318060 = 0.5;
        double r318061 = r318056 - r318060;
        double r318062 = r318059 * r318061;
        double r318063 = log(r318057);
        double r318064 = r318061 * r318063;
        double r318065 = r318064 - r318056;
        double r318066 = r318062 + r318065;
        double r318067 = 0.91893853320467;
        double r318068 = r318066 + r318067;
        double r318069 = 2.0;
        double r318070 = pow(r318045, r318069);
        double r318071 = r318070 / r318056;
        double r318072 = r318071 * r318044;
        double r318073 = r318045 / r318056;
        double r318074 = r318047 * r318073;
        double r318075 = r318072 - r318074;
        double r318076 = r318068 + r318075;
        double r318077 = log(r318056);
        double r318078 = -r318077;
        double r318079 = r318060 * r318078;
        double r318080 = r318079 - r318056;
        double r318081 = sqrt(r318056);
        double r318082 = r318081 * r318077;
        double r318083 = r318082 * r318081;
        double r318084 = r318080 + r318083;
        double r318085 = r318067 + r318084;
        double r318086 = 0.083333333333333;
        double r318087 = r318049 + r318086;
        double r318088 = r318087 / r318056;
        double r318089 = r318085 + r318088;
        double r318090 = r318055 ? r318076 : r318089;
        return r318090;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.7
Target	1.2
Herbie	4.1

\[\left(\left(\left(x - 0.5\right) \cdot \log x + \left(0.91893853320467001 - x\right)\right) + \frac{0.0833333333333329956}{x}\right) + \frac{z}{x} \cdot \left(z \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778\right)\]

Derivation

1. Split input into 2 regimes

2. if (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) < -2.2395846187766533e+132 or 1.1941689813598912e+308 < (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z)

   1. Initial program 45.5

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 45.5

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \color{blue}{\left(\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   4. Applied log-prod 45.5

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \log \left(\sqrt[3]{x}\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   5. Applied distribute-rgt-in 45.5

      \[\leadsto \left(\left(\color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right)\right)} - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   6. Applied associate--l+ 45.5

      \[\leadsto \left(\color{blue}{\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\log \left(\sqrt[3]{x}\right) \cdot \left(x - 0.5\right) - x\right)\right)} + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   7. Simplified 45.5

      \[\leadsto \left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)}\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   8. Taylor expanded around inf 45.5

      \[\leadsto \left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right) + 0.91893853320467001\right) + \color{blue}{\left(\left(7.93650079365100015 \cdot 10^{-4} \cdot \frac{{z}^{2}}{x} + \frac{{z}^{2} \cdot y}{x}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)}\]

   9. Simplified 31.4

      \[\leadsto \left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right) + 0.91893853320467001\right) + \color{blue}{\left(\frac{{z}^{2}}{x} \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)}\]

   if -2.2395846187766533e+132 < (* (- (* (+ y 0.0007936500793651) z) 0.0027777777777778) z) < 1.1941689813598912e+308

   1. Initial program 0.2

      \[\left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467001\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   2. Taylor expanded around inf 0.2

      \[\leadsto \color{blue}{\left(\left(0.5 \cdot \log \left(\frac{1}{x}\right) + 0.91893853320467001\right) - \left(x + x \cdot \log \left(\frac{1}{x}\right)\right)\right)} + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   3. Simplified 0.2

      \[\leadsto \color{blue}{\left(0.91893853320467001 + \left(\left(0.5 \cdot \left(-\log x\right) - x\right) + \log x \cdot x\right)\right)} + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
   4. Using strategy rm

   5. Applied add-sqr-sqrt 0.4

      \[\leadsto \left(0.91893853320467001 + \left(\left(0.5 \cdot \left(-\log x\right) - x\right) + \log x \cdot \color{blue}{\left(\sqrt{x} \cdot \sqrt{x}\right)}\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   6. Applied associate-*r* 0.4

      \[\leadsto \left(0.91893853320467001 + \left(\left(0.5 \cdot \left(-\log x\right) - x\right) + \color{blue}{\left(\log x \cdot \sqrt{x}\right) \cdot \sqrt{x}}\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]

   7. Simplified 0.4

      \[\leadsto \left(0.91893853320467001 + \left(\left(0.5 \cdot \left(-\log x\right) - x\right) + \color{blue}{\left(\sqrt{x} \cdot \log x\right)} \cdot \sqrt{x}\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\]
3. Recombined 2 regimes into one program.

4. Final simplification 4.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z \le -2.23958461877665325 \cdot 10^{132} \lor \neg \left(\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z \le 1.19416898135989124 \cdot 10^{308}\right):\\ \;\;\;\;\left(\left(\log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right) + 0.91893853320467001\right) + \left(\frac{{z}^{2}}{x} \cdot \left(y + 7.93650079365100015 \cdot 10^{-4}\right) - 0.0027777777777778 \cdot \frac{z}{x}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(0.91893853320467001 + \left(\left(0.5 \cdot \left(-\log x\right) - x\right) + \left(\sqrt{x} \cdot \log x\right) \cdot \sqrt{x}\right)\right) + \frac{\left(\left(y + 7.93650079365100015 \cdot 10^{-4}\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.0833333333333329956}{x}\\ \end{array}\]

Reproduce

herbie shell --seed 2019199 
(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)))