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

Average Error: 7.7 → 2.7

Time: 4.1s

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 1.59533764149046761 \cdot 10^{179}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \frac{1}{\frac{t \cdot z - x}{y \cdot z - x}}}{x + 1}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r927270 = x;
        double r927271 = y;
        double r927272 = z;
        double r927273 = r927271 * r927272;
        double r927274 = r927273 - r927270;
        double r927275 = t;
        double r927276 = r927275 * r927272;
        double r927277 = r927276 - r927270;
        double r927278 = r927274 / r927277;
        double r927279 = r927270 + r927278;
        double r927280 = 1.0;
        double r927281 = r927270 + r927280;
        double r927282 = r927279 / r927281;
        return r927282;
}

↓

double f(double x, double y, double z, double t) {
        double r927283 = x;
        double r927284 = y;
        double r927285 = z;
        double r927286 = r927284 * r927285;
        double r927287 = r927286 - r927283;
        double r927288 = t;
        double r927289 = r927288 * r927285;
        double r927290 = r927289 - r927283;
        double r927291 = r927287 / r927290;
        double r927292 = r927283 + r927291;
        double r927293 = 1.0;
        double r927294 = r927283 + r927293;
        double r927295 = r927292 / r927294;
        double r927296 = -inf.0;
        bool r927297 = r927295 <= r927296;
        double r927298 = 1.5953376414904676e+179;
        bool r927299 = r927295 <= r927298;
        double r927300 = !r927299;
        bool r927301 = r927297 || r927300;
        double r927302 = r927284 / r927288;
        double r927303 = r927283 + r927302;
        double r927304 = r927303 / r927294;
        double r927305 = 1.0;
        double r927306 = r927290 / r927287;
        double r927307 = r927305 / r927306;
        double r927308 = r927283 + r927307;
        double r927309 = r927308 / r927294;
        double r927310 = r927301 ? r927304 : r927309;
        return r927310;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	7.7
Target	0.3
Herbie	2.7

\[\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 1.5953376414904676e+179 < (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0))

   1. Initial program 53.1

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

   2. Taylor expanded around inf 15.0

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

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

   1. Initial program 0.8

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
   2. Using strategy rm

   3. Applied clear-num 0.8

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

4. Final simplification 2.7

   \[\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 1.59533764149046761 \cdot 10^{179}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \frac{1}{\frac{t \cdot z - x}{y \cdot z - x}}}{x + 1}\\ \end{array}\]

Reproduce

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