\[\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} \le -1.129525417747451895206584067278771288097 \cdot 10^{293} \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 -7.871356618472160089166896848678735709787 \cdot 10^{-243} \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.01445260762466640003481055345419026939 \cdot 10^{85}\right) \land \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.764994856652344411432804749280478465856 \cdot 10^{301}\right):\\ \;\;\;\;\left(\frac{\mathsf{fma}\left(y, x \cdot 9, b\right)}{z} - \left(a \cdot 4\right) \cdot t\right) \cdot \frac{1}{c}\\ \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} \le -1.129525417747451895206584067278771288097 \cdot 10^{293} \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 -7.871356618472160089166896848678735709787 \cdot 10^{-243} \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.01445260762466640003481055345419026939 \cdot 10^{85}\right) \land \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.764994856652344411432804749280478465856 \cdot 10^{301}\right):\\
\;\;\;\;\left(\frac{\mathsf{fma}\left(y, x \cdot 9, b\right)}{z} - \left(a \cdot 4\right) \cdot t\right) \cdot \frac{1}{c}\\

\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 r422718 = x;
        double r422719 = 9.0;
        double r422720 = r422718 * r422719;
        double r422721 = y;
        double r422722 = r422720 * r422721;
        double r422723 = z;
        double r422724 = 4.0;
        double r422725 = r422723 * r422724;
        double r422726 = t;
        double r422727 = r422725 * r422726;
        double r422728 = a;
        double r422729 = r422727 * r422728;
        double r422730 = r422722 - r422729;
        double r422731 = b;
        double r422732 = r422730 + r422731;
        double r422733 = c;
        double r422734 = r422723 * r422733;
        double r422735 = r422732 / r422734;
        return r422735;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r422736 = x;
        double r422737 = 9.0;
        double r422738 = r422736 * r422737;
        double r422739 = y;
        double r422740 = r422738 * r422739;
        double r422741 = z;
        double r422742 = 4.0;
        double r422743 = r422741 * r422742;
        double r422744 = t;
        double r422745 = r422743 * r422744;
        double r422746 = a;
        double r422747 = r422745 * r422746;
        double r422748 = r422740 - r422747;
        double r422749 = b;
        double r422750 = r422748 + r422749;
        double r422751 = c;
        double r422752 = r422741 * r422751;
        double r422753 = r422750 / r422752;
        double r422754 = -1.1295254177474519e+293;
        bool r422755 = r422753 <= r422754;
        double r422756 = -7.87135661847216e-243;
        bool r422757 = r422753 <= r422756;
        double r422758 = 1.0144526076246664e+85;
        bool r422759 = r422753 <= r422758;
        double r422760 = !r422759;
        double r422761 = 3.7649948566523444e+301;
        bool r422762 = r422753 <= r422761;
        bool r422763 = r422760 && r422762;
        bool r422764 = r422757 || r422763;
        double r422765 = !r422764;
        bool r422766 = r422755 || r422765;
        double r422767 = fma(r422739, r422738, r422749);
        double r422768 = r422767 / r422741;
        double r422769 = r422746 * r422742;
        double r422770 = r422769 * r422744;
        double r422771 = r422768 - r422770;
        double r422772 = 1.0;
        double r422773 = r422772 / r422751;
        double r422774 = r422771 * r422773;
        double r422775 = r422766 ? r422774 : r422753;
        return r422775;
}

Target

Original	20.7
Target	14.4
Herbie	7.6

\[\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.100156740804104887233830094663413900721 \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.170887791174748819600820354912645756062 \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.876823679546137226963937101710277849382 \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.383851504245631860711731716196098366993 \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)) < -1.1295254177474519e+293 or -7.87135661847216e-243 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 1.0144526076246664e+85 or 3.7649948566523444e+301 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))
1. Initial program 37.8
  \[\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. Simplified13.4
  \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left(y, x \cdot 9, b\right)}{z} - \left(a \cdot 4\right) \cdot t}{c}}\]
3. Using strategy rm
4. Applied div-inv13.5
  \[\leadsto \color{blue}{\left(\frac{\mathsf{fma}\left(y, x \cdot 9, b\right)}{z} - \left(a \cdot 4\right) \cdot t\right) \cdot \frac{1}{c}}\]
if -1.1295254177474519e+293 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -7.87135661847216e-243 or 1.0144526076246664e+85 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 3.7649948566523444e+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.6
\[\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} \le -1.129525417747451895206584067278771288097 \cdot 10^{293} \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 -7.871356618472160089166896848678735709787 \cdot 10^{-243} \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.01445260762466640003481055345419026939 \cdot 10^{85}\right) \land \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.764994856652344411432804749280478465856 \cdot 10^{301}\right):\\ \;\;\;\;\left(\frac{\mathsf{fma}\left(y, x \cdot 9, b\right)}{z} - \left(a \cdot 4\right) \cdot t\right) \cdot \frac{1}{c}\\ \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 2019303 +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.1001567408041049e-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.17088779117474882e-53) (/ (+ (- (* (* x 9) y) (* (* z 4) (* t a))) b) (* z c)) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 2.8768236795461372e130) (- (+ (* (* 9 (/ y c)) (/ x z)) (/ b (* c z))) (* 4 (/ (* a t) c))) (if (< (/ (+ (- (* (* x 9) y) (* (* (* z 4) t) a)) b) (* z c)) 1.3838515042456319e158) (/ (+ (- (* (* 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)) < -1.1295254177474519e+293 or -7.87135661847216e-243 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 1.0144526076246664e+85 or 3.7649948566523444e+301 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))`

`if -1.1295254177474519e+293 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -7.87135661847216e-243 or 1.0144526076246664e+85 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 3.7649948566523444e+301`

Reproduce