\[\frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{a \cdot 2}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot y - \left(z \cdot 9\right) \cdot t \le -1.56341946069433755 \cdot 10^{290} \lor \neg \left(x \cdot y - \left(z \cdot 9\right) \cdot t \le 7.94655575938796826 \cdot 10^{301}\right):\\ \;\;\;\;0.5 \cdot \left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}\right) - 4.5 \cdot \frac{t}{\frac{a}{z}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{a} \cdot \frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{2}\\ \end{array}\]

\frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{a \cdot 2}

↓

\begin{array}{l}
\mathbf{if}\;x \cdot y - \left(z \cdot 9\right) \cdot t \le -1.56341946069433755 \cdot 10^{290} \lor \neg \left(x \cdot y - \left(z \cdot 9\right) \cdot t \le 7.94655575938796826 \cdot 10^{301}\right):\\
\;\;\;\;0.5 \cdot \left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}\right) - 4.5 \cdot \frac{t}{\frac{a}{z}}\\

\mathbf{else}:\\
\;\;\;\;\frac{1}{a} \cdot \frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{2}\\

\end{array}

double f(double x, double y, double z, double t, double a) {
        double r861289 = x;
        double r861290 = y;
        double r861291 = r861289 * r861290;
        double r861292 = z;
        double r861293 = 9.0;
        double r861294 = r861292 * r861293;
        double r861295 = t;
        double r861296 = r861294 * r861295;
        double r861297 = r861291 - r861296;
        double r861298 = a;
        double r861299 = 2.0;
        double r861300 = r861298 * r861299;
        double r861301 = r861297 / r861300;
        return r861301;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r861302 = x;
        double r861303 = y;
        double r861304 = r861302 * r861303;
        double r861305 = z;
        double r861306 = 9.0;
        double r861307 = r861305 * r861306;
        double r861308 = t;
        double r861309 = r861307 * r861308;
        double r861310 = r861304 - r861309;
        double r861311 = -1.5634194606943375e+290;
        bool r861312 = r861310 <= r861311;
        double r861313 = 7.946555759387968e+301;
        bool r861314 = r861310 <= r861313;
        double r861315 = !r861314;
        bool r861316 = r861312 || r861315;
        double r861317 = 0.5;
        double r861318 = a;
        double r861319 = cbrt(r861318);
        double r861320 = r861319 * r861319;
        double r861321 = r861302 / r861320;
        double r861322 = r861303 / r861319;
        double r861323 = r861321 * r861322;
        double r861324 = r861317 * r861323;
        double r861325 = 4.5;
        double r861326 = r861318 / r861305;
        double r861327 = r861308 / r861326;
        double r861328 = r861325 * r861327;
        double r861329 = r861324 - r861328;
        double r861330 = 1.0;
        double r861331 = r861330 / r861318;
        double r861332 = 2.0;
        double r861333 = r861310 / r861332;
        double r861334 = r861331 * r861333;
        double r861335 = r861316 ? r861329 : r861334;
        return r861335;
}

Original	7.8
Target	5.6
Herbie	0.9

Derivation

Split input into 2 regimes
if (- (* x y) (* (* z 9.0) t)) < -1.5634194606943375e+290 or 7.946555759387968e+301 < (- (* x y) (* (* z 9.0) t))
1. Initial program 57.7
  \[\frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{a \cdot 2}\]
2. Taylor expanded around 0 57.0
  \[\leadsto \color{blue}{0.5 \cdot \frac{x \cdot y}{a} - 4.5 \cdot \frac{t \cdot z}{a}}\]
3. Using strategy rm
4. Applied add-cube-cbrt57.0
  \[\leadsto 0.5 \cdot \frac{x \cdot y}{\color{blue}{\left(\sqrt[3]{a} \cdot \sqrt[3]{a}\right) \cdot \sqrt[3]{a}}} - 4.5 \cdot \frac{t \cdot z}{a}\]
5. Applied times-frac28.5
  \[\leadsto 0.5 \cdot \color{blue}{\left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}\right)} - 4.5 \cdot \frac{t \cdot z}{a}\]
6. Using strategy rm
7. Applied associate-/l*0.9
  \[\leadsto 0.5 \cdot \left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}\right) - 4.5 \cdot \color{blue}{\frac{t}{\frac{a}{z}}}\]
if -1.5634194606943375e+290 < (- (* x y) (* (* z 9.0) t)) < 7.946555759387968e+301
1. Initial program 0.8
  \[\frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{a \cdot 2}\]
2. Using strategy rm
3. Applied *-un-lft-identity0.8
  \[\leadsto \frac{\color{blue}{1 \cdot \left(x \cdot y - \left(z \cdot 9\right) \cdot t\right)}}{a \cdot 2}\]
4. Applied times-frac0.9
  \[\leadsto \color{blue}{\frac{1}{a} \cdot \frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{2}}\]
Recombined 2 regimes into one program.
Final simplification0.9
\[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - \left(z \cdot 9\right) \cdot t \le -1.56341946069433755 \cdot 10^{290} \lor \neg \left(x \cdot y - \left(z \cdot 9\right) \cdot t \le 7.94655575938796826 \cdot 10^{301}\right):\\ \;\;\;\;0.5 \cdot \left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}\right) - 4.5 \cdot \frac{t}{\frac{a}{z}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{a} \cdot \frac{x \cdot y - \left(z \cdot 9\right) \cdot t}{2}\\ \end{array}\]

Reproduce

herbie shell --seed 2020056 +o rules:numerics
(FPCore (x y z t a)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, I"
  :precision binary64

  :herbie-target
  (if (< a -2.090464557976709e+86) (- (* 0.5 (/ (* y x) a)) (* 4.5 (/ t (/ a z)))) (if (< a 2.144030707833976e+99) (/ (- (* x y) (* z (* 9 t))) (* a 2)) (- (* (/ y a) (* x 0.5)) (* (/ t a) (* z 4.5)))))

  (/ (- (* x y) (* (* z 9) t)) (* a 2)))

Error

Try it out

Target

Derivation

`if (- (* x y) (* (* z 9.0) t)) < -1.5634194606943375e+290 or 7.946555759387968e+301 < (- (* x y) (* (* z 9.0) t))`

`if -1.5634194606943375e+290 < (- (* x y) (* (* z 9.0) t)) < 7.946555759387968e+301`

Reproduce

In
Out