Average Error: 20.4 → 15.1
Time: 9.0m
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 -inf.0:\\ \;\;\;\;\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 4.4715459573037013 \cdot 10^{+303}:\\ \;\;\;\;\left(2.0 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \left(\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}}\right) \cdot \sqrt[3]{\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}}\right) + \sin y \cdot \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.4
Target17.9
Herbie15.1
\[\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)) or 4.4715459573037013e+303 < (- y (/ (* z t) 3.0))

    1. Initial program 61.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. Taylor expanded around inf 25.7

      \[\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 simplify25.7

      \[\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 (- y (/ (* z t) 3.0)) < 4.4715459573037013e+303

    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 add-cube-cbrt13.5

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

    7. Applied add-cube-cbrt13.5

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

    9. Applied add-cube-cbrt13.5

      \[\leadsto \left(2.0 \cdot \sqrt{x}\right) \cdot \left(\cos y \cdot \left(\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\color{blue}{\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}}}\right) \cdot \sqrt[3]{\left(\sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)} \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}\right) \cdot \sqrt[3]{\cos \left(\frac{z \cdot t}{3.0}\right)}}\right) + \sin y \cdot \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: 9.0m)Debug log

herbie shell --seed '#(1567391828 2030694642 2833800258 828025724 3004380912 3532991858)' +o setup:early-exit +o reduce:binary-search
(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))))