fma_test2

Percentage Accurate: 34.2% → 99.6%

Time: 10.2s

Precision: binary64

Cost: 320

\[1.9 \leq t \land t \leq 2.1\]

Math

\[1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308} \]

↓

\[1.7 \cdot 10^{+308} \cdot \left(t + -1\right) \]

FPCore

(FPCore (t) :precision binary64 (- (* 1.7e+308 t) 1.7e+308))

↓

(FPCore (t) :precision binary64 (* 1.7e+308 (+ t -1.0)))

C

double code(double t) {
	return (1.7e+308 * t) - 1.7e+308;
}

↓

double code(double t) {
	return 1.7e+308 * (t + -1.0);
}

Fortran

real(8) function code(t)
    real(8), intent (in) :: t
    code = (1.7d+308 * t) - 1.7d+308
end function

↓

real(8) function code(t)
    real(8), intent (in) :: t
    code = 1.7d+308 * (t + (-1.0d0))
end function

Java

public static double code(double t) {
	return (1.7e+308 * t) - 1.7e+308;
}

↓

public static double code(double t) {
	return 1.7e+308 * (t + -1.0);
}

Python

def code(t):
	return (1.7e+308 * t) - 1.7e+308

↓

def code(t):
	return 1.7e+308 * (t + -1.0)

Julia

function code(t)
	return Float64(Float64(1.7e+308 * t) - 1.7e+308)
end

↓

function code(t)
	return Float64(1.7e+308 * Float64(t + -1.0))
end

MATLAB

function tmp = code(t)
	tmp = (1.7e+308 * t) - 1.7e+308;
end

↓

function tmp = code(t)
	tmp = 1.7e+308 * (t + -1.0);
end

Wolfram

code[t_] := N[(N[(1.7e+308 * t), $MachinePrecision] - 1.7e+308), $MachinePrecision]

↓

code[t_] := N[(1.7e+308 * N[(t + -1.0), $MachinePrecision]), $MachinePrecision]

Target

Original	34.2%
Target	99.6%
Herbie	99.6%

\[\mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right) \]

Derivation

1. Initial program 34.4%

   \[1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308} \]

