Average Error: 20.8 → 3.3
Time: 12.8s
Precision: 64
\[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]
\[\begin{array}{l} \mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{1}{z} \cdot \frac{b}{c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -3.86575567753969965 \cdot 10^{-184}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -0.0:\\ \;\;\;\;\left(\frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z} - a \cdot \left(4 \cdot t\right)\right) \cdot \frac{1}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le 2.5630952637815053 \cdot 10^{303}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{1}{z} \cdot \frac{b}{c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \end{array}\]
\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}
\begin{array}{l}
\mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} = -\infty:\\
\;\;\;\;\mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{1}{z} \cdot \frac{b}{c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\

\mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -3.86575567753969965 \cdot 10^{-184}:\\
\;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\

\mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -0.0:\\
\;\;\;\;\left(\frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z} - a \cdot \left(4 \cdot t\right)\right) \cdot \frac{1}{c}\\

\mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le 2.5630952637815053 \cdot 10^{303}:\\
\;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{1}{z} \cdot \frac{b}{c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\

\end{array}
double f(double x, double y, double z, double t, double a, double b, double c) {
        double r824237 = x;
        double r824238 = 9.0;
        double r824239 = r824237 * r824238;
        double r824240 = y;
        double r824241 = r824239 * r824240;
        double r824242 = z;
        double r824243 = 4.0;
        double r824244 = r824242 * r824243;
        double r824245 = t;
        double r824246 = r824244 * r824245;
        double r824247 = a;
        double r824248 = r824246 * r824247;
        double r824249 = r824241 - r824248;
        double r824250 = b;
        double r824251 = r824249 + r824250;
        double r824252 = c;
        double r824253 = r824242 * r824252;
        double r824254 = r824251 / r824253;
        return r824254;
}

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r824255 = x;
        double r824256 = 9.0;
        double r824257 = r824255 * r824256;
        double r824258 = y;
        double r824259 = r824257 * r824258;
        double r824260 = z;
        double r824261 = 4.0;
        double r824262 = r824260 * r824261;
        double r824263 = t;
        double r824264 = r824262 * r824263;
        double r824265 = a;
        double r824266 = r824264 * r824265;
        double r824267 = r824259 - r824266;
        double r824268 = b;
        double r824269 = r824267 + r824268;
        double r824270 = c;
        double r824271 = r824260 * r824270;
        double r824272 = r824269 / r824271;
        double r824273 = -inf.0;
        bool r824274 = r824272 <= r824273;
        double r824275 = r824270 / r824258;
        double r824276 = r824260 * r824275;
        double r824277 = r824255 / r824276;
        double r824278 = 1.0;
        double r824279 = r824278 / r824260;
        double r824280 = r824268 / r824270;
        double r824281 = r824279 * r824280;
        double r824282 = fma(r824277, r824256, r824281);
        double r824283 = r824265 / r824270;
        double r824284 = r824263 * r824283;
        double r824285 = r824261 * r824284;
        double r824286 = r824282 - r824285;
        double r824287 = -3.8657556775396997e-184;
        bool r824288 = r824272 <= r824287;
        double r824289 = -0.0;
        bool r824290 = r824272 <= r824289;
        double r824291 = r824256 * r824258;
        double r824292 = fma(r824255, r824291, r824268);
        double r824293 = r824292 / r824260;
        double r824294 = r824261 * r824263;
        double r824295 = r824265 * r824294;
        double r824296 = r824293 - r824295;
        double r824297 = r824278 / r824270;
        double r824298 = r824296 * r824297;
        double r824299 = 2.5630952637815053e+303;
        bool r824300 = r824272 <= r824299;
        double r824301 = r824300 ? r824272 : r824286;
        double r824302 = r824290 ? r824298 : r824301;
        double r824303 = r824288 ? r824272 : r824302;
        double r824304 = r824274 ? r824286 : r824303;
        return r824304;
}

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

Bits error versus c

Target

Original20.8
Target14.9
Herbie3.3
\[\begin{array}{l} \mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt -1.10015674080410512 \cdot 10^{-171}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(z \cdot 4\right) \cdot \left(t \cdot a\right)\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt -0.0:\\ \;\;\;\;\frac{\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z}}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt 1.17088779117474882 \cdot 10^{-53}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(z \cdot 4\right) \cdot \left(t \cdot a\right)\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt 2.8768236795461372 \cdot 10^{130}:\\ \;\;\;\;\left(\left(9 \cdot \frac{y}{c}\right) \cdot \frac{x}{z} + \frac{b}{c \cdot z}\right) - 4 \cdot \frac{a \cdot t}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \lt 1.3838515042456319 \cdot 10^{158}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(z \cdot 4\right) \cdot \left(t \cdot a\right)\right) + b}{z \cdot c}\\ \mathbf{else}:\\ \;\;\;\;\left(9 \cdot \left(\frac{y}{c \cdot z} \cdot x\right) + \frac{b}{c \cdot z}\right) - 4 \cdot \frac{a \cdot t}{c}\\ \end{array}\]

