Diagrams.Trail:splitAtParam from diagrams-lib-1.3.0.3, A

Average Error: 7.5 → 3.1

Time: 4.4s

Precision: 64

Math

\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1} = -\infty \lor \neg \left(\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1} \le 6.2717689435761409 \cdot 10^{148}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r891135 = x;
        double r891136 = y;
        double r891137 = z;
        double r891138 = r891136 * r891137;
        double r891139 = r891138 - r891135;
        double r891140 = t;
        double r891141 = r891140 * r891137;
        double r891142 = r891141 - r891135;
        double r891143 = r891139 / r891142;
        double r891144 = r891135 + r891143;
        double r891145 = 1.0;
        double r891146 = r891135 + r891145;
        double r891147 = r891144 / r891146;
        return r891147;
}

↓

double f(double x, double y, double z, double t) {
        double r891148 = x;
        double r891149 = y;
        double r891150 = z;
        double r891151 = r891149 * r891150;
        double r891152 = r891151 - r891148;
        double r891153 = t;
        double r891154 = r891153 * r891150;
        double r891155 = r891154 - r891148;
        double r891156 = r891152 / r891155;
        double r891157 = r891148 + r891156;
        double r891158 = 1.0;
        double r891159 = r891148 + r891158;
        double r891160 = r891157 / r891159;
        double r891161 = -inf.0;
        bool r891162 = r891160 <= r891161;
        double r891163 = 6.271768943576141e+148;
        bool r891164 = r891160 <= r891163;
        double r891165 = !r891164;
        bool r891166 = r891162 || r891165;
        double r891167 = r891149 / r891153;
        double r891168 = r891148 + r891167;
        double r891169 = r891168 / r891159;
        double r891170 = r891166 ? r891169 : r891160;
        return r891170;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	7.5
Target	0.4
Herbie	3.1

\[\frac{x + \left(\frac{y}{t - \frac{x}{z}} - \frac{x}{t \cdot z - x}\right)}{x + 1}\]

Derivation

1. Split input into 2 regimes

2. if (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)) < -inf.0 or 6.271768943576141e+148 < (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0))

   1. Initial program 50.6

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]

   2. Taylor expanded around inf 17.7

      \[\leadsto \frac{x + \color{blue}{\frac{y}{t}}}{x + 1}\]

   if -inf.0 < (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)) < 6.271768943576141e+148

   1. Initial program 0.8

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
3. Recombined 2 regimes into one program.

4. Final simplification 3.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1} = -\infty \lor \neg \left(\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1} \le 6.2717689435761409 \cdot 10^{148}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\\ \end{array}\]

Reproduce

herbie shell --seed 2020056 
(FPCore (x y z t)
  :name "Diagrams.Trail:splitAtParam  from diagrams-lib-1.3.0.3, A"
  :precision binary64

  :herbie-target
  (/ (+ x (- (/ y (- t (/ x z))) (/ x (- (* t z) x)))) (+ x 1))

  (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1)))