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

Average Error: 46.7 → 44.3

Time: 17.2s

Precision: binary64

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 \leq -7.405353146839985 \cdot 10^{+28}:\\ \;\;\;\;x\\ \mathbf{elif}\;t \leq 1.8640896652451287 \cdot 10^{-71}:\\ \;\;\;\;\left(x \cdot \cos \left(0.0625 \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\sqrt[3]{0.0625 + a \cdot 0.125} \cdot \left(\left(t \cdot b\right) \cdot \left(\sqrt[3]{0.0625 + a \cdot 0.125} \cdot \sqrt[3]{0.0625 + a \cdot 0.125}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array}\]

FPCore

(FPCore (x y z t a b)
 :precision binary64
 (*
  (* x (cos (/ (* (* (+ (* y 2.0) 1.0) z) t) 16.0)))
  (cos (/ (* (* (+ (* a 2.0) 1.0) b) t) 16.0))))

↓

(FPCore (x y z t a b)
 :precision binary64
 (if (<= t -7.405353146839985e+28)
   x
   (if (<= t 1.8640896652451287e-71)
     (*
      (* x (cos (* 0.0625 (* t z))))
      (cos
       (*
        (cbrt (+ 0.0625 (* a 0.125)))
        (*
         (* t b)
         (* (cbrt (+ 0.0625 (* a 0.125))) (cbrt (+ 0.0625 (* a 0.125))))))))
     x)))

C

double code(double x, double y, double z, double t, double a, double b) {
	return (x * cos(((((y * 2.0) + 1.0) * z) * t) / 16.0)) * cos(((((a * 2.0) + 1.0) * b) * t) / 16.0);
}

↓

double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if (t <= -7.405353146839985e+28) {
		tmp = x;
	} else if (t <= 1.8640896652451287e-71) {
		tmp = (x * cos(0.0625 * (t * z))) * cos(cbrt(0.0625 + (a * 0.125)) * ((t * b) * (cbrt(0.0625 + (a * 0.125)) * cbrt(0.0625 + (a * 0.125)))));
	} else {
		tmp = x;
	}
	return tmp;
}

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	46.7
Target	44.9
Herbie	44.3

\[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 < -7.4053531468399852e28 or 1.8640896652451287e-71 < t

   1. Initial program 58.0

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

      \[\leadsto \color{blue}{\left(x \cdot \cos \left(\left(z \cdot t\right) \cdot \left(0.0625 + y \cdot 0.125\right)\right)\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \left(0.0625 + a \cdot 0.125\right)\right)}\]

   3. Taylor expanded around 0 57.6

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

   4. Taylor expanded around 0 54.5

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

   if -7.4053531468399852e28 < t < 1.8640896652451287e-71

   1. Initial program 34.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 32.8

      \[\leadsto \color{blue}{\left(x \cdot \cos \left(\left(z \cdot t\right) \cdot \left(0.0625 + y \cdot 0.125\right)\right)\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \left(0.0625 + a \cdot 0.125\right)\right)}\]

   3. Taylor expanded around 0 32.7

      \[\leadsto \left(x \cdot \color{blue}{\cos \left(0.0625 \cdot \left(t \cdot z\right)\right)}\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \left(0.0625 + a \cdot 0.125\right)\right)\]
   4. Using strategy rm

   5. Applied add-cube-cbrt_binary64_20573 32.8

      \[\leadsto \left(x \cdot \cos \left(0.0625 \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\left(t \cdot b\right) \cdot \color{blue}{\left(\left(\sqrt[3]{0.0625 + a \cdot 0.125} \cdot \sqrt[3]{0.0625 + a \cdot 0.125}\right) \cdot \sqrt[3]{0.0625 + a \cdot 0.125}\right)}\right)\]

   6. Applied associate-*r*_binary64_20478 32.9

      \[\leadsto \left(x \cdot \cos \left(0.0625 \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \color{blue}{\left(\left(\left(t \cdot b\right) \cdot \left(\sqrt[3]{0.0625 + a \cdot 0.125} \cdot \sqrt[3]{0.0625 + a \cdot 0.125}\right)\right) \cdot \sqrt[3]{0.0625 + a \cdot 0.125}\right)}\]

   7. Simplified 32.9

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

4. Final simplification 44.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \leq -7.405353146839985 \cdot 10^{+28}:\\ \;\;\;\;x\\ \mathbf{elif}\;t \leq 1.8640896652451287 \cdot 10^{-71}:\\ \;\;\;\;\left(x \cdot \cos \left(0.0625 \cdot \left(t \cdot z\right)\right)\right) \cdot \cos \left(\sqrt[3]{0.0625 + a \cdot 0.125} \cdot \left(\left(t \cdot b\right) \cdot \left(\sqrt[3]{0.0625 + a \cdot 0.125} \cdot \sqrt[3]{0.0625 + a \cdot 0.125}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array}\]

Reproduce

herbie shell --seed 2021044 
(FPCore (x y z t a b)
  :name "Codec.Picture.Jpg.FastDct:referenceDct from JuicyPixels-3.2.6.1"
  :precision binary64

  :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))))