Derivation

  1. Split input into 3 regimes
  2. if (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -inf.0 or 2.5630952637815053e+303 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))

    1. Initial program 63.1

      \[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]
    2. Simplified26.7

      \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z} - a \cdot \left(4 \cdot t\right)}{c}}\]
    3. Taylor expanded around 0 30.7

      \[\leadsto \color{blue}{\left(\frac{b}{z \cdot c} + 9 \cdot \frac{x \cdot y}{z \cdot c}\right) - 4 \cdot \frac{t \cdot a}{c}}\]
    4. Simplified30.7

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x \cdot y}{z \cdot c}, 9, \frac{b}{z \cdot c}\right) - 4 \cdot \frac{t \cdot a}{c}}\]
    5. Using strategy rm
    6. Applied *-un-lft-identity30.7

      \[\leadsto \mathsf{fma}\left(\frac{x \cdot y}{z \cdot c}, 9, \frac{b}{z \cdot c}\right) - 4 \cdot \frac{t \cdot a}{\color{blue}{1 \cdot c}}\]
    7. Applied times-frac25.6

      \[\leadsto \mathsf{fma}\left(\frac{x \cdot y}{z \cdot c}, 9, \frac{b}{z \cdot c}\right) - 4 \cdot \color{blue}{\left(\frac{t}{1} \cdot \frac{a}{c}\right)}\]
    8. Simplified25.6

      \[\leadsto \mathsf{fma}\left(\frac{x \cdot y}{z \cdot c}, 9, \frac{b}{z \cdot c}\right) - 4 \cdot \left(\color{blue}{t} \cdot \frac{a}{c}\right)\]
    9. Using strategy rm
    10. Applied associate-/l*14.3

      \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{x}{\frac{z \cdot c}{y}}}, 9, \frac{b}{z \cdot c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\]
    11. Simplified11.4

      \[\leadsto \mathsf{fma}\left(\frac{x}{\color{blue}{z \cdot \frac{c}{y}}}, 9, \frac{b}{z \cdot c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\]
    12. Using strategy rm
    13. Applied *-un-lft-identity11.4

      \[\leadsto \mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{\color{blue}{1 \cdot b}}{z \cdot c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\]
    14. Applied times-frac10.6

      \[\leadsto \mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \color{blue}{\frac{1}{z} \cdot \frac{b}{c}}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\]

    if -inf.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -3.8657556775396997e-184 or -0.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 2.5630952637815053e+303

    1. Initial program 0.7

      \[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]

    if -3.8657556775396997e-184 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -0.0

    1. Initial program 33.9

      \[\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\]
    2. Simplified0.6

      \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z} - a \cdot \left(4 \cdot t\right)}{c}}\]
    3. Using strategy rm
    4. Applied div-inv0.7

      \[\leadsto \color{blue}{\left(\frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z} - a \cdot \left(4 \cdot t\right)\right) \cdot \frac{1}{c}}\]
  3. Recombined 3 regimes into one program.
  4. Final simplification3.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{1}{z} \cdot \frac{b}{c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -3.86575567753969965 \cdot 10^{-184}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le -0.0:\\ \;\;\;\;\left(\frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z} - a \cdot \left(4 \cdot t\right)\right) \cdot \frac{1}{c}\\ \mathbf{elif}\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c} \le 2.5630952637815053 \cdot 10^{303}:\\ \;\;\;\;\frac{\left(\left(x \cdot 9\right) \cdot y - \left(\left(z \cdot 4\right) \cdot t\right) \cdot a\right) + b}{z \cdot c}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z \cdot \frac{c}{y}}, 9, \frac{1}{z} \cdot \frac{b}{c}\right) - 4 \cdot \left(t \cdot \frac{a}{c}\right)\\ \end{array}\]

Reproduce

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

  :herbie-target
  (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) -1.1001567408041051e-171) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) -0.0) (/ (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) z) c) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 1.1708877911747488e-53) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 2.876823679546137e+130) (- (+ (* (* 9 (/ y c)) (/ x z)) (/ b (* c z))) (* 4 (/ (* a t) c))) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 1.3838515042456319e+158) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (- (+ (* 9 (* (/ y (* c z)) x)) (/ b (* c z))) (* 4 (/ (* a t) c))))))))

  (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)))