\[\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:\\ \;\;\;\;\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\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 -1.2924559506748985 \cdot 10^{48}:\\ \;\;\;\;\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 5.1699103539817533 \cdot 10^{-16}:\\ \;\;\;\;\left(\frac{b + \left(x \cdot 9\right) \cdot y}{z} - 4 \cdot \left(t \cdot a\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.03198024949057577 \cdot 10^{301}:\\ \;\;\;\;\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}:\\ \;\;\;\;\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\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:\\
\;\;\;\;\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\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 -1.2924559506748985 \cdot 10^{48}:\\
\;\;\;\;\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 5.1699103539817533 \cdot 10^{-16}:\\
\;\;\;\;\left(\frac{b + \left(x \cdot 9\right) \cdot y}{z} - 4 \cdot \left(t \cdot a\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.03198024949057577 \cdot 10^{301}:\\
\;\;\;\;\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}:\\
\;\;\;\;\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\right)}}\\

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r886958 = x;
        double r886959 = 9.0;
        double r886960 = r886958 * r886959;
        double r886961 = y;
        double r886962 = r886960 * r886961;
        double r886963 = z;
        double r886964 = 4.0;
        double r886965 = r886963 * r886964;
        double r886966 = t;
        double r886967 = r886965 * r886966;
        double r886968 = a;
        double r886969 = r886967 * r886968;
        double r886970 = r886962 - r886969;
        double r886971 = b;
        double r886972 = r886970 + r886971;
        double r886973 = c;
        double r886974 = r886963 * r886973;
        double r886975 = r886972 / r886974;
        return r886975;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c) {
        double r886976 = x;
        double r886977 = 9.0;
        double r886978 = r886976 * r886977;
        double r886979 = y;
        double r886980 = r886978 * r886979;
        double r886981 = z;
        double r886982 = 4.0;
        double r886983 = r886981 * r886982;
        double r886984 = t;
        double r886985 = r886983 * r886984;
        double r886986 = a;
        double r886987 = r886985 * r886986;
        double r886988 = r886980 - r886987;
        double r886989 = b;
        double r886990 = r886988 + r886989;
        double r886991 = c;
        double r886992 = r886981 * r886991;
        double r886993 = r886990 / r886992;
        double r886994 = -inf.0;
        bool r886995 = r886993 <= r886994;
        double r886996 = 1.0;
        double r886997 = r886977 * r886979;
        double r886998 = r886976 * r886997;
        double r886999 = r886989 + r886998;
        double r887000 = r886999 / r886981;
        double r887001 = r886984 * r886986;
        double r887002 = r886982 * r887001;
        double r887003 = r887000 - r887002;
        double r887004 = r886991 / r887003;
        double r887005 = r886996 / r887004;
        double r887006 = -1.2924559506748985e+48;
        bool r887007 = r886993 <= r887006;
        double r887008 = 5.169910353981753e-16;
        bool r887009 = r886993 <= r887008;
        double r887010 = r886989 + r886980;
        double r887011 = r887010 / r886981;
        double r887012 = r887011 - r887002;
        double r887013 = r886996 / r886991;
        double r887014 = r887012 * r887013;
        double r887015 = 2.0319802494905758e+301;
        bool r887016 = r886993 <= r887015;
        double r887017 = r887016 ? r886993 : r887005;
        double r887018 = r887009 ? r887014 : r887017;
        double r887019 = r887007 ? r886993 : r887018;
        double r887020 = r886995 ? r887005 : r887019;
        return r887020;
}

Target

Original	20.7
Target	15.2
Herbie	7.7

\[\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 3 regimes
if (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -inf.0 or 2.0319802494905758e+301 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c))
1. Initial program 63.0
  \[\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. Simplified27.6
  \[\leadsto \color{blue}{\frac{\frac{b + \left(x \cdot 9\right) \cdot y}{z} - 4 \cdot \left(t \cdot a\right)}{c}}\]
3. Using strategy rm
4. Applied associate-*l*27.5
  \[\leadsto \frac{\frac{b + \color{blue}{x \cdot \left(9 \cdot y\right)}}{z} - 4 \cdot \left(t \cdot a\right)}{c}\]
5. Using strategy rm
6. Applied clear-num27.6
  \[\leadsto \color{blue}{\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\right)}}}\]
if -inf.0 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -1.2924559506748985e+48 or 5.169910353981753e-16 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 2.0319802494905758e+301
1. Initial program 0.6
  \[\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 -1.2924559506748985e+48 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 5.169910353981753e-16
1. Initial program 13.0
  \[\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. Simplified1.0
  \[\leadsto \color{blue}{\frac{\frac{b + \left(x \cdot 9\right) \cdot y}{z} - 4 \cdot \left(t \cdot a\right)}{c}}\]
3. Using strategy rm
4. Applied div-inv1.1
  \[\leadsto \color{blue}{\left(\frac{b + \left(x \cdot 9\right) \cdot y}{z} - 4 \cdot \left(t \cdot a\right)\right) \cdot \frac{1}{c}}\]
Recombined 3 regimes into one program.
Final simplification7.7
\[\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:\\ \;\;\;\;\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\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 -1.2924559506748985 \cdot 10^{48}:\\ \;\;\;\;\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 5.1699103539817533 \cdot 10^{-16}:\\ \;\;\;\;\left(\frac{b + \left(x \cdot 9\right) \cdot y}{z} - 4 \cdot \left(t \cdot a\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.03198024949057577 \cdot 10^{301}:\\ \;\;\;\;\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}:\\ \;\;\;\;\frac{1}{\frac{c}{\frac{b + x \cdot \left(9 \cdot y\right)}{z} - 4 \cdot \left(t \cdot a\right)}}\\ \end{array}\]

Reproduce

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

Falling back on racket egraph because egg-herbie package not installed (more)

Error

Try it out

Target

Derivation

`if (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < -inf.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.2924559506748985e+48 or 5.169910353981753e-16 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 2.0319802494905758e+301`

`if -1.2924559506748985e+48 < (/ (+ (- (* (* x 9.0) y) (* (* (* z 4.0) t) a)) b) (* z c)) < 5.169910353981753e-16`

Reproduce

In
Out