\[\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 \lor \neg \left(\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 -1.9257526309191805 \cdot 10^{-200} \lor \neg \left(\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 \lor \neg \left(\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.03198024949057577 \cdot 10^{301}\right)\right)\right):\\ \;\;\;\;\mathsf{fma}\left(-4, t \cdot \frac{a}{c}, \frac{1}{z} \cdot \frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}\right)\\ \mathbf{else}:\\ \;\;\;\;\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}\\ \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 \lor \neg \left(\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 -1.9257526309191805 \cdot 10^{-200} \lor \neg \left(\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 \lor \neg \left(\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.03198024949057577 \cdot 10^{301}\right)\right)\right):\\
\;\;\;\;\mathsf{fma}\left(-4, t \cdot \frac{a}{c}, \frac{1}{z} \cdot \frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}\right)\\

\mathbf{else}:\\
\;\;\;\;\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}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r720885 = x;
        double r720886 = 9.0;
        double r720887 = r720885 * r720886;
        double r720888 = y;
        double r720889 = r720887 * r720888;
        double r720890 = z;
        double r720891 = 4.0;
        double r720892 = r720890 * r720891;
        double r720893 = t;
        double r720894 = r720892 * r720893;
        double r720895 = a;
        double r720896 = r720894 * r720895;
        double r720897 = r720889 - r720896;
        double r720898 = b;
        double r720899 = r720897 + r720898;
        double r720900 = c;
        double r720901 = r720890 * r720900;
        double r720902 = r720899 / r720901;
        return r720902;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r720903 = x;
        double r720904 = 9.0;
        double r720905 = r720903 * r720904;
        double r720906 = y;
        double r720907 = r720905 * r720906;
        double r720908 = z;
        double r720909 = 4.0;
        double r720910 = r720908 * r720909;
        double r720911 = t;
        double r720912 = r720910 * r720911;
        double r720913 = a;
        double r720914 = r720912 * r720913;
        double r720915 = r720907 - r720914;
        double r720916 = b;
        double r720917 = r720915 + r720916;
        double r720918 = c;
        double r720919 = r720908 * r720918;
        double r720920 = r720917 / r720919;
        double r720921 = -inf.0;
        bool r720922 = r720920 <= r720921;
        double r720923 = -1.9257526309191805e-200;
        bool r720924 = r720920 <= r720923;
        double r720925 = -0.0;
        bool r720926 = r720920 <= r720925;
        double r720927 = 2.0319802494905758e+301;
        bool r720928 = r720920 <= r720927;
        double r720929 = !r720928;
        bool r720930 = r720926 || r720929;
        double r720931 = !r720930;
        bool r720932 = r720924 || r720931;
        double r720933 = !r720932;
        bool r720934 = r720922 || r720933;
        double r720935 = -r720909;
        double r720936 = r720913 / r720918;
        double r720937 = r720911 * r720936;
        double r720938 = 1.0;
        double r720939 = r720938 / r720908;
        double r720940 = r720904 * r720903;
        double r720941 = fma(r720940, r720906, r720916);
        double r720942 = r720941 / r720918;
        double r720943 = r720939 * r720942;
        double r720944 = fma(r720935, r720937, r720943);
        double r720945 = r720934 ? r720944 : r720920;
        return r720945;
}

Target

Original	20.7
Target	15.2
Herbie	7.4

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

Split input into 2 regimes
if (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -inf.0 or -1.9257526309191805e-200 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -0.0 or 2.0319802494905758e+301 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))
1. Initial program 53.4
  \[\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. Simplified28.5
  \[\leadsto \color{blue}{\mathsf{fma}\left(-4, \frac{t \cdot a}{c}, \frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{z \cdot c}\right)}\]
3. Using strategy rm
4. Applied *-un-lft-identity28.5
  \[\leadsto \mathsf{fma}\left(-4, \frac{t \cdot a}{c}, \frac{\color{blue}{1 \cdot \mathsf{fma}\left(x, 9 \cdot y, b\right)}}{z \cdot c}\right)\]
5. Applied times-frac21.2
  \[\leadsto \mathsf{fma}\left(-4, \frac{t \cdot a}{c}, \color{blue}{\frac{1}{z} \cdot \frac{\mathsf{fma}\left(x, 9 \cdot y, b\right)}{c}}\right)\]
6. Simplified21.2
  \[\leadsto \mathsf{fma}\left(-4, \frac{t \cdot a}{c}, \frac{1}{z} \cdot \color{blue}{\frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}}\right)\]
7. Using strategy rm
8. Applied *-un-lft-identity21.2
  \[\leadsto \mathsf{fma}\left(-4, \frac{t \cdot a}{\color{blue}{1 \cdot c}}, \frac{1}{z} \cdot \frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}\right)\]
9. Applied times-frac18.4
  \[\leadsto \mathsf{fma}\left(-4, \color{blue}{\frac{t}{1} \cdot \frac{a}{c}}, \frac{1}{z} \cdot \frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}\right)\]
10. Simplified18.4
  \[\leadsto \mathsf{fma}\left(-4, \color{blue}{t} \cdot \frac{a}{c}, \frac{1}{z} \cdot \frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}\right)\]
if -inf.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -1.9257526309191805e-200 or -0.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 2.0319802494905758e+301
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}\]
Recombined 2 regimes into one program.
Final simplification7.4
\[\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 \lor \neg \left(\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 -1.9257526309191805 \cdot 10^{-200} \lor \neg \left(\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 \lor \neg \left(\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.03198024949057577 \cdot 10^{301}\right)\right)\right):\\ \;\;\;\;\mathsf{fma}\left(-4, t \cdot \frac{a}{c}, \frac{1}{z} \cdot \frac{\mathsf{fma}\left(9 \cdot x, y, b\right)}{c}\right)\\ \mathbf{else}:\\ \;\;\;\;\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}\\ \end{array}\]

Reproduce

herbie shell --seed 2020046 +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)))

Error

Target

Derivation

`if (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -inf.0 or -1.9257526309191805e-200 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -0.0 or 2.0319802494905758e+301 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))`

`if -inf.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -1.9257526309191805e-200 or -0.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 2.0319802494905758e+301`

Reproduce