Codec.Picture.Jpg.FastDct:referenceDct from JuicyPixels-3.2.6.1

Average Error: 45.8 → 44.4

Time: 32.7s

Precision: 64

Math

\[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;t \le -11798408174549729122573948662763061510140:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;\left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \left(\left(\left(\sqrt[3]{\cos \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right)} \cdot \sqrt[3]{\cos \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right)}\right) \cdot \cos \left(1 \cdot \frac{t \cdot b}{16}\right) - \sin \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right) \cdot \sin \left(1 \cdot \frac{t \cdot b}{16}\right)\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r736588 = x;
        double r736589 = y;
        double r736590 = 2.0;
        double r736591 = r736589 * r736590;
        double r736592 = 1.0;
        double r736593 = r736591 + r736592;
        double r736594 = z;
        double r736595 = r736593 * r736594;
        double r736596 = t;
        double r736597 = r736595 * r736596;
        double r736598 = 16.0;
        double r736599 = r736597 / r736598;
        double r736600 = cos(r736599);
        double r736601 = r736588 * r736600;
        double r736602 = a;
        double r736603 = r736602 * r736590;
        double r736604 = r736603 + r736592;
        double r736605 = b;
        double r736606 = r736604 * r736605;
        double r736607 = r736606 * r736596;
        double r736608 = r736607 / r736598;
        double r736609 = cos(r736608);
        double r736610 = r736601 * r736609;
        return r736610;
}

↓

