Average Error: 45.4 → 19.7
Time: 55.0s
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 -1.7210213825870034 \cdot 10^{+55}:\\ \;\;\;\;\left((x \cdot y + z)_* - z\right) - \left(x \cdot y + 1\right)\\ \mathbf{if}\;z \le 6.03684444331961 \cdot 10^{+16}:\\ \;\;\;\;\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

Original45.4
Target0
Herbie19.7
\[-1\]

Derivation

  1. Split input into 2 regimes

  2. if z < -1.7210213825870034e+55 or 6.03684444331961e+16 < 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.6

      \[\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-exp62.9

      \[\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.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. 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.2

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

    if -1.7210213825870034e+55 < z < 6.03684444331961e+16

    1. Initial program 31.5

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

    3. Applied flip-+31.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-sub31.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-31.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-31.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-exp33.1

      \[\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-exp34.4

      \[\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.7

      \[\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.7

      \[\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.7

      \[\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.1

      \[\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.1

      \[\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-frac10.1

      \[\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: 55.0s)Debug log

herbie shell --seed '#(1151762963 887253659 3096734101 777879090 2714024476 786371635)' 
(FPCore (x y z)
  :name "simple fma test"

  :herbie-target
  -1

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