Average Error: 45.3 → 25.2
Time: 44.9s
Precision: 64
Internal Precision: 2432
\[(x \cdot y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
↓
\[\begin{array}{l} \mathbf{if}\;(x \cdot y + z)_* - 1 \le -2.746091189880756 \cdot 10^{+160}:\\ \;\;\;\;\log \left(e^{\left((x \cdot y + z)_* - \frac{y \cdot x}{1} \cdot \frac{y \cdot x}{y \cdot x - z}\right) + \left(\frac{z \cdot z}{y \cdot x - z} - 1\right)}\right)\\ \mathbf{if}\;(x \cdot y + z)_* - 1 \le 1.4757573520937636 \cdot 10^{+156}:\\ \;\;\;\;\log \left(e^{\left(\left((x \cdot y + z)_* - \frac{\left(y \cdot x\right) \cdot \left(y \cdot x\right)}{y \cdot x - z}\right) + \frac{z \cdot z}{y \cdot x - z}\right) + \left(-1\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(e^{\left((x \cdot y + z)_* - \frac{y \cdot x}{1} \cdot \frac{y \cdot x}{y \cdot x - z}\right) + \left(\frac{z \cdot z}{y \cdot x - z} - 1\right)}\right)\\ \end{array}\]

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original45.3
Target0
Herbie25.2
\[-1\]

Derivation

  1. Split input into 2 regimes

  2. if (- (fma x y z) 1) < -2.746091189880756e+160 or 1.4757573520937636e+156 < (- (fma x y z) 1)

    1. Initial program 62.4

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

    3. Applied flip-+63.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-sub63.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-63.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-63.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-exp63.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-exp63.1

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

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

    16. Applied *-un-lft-identity63.1

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

    17. Applied times-frac49.0

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

    if -2.746091189880756e+160 < (- (fma x y z) 1) < 1.4757573520937636e+156

    1. Initial program 30.8

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

    3. Applied flip-+30.9

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

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

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

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

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

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

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

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

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

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

    16. Applied sub-neg19.8

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

    17. Applied associate-+r+5.1

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

Runtime

Time bar (total: 44.9s)Debug logProfile

herbie shell --seed '#(1070100504 930361288 1279167582 284574201 1450237281 2578255382)' 
(FPCore (x y z)
  :name "simple fma test"

  :herbie-target
  -1

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