Average Error: 6.3 → 1.3
Time: 9.3s
Precision: 64
\[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\]
↓
\[\begin{array}{l} \mathbf{if}\;\left(a + b \cdot c\right) \cdot c = -\infty \lor \neg \left(\left(a + b \cdot c\right) \cdot c \le 4.51874428508253623 \cdot 10^{119}\right):\\ \;\;\;\;1 \cdot \left(2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\\ \end{array}\]
2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)
↓
\begin{array}{l}
\mathbf{if}\;\left(a + b \cdot c\right) \cdot c = -\infty \lor \neg \left(\left(a + b \cdot c\right) \cdot c \le 4.51874428508253623 \cdot 10^{119}\right):\\
\;\;\;\;1 \cdot \left(2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\\

\end{array}
double f(double x, double y, double z, double t, double a, double b, double c, double i) {
        double r824050 = 2.0;
        double r824051 = x;
        double r824052 = y;
        double r824053 = r824051 * r824052;
        double r824054 = z;
        double r824055 = t;
        double r824056 = r824054 * r824055;
        double r824057 = r824053 + r824056;
        double r824058 = a;
        double r824059 = b;
        double r824060 = c;
        double r824061 = r824059 * r824060;
        double r824062 = r824058 + r824061;
        double r824063 = r824062 * r824060;
        double r824064 = i;
        double r824065 = r824063 * r824064;
        double r824066 = r824057 - r824065;
        double r824067 = r824050 * r824066;
        return r824067;
}
↓
double f(double x, double y, double z, double t, double a, double b, double c, double i) {
        double r824068 = a;
        double r824069 = b;
        double r824070 = c;
        double r824071 = r824069 * r824070;
        double r824072 = r824068 + r824071;
        double r824073 = r824072 * r824070;
        double r824074 = -inf.0;
        bool r824075 = r824073 <= r824074;
        double r824076 = 4.518744285082536e+119;
        bool r824077 = r824073 <= r824076;
        double r824078 = !r824077;
        bool r824079 = r824075 || r824078;
        double r824080 = 1.0;
        double r824081 = 2.0;
        double r824082 = x;
        double r824083 = y;
        double r824084 = r824082 * r824083;
        double r824085 = z;
        double r824086 = t;
        double r824087 = r824085 * r824086;
        double r824088 = r824084 + r824087;
        double r824089 = i;
        double r824090 = r824070 * r824089;
        double r824091 = r824072 * r824090;
        double r824092 = r824088 - r824091;
        double r824093 = r824081 * r824092;
        double r824094 = r824080 * r824093;
        double r824095 = r824073 * r824089;
        double r824096 = r824088 - r824095;
        double r824097 = r824081 * r824096;
        double r824098 = r824079 ? r824094 : r824097;
        return r824098;
}

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

Bits error versus i

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original6.3
Target1.9
Herbie1.3
\[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right)\]

Derivation

  1. Split input into 2 regimes

  2. if (* (+ a (* b c)) c) < -inf.0 or 4.518744285082536e+119 < (* (+ a (* b c)) c)

    1. Initial program 31.9

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\]
    2. Using strategy rm

    3. Applied associate-*l*5.7

      \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \color{blue}{\left(a + b \cdot c\right) \cdot \left(c \cdot i\right)}\right)\]
    4. Using strategy rm

    5. Applied *-un-lft-identity5.7

      \[\leadsto \color{blue}{1 \cdot \left(2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right)\right)}\]

    if -inf.0 < (* (+ a (* b c)) c) < 4.518744285082536e+119

    1. Initial program 0.3

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\]
  3. Recombined 2 regimes into one program.

  4. Final simplification1.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\left(a + b \cdot c\right) \cdot c = -\infty \lor \neg \left(\left(a + b \cdot c\right) \cdot c \le 4.51874428508253623 \cdot 10^{119}\right):\\ \;\;\;\;1 \cdot \left(2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020027 
(FPCore (x y z t a b c i)
  :name "Diagrams.ThreeD.Shapes:frustum from diagrams-lib-1.3.0.3, A"
  :precision binary64

  :herbie-target
  (* 2 (- (+ (* x y) (* z t)) (* (+ a (* b c)) (* c i))))

  (* 2 (- (+ (* x y) (* z t)) (* (* (+ a (* b c)) c) i))))