2. Applied egg-rr 0.0%

   \[\leadsto \color{blue}{\left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)}} \]
   Step-by-step derivation

   [Start] 34.4%	\[ 1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308} \]
   flip3-- [=>] 0.0%	\[ \color{blue}{\frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - {\left( 1.7 \cdot 10^{+308} \right)}^{3}}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)}} \]
   div-inv [=>] 0.0%	\[ \color{blue}{\left({\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - {\left( 1.7 \cdot 10^{+308} \right)}^{3}\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)}} \]
   pow3 [<=] 0.0%	\[ \left(\color{blue}{\left(\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)} - {\left( 1.7 \cdot 10^{+308} \right)}^{3}\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [=>] 0.0%	\[ \left(\left(\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) - \color{blue}{+\infty}\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [<=] 0.0%	\[ \left(\left(\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) - \color{blue}{+\infty \cdot 1.7 \cdot 10^{+308}}\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [<=] 0.0%	\[ \left(\left(\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) - \color{blue}{\left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308}\right)} \cdot 1.7 \cdot 10^{+308}\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   sub-neg [=>] 0.0%	\[ \color{blue}{\left(\left(\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(-\left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308}\right) \cdot 1.7 \cdot 10^{+308}\right)\right)} \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   pow3 [=>] 0.0%	\[ \left(\color{blue}{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3}} + \left(-\left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308}\right) \cdot 1.7 \cdot 10^{+308}\right)\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   unpow-prod-down [=>] 0.0%	\[ \left(\color{blue}{{\left( 1.7 \cdot 10^{+308} \right)}^{3} \cdot {t}^{3}} + \left(-\left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308}\right) \cdot 1.7 \cdot 10^{+308}\right)\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [=>] 0.0%	\[ \left(\color{blue}{+\infty} \cdot {t}^{3} + \left(-\left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308}\right) \cdot 1.7 \cdot 10^{+308}\right)\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + \left(-\color{blue}{+\infty} \cdot 1.7 \cdot 10^{+308}\right)\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + \left(-\color{blue}{+\infty}\right)\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + \color{blue}{-\infty}\right) \cdot \frac{1}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   *-commutative [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{\color{blue}{\left(t \cdot 1.7 \cdot 10^{+308}\right)} \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   associate-*l* [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{\color{blue}{t \cdot \left(1.7 \cdot 10^{+308} \cdot \left(1.7 \cdot 10^{+308} \cdot t\right)\right)} + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   *-commutative [<=] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{t \cdot \color{blue}{\left(\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   *-commutative [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{t \cdot \left(\color{blue}{\left(t \cdot 1.7 \cdot 10^{+308}\right)} \cdot 1.7 \cdot 10^{+308}\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   associate-*l* [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{t \cdot \color{blue}{\left(t \cdot \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308}\right)\right)} + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]
   metadata-eval [=>] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{t \cdot \left(t \cdot \color{blue}{+\infty}\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)} \]

3. Simplified 99.2%

   \[\leadsto \color{blue}{\frac{1.7 \cdot 10^{+308}}{t + \mathsf{fma}\left(t, t, 1\right)} \cdot \left({t}^{3} + -1\right)} \]
   Step-by-step derivation

   [Start] 0.0%	\[ \left(+\infty \cdot {t}^{3} + -\infty\right) \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   *-commutative [=>] 0.0%	\[ \color{blue}{\frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \cdot \left(+\infty \cdot {t}^{3} + -\infty\right)} \]
   distribute-rgt-in [=>] 0.0%	\[ \color{blue}{\left(+\infty \cdot {t}^{3}\right) \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + -\infty \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)}} \]
   associate-*r/ [=>] 0.0%	\[ \color{blue}{\frac{\left(+\infty \cdot {t}^{3}\right) \cdot 1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)}} + -\infty \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   *-rgt-identity [=>] 0.0%	\[ \frac{\color{blue}{+\infty \cdot {t}^{3}}}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + -\infty \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   associate-*l/ [<=] 0.0%	\[ \color{blue}{\frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \cdot {t}^{3}} + -\infty \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   *-commutative [=>] 0.0%	\[ \color{blue}{{t}^{3} \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)}} + -\infty \cdot \frac{1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   associate-*r/ [=>] 0.0%	\[ {t}^{3} \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + \color{blue}{\frac{-\infty \cdot 1}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)}} \]
   metadata-eval [=>] 0.0%	\[ {t}^{3} \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + \frac{\color{blue}{-\infty}}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   metadata-eval [<=] 0.0%	\[ {t}^{3} \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + \frac{\color{blue}{-1 \cdot +\infty}}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   metadata-eval [<=] 0.0%	\[ {t}^{3} \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + \frac{\color{blue}{\left(-1\right)} \cdot +\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \]
   associate-*r/ [<=] 0.0%	\[ {t}^{3} \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} + \color{blue}{\left(-1\right) \cdot \frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)}} \]
   distribute-rgt-out [=>] 0.0%	\[ \color{blue}{\frac{+\infty}{t \cdot \left(t \cdot +\infty\right) + \left(+\infty + t \cdot +\infty\right)} \cdot \left({t}^{3} + \left(-1\right)\right)} \]

4. Applied egg-rr 99.1%

   \[\leadsto \color{blue}{\frac{1.7 \cdot 10^{+308}}{\frac{t + \mathsf{fma}\left(t, t, 1\right)}{{t}^{3} + -1}}} \]
   Step-by-step derivation

   [Start] 99.2%	\[ \frac{1.7 \cdot 10^{+308}}{t + \mathsf{fma}\left(t, t, 1\right)} \cdot \left({t}^{3} + -1\right) \]
   associate-*l/ [=>] 34.4%	\[ \color{blue}{\frac{1.7 \cdot 10^{+308} \cdot \left({t}^{3} + -1\right)}{t + \mathsf{fma}\left(t, t, 1\right)}} \]
   associate-/l* [=>] 99.1%	\[ \color{blue}{\frac{1.7 \cdot 10^{+308}}{\frac{t + \mathsf{fma}\left(t, t, 1\right)}{{t}^{3} + -1}}} \]

5. Applied egg-rr 99.1%

   \[\leadsto \color{blue}{1.7 \cdot 10^{+308} \cdot \frac{1}{\frac{t + \mathsf{fma}\left(t, t, 1\right)}{{t}^{3} + -1}}} \]
   Step-by-step derivation

   [Start] 99.1%	\[ \frac{1.7 \cdot 10^{+308}}{\frac{t + \mathsf{fma}\left(t, t, 1\right)}{{t}^{3} + -1}} \]
   div-inv [=>] 99.1%	\[ \color{blue}{1.7 \cdot 10^{+308} \cdot \frac{1}{\frac{t + \mathsf{fma}\left(t, t, 1\right)}{{t}^{3} + -1}}} \]

6. Taylor expanded in t around 0 99.6%

   \[\leadsto 1.7 \cdot 10^{+308} \cdot \color{blue}{\left(t - 1\right)} \]

7. Final simplification 99.6%

   \[\leadsto 1.7 \cdot 10^{+308} \cdot \left(t + -1\right) \]

Alternatives

Alternative 1
Accuracy	99.6%
Cost	320

\[1.7 \cdot 10^{+308} \cdot \left(t + -1\right) \]

Alternative 2
Accuracy	34.2%
Cost	192

\[1.7 \cdot 10^{+308} \cdot t \]

Alternative 3
Accuracy	0.0%
Cost	64

\[-1.7 \cdot 10^{+308} \]

Reproduce

herbie shell --seed 2023255 
(FPCore (t)
  :name "fma_test2"
  :precision binary64
  :pre (and (<= 1.9 t) (<= t 2.1))

  :herbie-target
  (fma 1.7e+308 t (- 1.7e+308))

  (- (* 1.7e+308 t) 1.7e+308))