Average Error: 44.7 → 20.2
Time: 4.7m
Precision: 64
Internal Precision: 2432
\[(x \cdot y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
↓
\[\begin{array}{l} \mathbf{if}\;z \le -2.6889679176030457 \cdot 10^{+34}:\\ \;\;\;\;\left((x \cdot y + z)_* - z\right) - \left(x \cdot y + 1\right)\\ \mathbf{if}\;z \le 2.0701106167539876 \cdot 10^{+43}:\\ \;\;\;\;\log \left(e^{\left((x \cdot y + z)_* - \frac{x \cdot y}{1} \cdot \frac{x \cdot y}{x \cdot y - z}\right) - \left(1 - \frac{z \cdot z}{x \cdot y - z}\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\left((x \cdot y + z)_* - z\right) - \left(x \cdot y + 1\right)\\ \end{array}\]

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original44.7
Target0
Herbie20.2
\[-1\]

Derivation

  1. Split input into 2 regimes

  2. if z < -2.6889679176030457e+34 or 2.0701106167539876e+43 < z

    1. Initial program 62.2

      \[(x \cdot y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
    2. Using strategy rm

    3. Applied flip-+62.7

      \[\leadsto (x \cdot y + z)_* - \left(1 + \color{blue}{\frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - z \cdot z}{x \cdot y - z}}\right)\]
    4. Using strategy rm

    5. Applied div-sub62.7

      \[\leadsto (x \cdot y + z)_* - \left(1 + \color{blue}{\left(\frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z} - \frac{z \cdot z}{x \cdot y - z}\right)}\right)\]

    6. Applied associate-+r-62.7

      \[\leadsto (x \cdot y + z)_* - \color{blue}{\left(\left(1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right) - \frac{z \cdot z}{x \cdot y - z}\right)}\]

    7. Applied associate--r-62.7

      \[\leadsto \color{blue}{\left((x \cdot y + z)_* - \left(1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right)\right) + \frac{z \cdot z}{x \cdot y - z}}\]
    8. Using strategy rm

    9. Applied add-log-exp63.0

      \[\leadsto \left((x \cdot y + z)_* - \left(1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right)\right) + \color{blue}{\log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)}\]

    10. Applied add-log-exp63.0

      \[\leadsto \left((x \cdot y + z)_* - \color{blue}{\log \left(e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}\right)}\right) + \log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)\]

    11. Applied add-log-exp63.6

      \[\leadsto \left(\color{blue}{\log \left(e^{(x \cdot y + z)_*}\right)} - \log \left(e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}\right)\right) + \log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)\]

    12. Applied diff-log63.6

      \[\leadsto \color{blue}{\log \left(\frac{e^{(x \cdot y + z)_*}}{e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}}\right)} + \log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)\]

    13. Applied sum-log63.6

      \[\leadsto \color{blue}{\log \left(\frac{e^{(x \cdot y + z)_*}}{e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}} \cdot e^{\frac{z \cdot z}{x \cdot y - z}}\right)}\]

    14. Applied simplify62.4

      \[\leadsto \log \color{blue}{\left(e^{\left((x \cdot y + z)_* - \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right) - \left(1 - \frac{z \cdot z}{x \cdot y - z}\right)}\right)}\]

    15. Taylor expanded around 0 62.2

      \[\leadsto \log \left(e^{\color{blue}{(x \cdot y + z)_* - \left(z + \left(1 + y \cdot x\right)\right)}}\right)\]

    16. Applied simplify31.8

      \[\leadsto \color{blue}{\left((x \cdot y + z)_* - z\right) - \left(x \cdot y + 1\right)}\]

    if -2.6889679176030457e+34 < z < 2.0701106167539876e+43

    1. Initial program 30.9

      \[(x \cdot y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
    2. Using strategy rm

    3. Applied flip-+31.1

      \[\leadsto (x \cdot y + z)_* - \left(1 + \color{blue}{\frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - z \cdot z}{x \cdot y - z}}\right)\]
    4. Using strategy rm

    5. Applied div-sub31.1

      \[\leadsto (x \cdot y + z)_* - \left(1 + \color{blue}{\left(\frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z} - \frac{z \cdot z}{x \cdot y - z}\right)}\right)\]

    6. Applied associate-+r-31.1

      \[\leadsto (x \cdot y + z)_* - \color{blue}{\left(\left(1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right) - \frac{z \cdot z}{x \cdot y - z}\right)}\]

    7. Applied associate--r-31.1

      \[\leadsto \color{blue}{\left((x \cdot y + z)_* - \left(1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right)\right) + \frac{z \cdot z}{x \cdot y - z}}\]
    8. Using strategy rm

    9. Applied add-log-exp32.4

      \[\leadsto \left((x \cdot y + z)_* - \left(1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right)\right) + \color{blue}{\log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)}\]

    10. Applied add-log-exp33.8

      \[\leadsto \left((x \cdot y + z)_* - \color{blue}{\log \left(e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}\right)}\right) + \log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)\]

    11. Applied add-log-exp34.1

      \[\leadsto \left(\color{blue}{\log \left(e^{(x \cdot y + z)_*}\right)} - \log \left(e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}\right)\right) + \log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)\]

    12. Applied diff-log34.1

      \[\leadsto \color{blue}{\log \left(\frac{e^{(x \cdot y + z)_*}}{e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}}\right)} + \log \left(e^{\frac{z \cdot z}{x \cdot y - z}}\right)\]

    13. Applied sum-log34.1

      \[\leadsto \color{blue}{\log \left(\frac{e^{(x \cdot y + z)_*}}{e^{1 + \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}}} \cdot e^{\frac{z \cdot z}{x \cdot y - z}}\right)}\]

    14. Applied simplify21.2

      \[\leadsto \log \color{blue}{\left(e^{\left((x \cdot y + z)_* - \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{x \cdot y - z}\right) - \left(1 - \frac{z \cdot z}{x \cdot y - z}\right)}\right)}\]
    15. Using strategy rm

    16. Applied *-un-lft-identity21.2

      \[\leadsto \log \left(e^{\left((x \cdot y + z)_* - \frac{\left(x \cdot y\right) \cdot \left(x \cdot y\right)}{\color{blue}{1 \cdot \left(x \cdot y - z\right)}}\right) - \left(1 - \frac{z \cdot z}{x \cdot y - z}\right)}\right)\]

    17. Applied times-frac11.0

      \[\leadsto \log \left(e^{\left((x \cdot y + z)_* - \color{blue}{\frac{x \cdot y}{1} \cdot \frac{x \cdot y}{x \cdot y - z}}\right) - \left(1 - \frac{z \cdot z}{x \cdot y - z}\right)}\right)\]
  3. Recombined 2 regimes into one program.

Runtime

Time bar (total: 4.7m)Debug log

herbie shell --seed '#(991339738 1419949195 2842012120 4157638069 1320221275 2092628673)' 
(FPCore (x y z)
  :name "simple fma test"

  :herbie-target
  -1

  (- (fma x y z) (+ 1 (+ (* x y) z))))