double f(double x, double __attribute__((unused)) y, double z, double t, double a, double b) {
        double r736611 = t;
        double r736612 = -1.179840817454973e+40;
        bool r736613 = r736611 <= r736612;
        double r736614 = x;
        double r736615 = z;
        double r736616 = r736615 * r736611;
        double r736617 = 0.0625;
        double r736618 = r736616 * r736617;
        double r736619 = cos(r736618);
        double r736620 = r736619 * r736614;
        double r736621 = 2.0;
        double r736622 = a;
        double r736623 = r736621 * r736622;
        double r736624 = b;
        double r736625 = r736611 * r736624;
        double r736626 = r736623 * r736625;
        double r736627 = 16.0;
        double r736628 = r736626 / r736627;
        double r736629 = cos(r736628);
        double r736630 = cbrt(r736629);
        double r736631 = r736630 * r736630;
        double r736632 = r736631 * r736630;
        double r736633 = 1.0;
        double r736634 = r736625 / r736627;
        double r736635 = r736633 * r736634;
        double r736636 = cos(r736635);
        double r736637 = r736632 * r736636;
        double r736638 = sin(r736628);
        double r736639 = sin(r736635);
        double r736640 = r736638 * r736639;
        double r736641 = r736637 - r736640;
        double r736642 = r736620 * r736641;
        double r736643 = r736613 ? r736614 : r736642;
        return r736643;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Target

Original	45.8
Target	44.1
Herbie	44.4

\[x \cdot \cos \left(\frac{b}{16} \cdot \frac{t}{\left(1 - a \cdot 2\right) + {\left(a \cdot 2\right)}^{2}}\right)\]

Derivation

1. Split input into 2 regimes

2. if t < -1.179840817454973e+40

   1. Initial program 59.4

      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right)\]

   2. Simplified 59.3

      \[\leadsto \color{blue}{\left(\cos \left(\left(\frac{z}{16} \cdot t\right) \cdot \mathsf{fma}\left(2, y, 1\right)\right) \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \mathsf{fma}\left(a, 2, 1\right)\right)}\]

   3. Taylor expanded around 0 58.9

      \[\leadsto \left(\cos \color{blue}{\left(0.0625 \cdot \left(t \cdot z\right)\right)} \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \mathsf{fma}\left(a, 2, 1\right)\right)\]

   4. Simplified 58.9

      \[\leadsto \left(\cos \color{blue}{\left(\left(z \cdot t\right) \cdot 0.0625\right)} \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \mathsf{fma}\left(a, 2, 1\right)\right)\]

   5. Taylor expanded around 0 55.6

      \[\leadsto \color{blue}{x}\]

   if -1.179840817454973e+40 < t

   1. Initial program 42.1

      \[\left(x \cdot \cos \left(\frac{\left(\left(y \cdot 2 + 1\right) \cdot z\right) \cdot t}{16}\right)\right) \cdot \cos \left(\frac{\left(\left(a \cdot 2 + 1\right) \cdot b\right) \cdot t}{16}\right)\]

   2. Simplified 41.5

      \[\leadsto \color{blue}{\left(\cos \left(\left(\frac{z}{16} \cdot t\right) \cdot \mathsf{fma}\left(2, y, 1\right)\right) \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \mathsf{fma}\left(a, 2, 1\right)\right)}\]

   3. Taylor expanded around 0 41.4

      \[\leadsto \left(\cos \color{blue}{\left(0.0625 \cdot \left(t \cdot z\right)\right)} \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \mathsf{fma}\left(a, 2, 1\right)\right)\]

   4. Simplified 41.4

      \[\leadsto \left(\cos \color{blue}{\left(\left(z \cdot t\right) \cdot 0.0625\right)} \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \mathsf{fma}\left(a, 2, 1\right)\right)\]
   5. Using strategy rm

   6. Applied fma-udef 41.4

      \[\leadsto \left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \color{blue}{\left(a \cdot 2 + 1\right)}\right)\]

   7. Applied distribute-lft-in 41.4

      \[\leadsto \left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \cos \color{blue}{\left(\left(\frac{b}{16} \cdot t\right) \cdot \left(a \cdot 2\right) + \left(\frac{b}{16} \cdot t\right) \cdot 1\right)}\]

   8. Applied cos-sum 41.4

      \[\leadsto \left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \color{blue}{\left(\cos \left(\left(\frac{b}{16} \cdot t\right) \cdot \left(a \cdot 2\right)\right) \cdot \cos \left(\left(\frac{b}{16} \cdot t\right) \cdot 1\right) - \sin \left(\left(\frac{b}{16} \cdot t\right) \cdot \left(a \cdot 2\right)\right) \cdot \sin \left(\left(\frac{b}{16} \cdot t\right) \cdot 1\right)\right)}\]

   9. Simplified 41.4

      \[\leadsto \left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \left(\color{blue}{\cos \left(\frac{t \cdot b}{16} \cdot 1\right) \cdot \cos \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right)} - \sin \left(\left(\frac{b}{16} \cdot t\right) \cdot \left(a \cdot 2\right)\right) \cdot \sin \left(\left(\frac{b}{16} \cdot t\right) \cdot 1\right)\right)\]

   10. Simplified 41.4

       \[\leadsto \left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \left(\cos \left(\frac{t \cdot b}{16} \cdot 1\right) \cdot \cos \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right) - \color{blue}{\sin \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right) \cdot \sin \left(\frac{t \cdot b}{16} \cdot 1\right)}\right)\]
   11. Using strategy rm

   12. Applied add-cube-cbrt 41.4

       \[\leadsto \left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \left(\cos \left(\frac{t \cdot b}{16} \cdot 1\right) \cdot \color{blue}{\left(\left(\sqrt[3]{\cos \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right)} \cdot \sqrt[3]{\cos \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right)}\right)} - \sin \left(\frac{\left(t \cdot b\right) \cdot \left(a \cdot 2\right)}{16}\right) \cdot \sin \left(\frac{t \cdot b}{16} \cdot 1\right)\right)\]
3. Recombined 2 regimes into one program.

4. Final simplification 44.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -11798408174549729122573948662763061510140:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;\left(\cos \left(\left(z \cdot t\right) \cdot 0.0625\right) \cdot x\right) \cdot \left(\left(\left(\sqrt[3]{\cos \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right)} \cdot \sqrt[3]{\cos \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right)}\right) \cdot \cos \left(1 \cdot \frac{t \cdot b}{16}\right) - \sin \left(\frac{\left(2 \cdot a\right) \cdot \left(t \cdot b\right)}{16}\right) \cdot \sin \left(1 \cdot \frac{t \cdot b}{16}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019194 +o rules:numerics
(FPCore (x y z t a b)
  :name "Codec.Picture.Jpg.FastDct:referenceDct from JuicyPixels-3.2.6.1"

  :herbie-target
  (* x (cos (* (/ b 16.0) (/ t (+ (- 1.0 (* a 2.0)) (pow (* a 2.0) 2.0))))))

  (* (* x (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0))) (cos (/ (* (* (+ (* a 2.0) 1.0) b) t) 16.0))))