Average Error: 20.3 → 13.9
Time: 5.7m
Precision: 64
Internal Precision: 2432
\[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
↓
\[\begin{array}{l} \mathbf{if}\;y - \frac{z \cdot t}{3.0} \le -2.0335655380336073 \cdot 10^{+307}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{0.3333333333333333}{z \cdot t}\right) - \frac{a}{b \cdot 3.0}\\ \mathbf{if}\;y - \frac{z \cdot t}{3.0} \le 1.506191503122346 \cdot 10^{+304}:\\ \;\;\;\;\frac{\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)}{\cos y \cdot \log \left(e^{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)}\right)} - \frac{a}{b \cdot 3.0}\\ \mathbf{else}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{0.3333333333333333}{z \cdot t}\right) - \frac{a}{b \cdot 3.0}\\ \end{array}\]

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

Original20.3
Target17.4
Herbie13.9
\[\begin{array}{l} \mathbf{if}\;z \lt -1.3793337487235141 \cdot 10^{+129}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333}{z}}{t}\right) - \frac{\frac{a}{3.0}}{b}\\ \mathbf{if}\;z \lt 3.516290613555987 \cdot 10^{+106}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2.0\right) \cdot \cos \left(y - \frac{t}{3.0} \cdot z\right) - \frac{\frac{a}{3.0}}{b}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(y - \frac{\frac{0.3333333333333333}{z}}{t}\right) \cdot \left(2.0 \cdot \sqrt{x}\right) - \frac{\frac{a}{b}}{3.0}\\ \end{array}\]

Derivation

  1. Split input into 2 regimes

  2. if (- y (/ (* z t) 3.0)) < -2.0335655380336073e+307 or 1.506191503122346e+304 < (- y (/ (* z t) 3.0))

    1. Initial program 60.8

      \[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]

    2. Taylor expanded around inf 16.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\cos \left(\frac{1}{y} - 0.3333333333333333 \cdot \frac{1}{z \cdot t}\right)} - \frac{a}{b \cdot 3.0}\]

    3. Applied simplify16.5

      \[\leadsto \color{blue}{\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{0.3333333333333333}{z \cdot t}\right) - \frac{a}{b \cdot 3.0}}\]

    if -2.0335655380336073e+307 < (- y (/ (* z t) 3.0)) < 1.506191503122346e+304

    1. Initial program 14.1

      \[\left(2.0 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3.0}\right) - \frac{a}{b \cdot 3.0}\]
    2. Using strategy rm

    3. Applied cos-diff13.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right) + \sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)} - \frac{a}{b \cdot 3.0}\]
    4. Using strategy rm

    5. Applied flip-+13.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \color{blue}{\frac{\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)}{\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right) - \sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)}} - \frac{a}{b \cdot 3.0}\]

    6. Applied associate-*r/13.5

      \[\leadsto \color{blue}{\frac{\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)}{\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right) - \sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)}} - \frac{a}{b \cdot 3.0}\]
    7. Using strategy rm

    8. Applied add-cube-cbrt13.5

      \[\leadsto \frac{\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)}{\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right) - \sin y \cdot \color{blue}{\left(\left(\sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)}\right)}} - \frac{a}{b \cdot 3.0}\]
    9. Using strategy rm

    10. Applied add-log-exp13.5

      \[\leadsto \frac{\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\cos y \cdot \cos \left(\frac{z \cdot t}{3.0}\right)\right) - \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right) \cdot \left(\sin y \cdot \sin \left(\frac{z \cdot t}{3.0}\right)\right)\right)}{\cos y \cdot \color{blue}{\log \left(e^{\cos \left(\frac{z \cdot t}{3.0}\right)}\right)} - \sin y \cdot \left(\left(\sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\sin \left(\frac{z \cdot t}{3.0}\right)}\right)} - \frac{a}{b \cdot 3.0}\]
  3. Recombined 2 regimes into one program.
  4. Removed slow pow expressions.

Runtime

Time bar (total: 5.7m)Debug log

herbie shell --seed '#(1567391828 2030694642 2833800258 828025724 3004380912 3532991858)' +o setup:early-exit
(FPCore (x y z t a b)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, K"

  :herbie-target
  (if (< z -1.3793337487235141e+129) (- (* (* 2.0 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.3333333333333333 z) t)))) (/ (/ a 3.0) b)) (if (< z 3.516290613555987e+106) (- (* (* (sqrt x) 2.0) (cos (- y (* (/ t 3.0) z)))) (/ (/ a 3.0) b)) (- (* (cos (- y (/ (/ 0.3333333333333333 z) t))) (* 2.0 (sqrt x))) (/ (/ a b) 3.0))))

  (- (* (* 2.0 (sqrt x)) (cos (- y (/ (* z t) 3.0)))) (/ a (* b 3.0))))