Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A

Average Error: 10.3 → 2.5

Time: 11.8s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -3.551849925243378557590267856505205658033 \cdot 10^{63} \lor \neg \left(z \le 7.78354143719955323570028935715887199383 \cdot 10^{117}\right):\\ \;\;\;\;\frac{x}{\sqrt[3]{t - a \cdot z}} \cdot \frac{1}{\sqrt[3]{t - a \cdot z} \cdot \sqrt[3]{t - a \cdot z}} - \frac{y}{\frac{t}{z} - a}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{t - a \cdot z} - \left(z \cdot y\right) \cdot \frac{1}{t - a \cdot z}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a) {
        double r656190 = x;
        double r656191 = y;
        double r656192 = z;
        double r656193 = r656191 * r656192;
        double r656194 = r656190 - r656193;
        double r656195 = t;
        double r656196 = a;
        double r656197 = r656196 * r656192;
        double r656198 = r656195 - r656197;
        double r656199 = r656194 / r656198;
        return r656199;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r656200 = z;
        double r656201 = -3.5518499252433786e+63;
        bool r656202 = r656200 <= r656201;
        double r656203 = 7.783541437199553e+117;
        bool r656204 = r656200 <= r656203;
        double r656205 = !r656204;
        bool r656206 = r656202 || r656205;
        double r656207 = x;
        double r656208 = t;
        double r656209 = a;
        double r656210 = r656209 * r656200;
        double r656211 = r656208 - r656210;
        double r656212 = cbrt(r656211);
        double r656213 = r656207 / r656212;
        double r656214 = 1.0;
        double r656215 = r656212 * r656212;
        double r656216 = r656214 / r656215;
        double r656217 = r656213 * r656216;
        double r656218 = y;
        double r656219 = r656208 / r656200;
        double r656220 = r656219 - r656209;
        double r656221 = r656218 / r656220;
        double r656222 = r656217 - r656221;
        double r656223 = r656207 / r656211;
        double r656224 = r656200 * r656218;
        double r656225 = r656214 / r656211;
        double r656226 = r656224 * r656225;
        double r656227 = r656223 - r656226;
        double r656228 = r656206 ? r656222 : r656227;
        return r656228;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original	10.3
Target	1.6
Herbie	2.5

\[\begin{array}{l} \mathbf{if}\;z \lt -32113435955957344:\\ \;\;\;\;\frac{x}{t - a \cdot z} - \frac{y}{\frac{t}{z} - a}\\ \mathbf{elif}\;z \lt 3.51395223729782958298856956410892592016 \cdot 10^{-86}:\\ \;\;\;\;\left(x - y \cdot z\right) \cdot \frac{1}{t - a \cdot z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{t - a \cdot z} - \frac{y}{\frac{t}{z} - a}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if z < -3.5518499252433786e+63 or 7.783541437199553e+117 < z

   1. Initial program 26.3

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

   2. Simplified 26.3

      \[\leadsto \color{blue}{\frac{x - z \cdot y}{t - z \cdot a}}\]
   3. Using strategy rm

   4. Applied div-sub 26.3

      \[\leadsto \color{blue}{\frac{x}{t - z \cdot a} - \frac{z \cdot y}{t - z \cdot a}}\]

   5. Simplified 15.7

      \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\frac{z}{t - z \cdot a} \cdot y}\]
   6. Using strategy rm

   7. Applied clear-num 15.8

      \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\frac{1}{\frac{t - z \cdot a}{z}}} \cdot y\]

   8. Simplified 3.4

      \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\color{blue}{\frac{t}{z} - \frac{a}{1}}} \cdot y\]
   9. Using strategy rm

   10. Applied *-un-lft-identity 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\frac{t}{z} - \frac{a}{\color{blue}{1 \cdot 1}}} \cdot y\]

   11. Applied *-un-lft-identity 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\frac{t}{z} - \frac{\color{blue}{1 \cdot a}}{1 \cdot 1}} \cdot y\]

   12. Applied times-frac 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\frac{t}{z} - \color{blue}{\frac{1}{1} \cdot \frac{a}{1}}} \cdot y\]

   13. Applied *-un-lft-identity 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\frac{t}{\color{blue}{1 \cdot z}} - \frac{1}{1} \cdot \frac{a}{1}} \cdot y\]

   14. Applied *-un-lft-identity 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\frac{\color{blue}{1 \cdot t}}{1 \cdot z} - \frac{1}{1} \cdot \frac{a}{1}} \cdot y\]

   15. Applied times-frac 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\color{blue}{\frac{1}{1} \cdot \frac{t}{z}} - \frac{1}{1} \cdot \frac{a}{1}} \cdot y\]

   16. Applied distribute-lft-out-- 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\color{blue}{\frac{1}{1} \cdot \left(\frac{t}{z} - \frac{a}{1}\right)}} \cdot y\]

   17. Applied add-cube-cbrt 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{\frac{1}{1} \cdot \left(\frac{t}{z} - \frac{a}{1}\right)} \cdot y\]

   18. Applied times-frac 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\left(\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \frac{\sqrt[3]{1}}{\frac{t}{z} - \frac{a}{1}}\right)} \cdot y\]

   19. Applied associate-*l* 3.4

       \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \left(\frac{\sqrt[3]{1}}{\frac{t}{z} - \frac{a}{1}} \cdot y\right)}\]

   20. Simplified 3.3

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \color{blue}{\frac{y}{\frac{t}{z} - a}}\]
   21. Using strategy rm

   22. Applied add-cube-cbrt 3.5

       \[\leadsto \frac{x}{\color{blue}{\left(\sqrt[3]{t - z \cdot a} \cdot \sqrt[3]{t - z \cdot a}\right) \cdot \sqrt[3]{t - z \cdot a}}} - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \frac{y}{\frac{t}{z} - a}\]

   23. Applied *-un-lft-identity 3.5

       \[\leadsto \frac{\color{blue}{1 \cdot x}}{\left(\sqrt[3]{t - z \cdot a} \cdot \sqrt[3]{t - z \cdot a}\right) \cdot \sqrt[3]{t - z \cdot a}} - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \frac{y}{\frac{t}{z} - a}\]

   24. Applied times-frac 3.5

       \[\leadsto \color{blue}{\frac{1}{\sqrt[3]{t - z \cdot a} \cdot \sqrt[3]{t - z \cdot a}} \cdot \frac{x}{\sqrt[3]{t - z \cdot a}}} - \frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\frac{1}{1}} \cdot \frac{y}{\frac{t}{z} - a}\]

   if -3.5518499252433786e+63 < z < 7.783541437199553e+117

   1. Initial program 1.9

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

   2. Simplified 1.9

      \[\leadsto \color{blue}{\frac{x - z \cdot y}{t - z \cdot a}}\]
   3. Using strategy rm

   4. Applied div-sub 1.9

      \[\leadsto \color{blue}{\frac{x}{t - z \cdot a} - \frac{z \cdot y}{t - z \cdot a}}\]

   5. Simplified 3.0

      \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\frac{z}{t - z \cdot a} \cdot y}\]
   6. Using strategy rm

   7. Applied clear-num 3.2

      \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\frac{1}{\frac{t - z \cdot a}{z}}} \cdot y\]

   8. Simplified 2.7

      \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\color{blue}{\frac{t}{z} - \frac{a}{1}}} \cdot y\]
   9. Using strategy rm

   10. Applied frac-sub 3.2

       \[\leadsto \frac{x}{t - z \cdot a} - \frac{1}{\color{blue}{\frac{t \cdot 1 - z \cdot a}{z \cdot 1}}} \cdot y\]

   11. Applied associate-/r/ 3.0

       \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\left(\frac{1}{t \cdot 1 - z \cdot a} \cdot \left(z \cdot 1\right)\right)} \cdot y\]

   12. Applied associate-*l* 2.0

       \[\leadsto \frac{x}{t - z \cdot a} - \color{blue}{\frac{1}{t \cdot 1 - z \cdot a} \cdot \left(\left(z \cdot 1\right) \cdot y\right)}\]

   13. Simplified 2.0

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

4. Final simplification 2.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -3.551849925243378557590267856505205658033 \cdot 10^{63} \lor \neg \left(z \le 7.78354143719955323570028935715887199383 \cdot 10^{117}\right):\\ \;\;\;\;\frac{x}{\sqrt[3]{t - a \cdot z}} \cdot \frac{1}{\sqrt[3]{t - a \cdot z} \cdot \sqrt[3]{t - a \cdot z}} - \frac{y}{\frac{t}{z} - a}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{t - a \cdot z} - \left(z \cdot y\right) \cdot \frac{1}{t - a \cdot z}\\ \end{array}\]

Reproduce

herbie shell --seed 2019179 
(FPCore (x y z t a)
  :name "Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A"

  :herbie-target
  (if (< z -32113435955957344.0) (- (/ x (- t (* a z))) (/ y (- (/ t z) a))) (if (< z 3.5139522372978296e-86) (* (- x (* y z)) (/ 1.0 (- t (* a z)))) (- (/ x (- t (* a z))) (/ y (- (/ t z) a)))))

  (/ (- x (* y z)) (- t (* a z))))