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

Average Error: 5.3 → 3.3

Time: 19.6s

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}\;x \le 1.1968875348652573 \cdot 10^{+130}:\\ \;\;\;\;\frac{z \cdot \left(z \cdot \left(y + 0.0007936500793651\right) - 0.0027777777777778\right) + 0.083333333333333}{x} + \sqrt{0.91893853320467 + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right)\right) - x\right)} \cdot \sqrt{\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right) + \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right)\right) + 0.91893853320467\right) + \frac{1}{x \cdot \left(z \cdot 0.4000000000000064 - 0.10095227809524161 \cdot \left(z \cdot z\right)\right) + x \cdot 12.000000000000048}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r9071303 = x;
        double r9071304 = 0.5;
        double r9071305 = r9071303 - r9071304;
        double r9071306 = log(r9071303);
        double r9071307 = r9071305 * r9071306;
        double r9071308 = r9071307 - r9071303;
        double r9071309 = 0.91893853320467;
        double r9071310 = r9071308 + r9071309;
        double r9071311 = y;
        double r9071312 = 0.0007936500793651;
        double r9071313 = r9071311 + r9071312;
        double r9071314 = z;
        double r9071315 = r9071313 * r9071314;
        double r9071316 = 0.0027777777777778;
        double r9071317 = r9071315 - r9071316;
        double r9071318 = r9071317 * r9071314;
        double r9071319 = 0.083333333333333;
        double r9071320 = r9071318 + r9071319;
        double r9071321 = r9071320 / r9071303;
        double r9071322 = r9071310 + r9071321;
        return r9071322;
}

↓

double f(double x, double y, double z) {
        double r9071323 = x;
        double r9071324 = 1.1968875348652573e+130;
        bool r9071325 = r9071323 <= r9071324;
        double r9071326 = z;
        double r9071327 = y;
        double r9071328 = 0.0007936500793651;
        double r9071329 = r9071327 + r9071328;
        double r9071330 = r9071326 * r9071329;
        double r9071331 = 0.0027777777777778;
        double r9071332 = r9071330 - r9071331;
        double r9071333 = r9071326 * r9071332;
        double r9071334 = 0.083333333333333;
        double r9071335 = r9071333 + r9071334;
        double r9071336 = r9071335 / r9071323;
        double r9071337 = 0.91893853320467;
        double r9071338 = 0.5;
        double r9071339 = r9071323 - r9071338;
        double r9071340 = cbrt(r9071323);
        double r9071341 = log(r9071340);
        double r9071342 = r9071339 * r9071341;
        double r9071343 = r9071342 + r9071342;
        double r9071344 = r9071342 + r9071343;
        double r9071345 = r9071344 - r9071323;
        double r9071346 = r9071337 + r9071345;
        double r9071347 = sqrt(r9071346);
        double r9071348 = log(r9071323);
        double r9071349 = r9071339 * r9071348;
        double r9071350 = r9071349 - r9071323;
        double r9071351 = r9071350 + r9071337;
        double r9071352 = sqrt(r9071351);
        double r9071353 = r9071347 * r9071352;
        double r9071354 = r9071336 + r9071353;
        double r9071355 = r9071342 - r9071323;
        double r9071356 = r9071340 * r9071340;
        double r9071357 = log(r9071356);
        double r9071358 = r9071357 * r9071339;
        double r9071359 = r9071355 + r9071358;
        double r9071360 = r9071359 + r9071337;
        double r9071361 = 1.0;
        double r9071362 = 0.4000000000000064;
        double r9071363 = r9071326 * r9071362;
        double r9071364 = 0.10095227809524161;
        double r9071365 = r9071326 * r9071326;
        double r9071366 = r9071364 * r9071365;
        double r9071367 = r9071363 - r9071366;
        double r9071368 = r9071323 * r9071367;
        double r9071369 = 12.000000000000048;
        double r9071370 = r9071323 * r9071369;
        double r9071371 = r9071368 + r9071370;
        double r9071372 = r9071361 / r9071371;
        double r9071373 = r9071360 + r9071372;
        double r9071374 = r9071325 ? r9071354 : r9071373;
        return r9071374;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	5.3
Target	1.2
Herbie	3.3

\[\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 x < 1.1968875348652573e+130

   1. Initial program 1.7

      \[\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 1.8

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

   5. Applied add-cube-cbrt 1.8

      \[\leadsto \sqrt{\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467} \cdot \sqrt{\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.91893853320467} + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   6. Applied log-prod 1.8

      \[\leadsto \sqrt{\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467} \cdot \sqrt{\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.91893853320467} + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   7. Applied distribute-lft-in 1.8

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

   8. Simplified 1.8

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

   if 1.1968875348652573e+130 < x

   1. Initial program 12.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-cube-cbrt 12.2

      \[\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.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   4. Applied log-prod 12.3

      \[\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.91893853320467\right) + \frac{\left(\left(y + 0.0007936500793651\right) \cdot z - 0.0027777777777778\right) \cdot z + 0.083333333333333}{x}\]

   5. Applied distribute-lft-in 12.3

      \[\leadsto \left(\left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{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}\]

   6. Applied associate--l+ 12.2

      \[\leadsto \left(\color{blue}{\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\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 clear-num 12.2

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

   9. Taylor expanded around 0 11.1

      \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right) + 0.91893853320467\right) + \frac{1}{\color{blue}{\left(12.000000000000048 \cdot x + 0.4000000000000064 \cdot \left(x \cdot z\right)\right) - 0.10095227809524161 \cdot \left(x \cdot {z}^{2}\right)}}\]

   10. Simplified 6.1

       \[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right)\right) + 0.91893853320467\right) + \frac{1}{\color{blue}{x \cdot \left(z \cdot 0.4000000000000064 - \left(z \cdot z\right) \cdot 0.10095227809524161\right) + 12.000000000000048 \cdot x}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 3.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 1.1968875348652573 \cdot 10^{+130}:\\ \;\;\;\;\frac{z \cdot \left(z \cdot \left(y + 0.0007936500793651\right) - 0.0027777777777778\right) + 0.083333333333333}{x} + \sqrt{0.91893853320467 + \left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) + \left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) + \left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right)\right)\right) - x\right)} \cdot \sqrt{\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x - 0.5\right) \cdot \log \left(\sqrt[3]{x}\right) - x\right) + \log \left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \left(x - 0.5\right)\right) + 0.91893853320467\right) + \frac{1}{x \cdot \left(z \cdot 0.4000000000000064 - 0.10095227809524161 \cdot \left(z \cdot z\right)\right) + x \cdot 12.000000000000048}\\ \end{array}\]

Reproduce

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