xlohi (overflows)

Average Error: 62.0 → 43.8

Time: 19.1s

Precision: binary64

Cost: 57088

\[lo < -1 \cdot 10^{+308} \land hi > 10^{+308}\]

Math

\[\frac{x - lo}{hi - lo} \]

↓

\[\begin{array}{l} t_0 := 1 + \frac{hi}{lo}\\ t_1 := \frac{hi - x}{lo}\\ t_2 := {t_1}^{3}\\ t_3 := 1 + t_2\\ t_4 := 1 - {t_1}^{6}\\ \left(\frac{\left(1 - t_2\right) + {\left(\left(hi - x\right) \cdot \frac{t_0}{lo}\right)}^{2} \cdot \left(t_2 + -1\right)}{t_4 \cdot t_4} \cdot \left(t_3 \cdot t_3\right)\right) \cdot \left(1 + \left(t_1 \cdot t_0\right) \cdot \mathsf{fma}\left(t_0, t_1, 1\right)\right) \end{array} \]

FPCore

(FPCore (lo hi x) :precision binary64 (/ (- x lo) (- hi lo)))

↓

(FPCore (lo hi x)
 :precision binary64
 (let* ((t_0 (+ 1.0 (/ hi lo)))
        (t_1 (/ (- hi x) lo))
        (t_2 (pow t_1 3.0))
        (t_3 (+ 1.0 t_2))
        (t_4 (- 1.0 (pow t_1 6.0))))
   (*
    (*
     (/
      (+ (- 1.0 t_2) (* (pow (* (- hi x) (/ t_0 lo)) 2.0) (+ t_2 -1.0)))
      (* t_4 t_4))
     (* t_3 t_3))
    (+ 1.0 (* (* t_1 t_0) (fma t_0 t_1 1.0))))))

C

double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}

↓

double code(double lo, double hi, double x) {
	double t_0 = 1.0 + (hi / lo);
	double t_1 = (hi - x) / lo;
	double t_2 = pow(t_1, 3.0);
	double t_3 = 1.0 + t_2;
	double t_4 = 1.0 - pow(t_1, 6.0);
	return ((((1.0 - t_2) + (pow(((hi - x) * (t_0 / lo)), 2.0) * (t_2 + -1.0))) / (t_4 * t_4)) * (t_3 * t_3)) * (1.0 + ((t_1 * t_0) * fma(t_0, t_1, 1.0)));
}

Julia

function code(lo, hi, x)
	return Float64(Float64(x - lo) / Float64(hi - lo))
end

↓

function code(lo, hi, x)
	t_0 = Float64(1.0 + Float64(hi / lo))
	t_1 = Float64(Float64(hi - x) / lo)
	t_2 = t_1 ^ 3.0
	t_3 = Float64(1.0 + t_2)
	t_4 = Float64(1.0 - (t_1 ^ 6.0))
	return Float64(Float64(Float64(Float64(Float64(1.0 - t_2) + Float64((Float64(Float64(hi - x) * Float64(t_0 / lo)) ^ 2.0) * Float64(t_2 + -1.0))) / Float64(t_4 * t_4)) * Float64(t_3 * t_3)) * Float64(1.0 + Float64(Float64(t_1 * t_0) * fma(t_0, t_1, 1.0))))
end

Wolfram

code[lo_, hi_, x_] := N[(N[(x - lo), $MachinePrecision] / N[(hi - lo), $MachinePrecision]), $MachinePrecision]

↓

code[lo_, hi_, x_] := Block[{t$95$0 = N[(1.0 + N[(hi / lo), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[(hi - x), $MachinePrecision] / lo), $MachinePrecision]}, Block[{t$95$2 = N[Power[t$95$1, 3.0], $MachinePrecision]}, Block[{t$95$3 = N[(1.0 + t$95$2), $MachinePrecision]}, Block[{t$95$4 = N[(1.0 - N[Power[t$95$1, 6.0], $MachinePrecision]), $MachinePrecision]}, N[(N[(N[(N[(N[(1.0 - t$95$2), $MachinePrecision] + N[(N[Power[N[(N[(hi - x), $MachinePrecision] * N[(t$95$0 / lo), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] * N[(t$95$2 + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(t$95$4 * t$95$4), $MachinePrecision]), $MachinePrecision] * N[(t$95$3 * t$95$3), $MachinePrecision]), $MachinePrecision] * N[(1.0 + N[(N[(t$95$1 * t$95$0), $MachinePrecision] * N[(t$95$0 * t$95$1 + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]]

Derivation

1. Initial program 62.0

   \[\frac{x - lo}{hi - lo} \]

2. Taylor expanded in lo around inf 64.0

   \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{lo} + \left(\frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}} + 1\right)\right) - -1 \cdot \frac{hi}{lo}} \]

3. Simplified 51.9

   \[\leadsto \color{blue}{1 + \left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}} \]
   Proof

   [Start] 64.0	\[ \left(-1 \cdot \frac{x}{lo} + \left(\frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}} + 1\right)\right) - -1 \cdot \frac{hi}{lo} \]
   +-commutative [=>] 64.0	\[ \color{blue}{\left(\left(\frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}} + 1\right) + -1 \cdot \frac{x}{lo}\right)} - -1 \cdot \frac{hi}{lo} \]
   associate--l+ [=>] 64.0	\[ \color{blue}{\left(\frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}} + 1\right) + \left(-1 \cdot \frac{x}{lo} - -1 \cdot \frac{hi}{lo}\right)} \]
   +-commutative [=>] 64.0	\[ \color{blue}{\left(1 + \frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}}\right)} + \left(-1 \cdot \frac{x}{lo} - -1 \cdot \frac{hi}{lo}\right) \]
   associate-*r/ [=>] 64.0	\[ \left(1 + \frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}}\right) + \left(\color{blue}{\frac{-1 \cdot x}{lo}} - -1 \cdot \frac{hi}{lo}\right) \]
   associate-*r/ [=>] 64.0	\[ \left(1 + \frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}}\right) + \left(\frac{-1 \cdot x}{lo} - \color{blue}{\frac{-1 \cdot hi}{lo}}\right) \]
   div-sub [<=] 64.0	\[ \left(1 + \frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}}\right) + \color{blue}{\frac{-1 \cdot x - -1 \cdot hi}{lo}} \]
   distribute-lft-out-- [=>] 64.0	\[ \left(1 + \frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}}\right) + \frac{\color{blue}{-1 \cdot \left(x - hi\right)}}{lo} \]
   associate-*r/ [<=] 64.0	\[ \left(1 + \frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}}\right) + \color{blue}{-1 \cdot \frac{x - hi}{lo}} \]
   associate-+r+ [<=] 64.0	\[ \color{blue}{1 + \left(\frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}} + -1 \cdot \frac{x - hi}{lo}\right)} \]

4. Applied egg-rr 51.9

   \[\leadsto \color{blue}{\frac{1 - {\left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right)}^{2}}{1 - {\left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right)}^{3}} \cdot \left(1 + \left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right)} \]

5. Taylor expanded in lo around inf 64.0

   \[\leadsto \frac{1 - {\left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right)}^{2}}{1 - \color{blue}{\frac{{\left(hi - x\right)}^{3}}{{lo}^{3}}}} \cdot \left(1 + \left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right) \]

6. Simplified 43.8

   \[\leadsto \frac{1 - {\left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right)}^{2}}{1 - \color{blue}{{\left(\frac{hi - x}{lo}\right)}^{3}}} \cdot \left(1 + \left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right) \]
   Proof

   [Start] 64.0	\[ \frac{1 - {\left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right)}^{2}}{1 - \frac{{\left(hi - x\right)}^{3}}{{lo}^{3}}} \cdot \left(1 + \left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right) \]
   cube-div [<=] 43.8	\[ \frac{1 - {\left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right)}^{2}}{1 - \color{blue}{{\left(\frac{hi - x}{lo}\right)}^{3}}} \cdot \left(1 + \left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right) \]

7. Applied egg-rr 43.8

   \[\leadsto \color{blue}{\left(\frac{\left(1 - {\left(\frac{hi - x}{lo}\right)}^{3}\right) - \left(1 - {\left(\frac{hi - x}{lo}\right)}^{3}\right) \cdot {\left(\frac{1 + \frac{hi}{lo}}{lo} \cdot \left(hi - x\right)\right)}^{2}}{\left(1 - {\left(\frac{hi - x}{lo}\right)}^{6}\right) \cdot \left(1 - {\left(\frac{hi - x}{lo}\right)}^{6}\right)} \cdot \left(\left({\left(\frac{hi - x}{lo}\right)}^{3} + 1\right) \cdot \left({\left(\frac{hi - x}{lo}\right)}^{3} + 1\right)\right)\right)} \cdot \left(1 + \left(\left(1 + \frac{hi}{lo}\right) \cdot \frac{hi - x}{lo}\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right) \]

8. Final simplification 43.8

   \[\leadsto \left(\frac{\left(1 - {\left(\frac{hi - x}{lo}\right)}^{3}\right) + {\left(\left(hi - x\right) \cdot \frac{1 + \frac{hi}{lo}}{lo}\right)}^{2} \cdot \left({\left(\frac{hi - x}{lo}\right)}^{3} + -1\right)}{\left(1 - {\left(\frac{hi - x}{lo}\right)}^{6}\right) \cdot \left(1 - {\left(\frac{hi - x}{lo}\right)}^{6}\right)} \cdot \left(\left(1 + {\left(\frac{hi - x}{lo}\right)}^{3}\right) \cdot \left(1 + {\left(\frac{hi - x}{lo}\right)}^{3}\right)\right)\right) \cdot \left(1 + \left(\frac{hi - x}{lo} \cdot \left(1 + \frac{hi}{lo}\right)\right) \cdot \mathsf{fma}\left(1 + \frac{hi}{lo}, \frac{hi - x}{lo}, 1\right)\right) \]

Alternatives

Alternative 1
Error	43.8
Cost	57088

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := {t_0}^{3}\\ t_2 := 1 + t_1\\ t_3 := 1 + \frac{hi}{lo}\\ t_4 := 1 - {t_0}^{6}\\ \left(1 + \left(t_0 \cdot t_3\right) \cdot \mathsf{fma}\left(t_3, t_0, 1\right)\right) \cdot \left(\left(t_2 \cdot t_2\right) \cdot \frac{1 - \left(t_1 + \left(1 - t_1\right) \cdot {\left(\left(hi - x\right) \cdot \frac{t_3}{lo}\right)}^{2}\right)}{t_4 \cdot t_4}\right) \end{array} \]

Alternative 2
Error	43.8
Cost	29440

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := 1 + \frac{hi}{lo}\\ \left(1 + \left(t_0 \cdot t_1\right) \cdot \mathsf{fma}\left(t_1, t_0, 1\right)\right) \cdot \left(\frac{1}{1 - {t_0}^{6}} \cdot \left(\left(1 + {t_0}^{3}\right) \cdot \left(1 - {\left(\left(hi - x\right) \cdot \frac{t_1}{lo}\right)}^{2}\right)\right)\right) \end{array} \]

Alternative 3
Error	43.8
Cost	29312

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := 1 + \frac{hi}{lo}\\ \left(1 + \left(t_0 \cdot t_1\right) \cdot \mathsf{fma}\left(t_1, t_0, 1\right)\right) \cdot \left(\left(1 - {\left(\left(hi - x\right) \cdot \frac{t_1}{lo}\right)}^{2}\right) \cdot \frac{1 + {t_0}^{3}}{1 - {t_0}^{6}}\right) \end{array} \]

Alternative 4
Error	43.8
Cost	29312

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := 1 + \frac{hi}{lo}\\ \left(1 + \left(t_0 \cdot t_1\right) \cdot \mathsf{fma}\left(t_1, t_0, 1\right)\right) \cdot \left(\left(1 + {t_0}^{3}\right) \cdot \frac{1 - {\left(\left(hi - x\right) \cdot \frac{t_1}{lo}\right)}^{2}}{1 - {t_0}^{6}}\right) \end{array} \]

Alternative 5
Error	43.8
Cost	29312

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := 1 + \frac{hi}{lo}\\ \left(1 + \left(t_0 \cdot t_1\right) \cdot \mathsf{fma}\left(t_1, t_0, 1\right)\right) \cdot \left(\frac{1 - {\left(\frac{t_1}{\frac{lo}{hi - x}}\right)}^{2}}{{t_0}^{6} + -1} \cdot \left(-1 - {t_0}^{3}\right)\right) \end{array} \]

Alternative 6
Error	43.8
Cost	22464

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := 1 + \frac{hi}{lo}\\ t_2 := t_0 \cdot t_1\\ \left(1 + t_2 \cdot \mathsf{fma}\left(t_1, t_0, 1\right)\right) \cdot \frac{1 - {t_2}^{2}}{1 + \frac{-1}{{\left(\frac{lo}{hi - x}\right)}^{3}}} \end{array} \]

Alternative 7
Error	43.8
Cost	16640

\[\begin{array}{l} t_0 := \frac{hi - x}{lo}\\ t_1 := 1 + \frac{hi}{lo}\\ t_2 := t_0 \cdot t_1\\ \left(1 + t_2 \cdot \mathsf{fma}\left(t_1, t_0, 1\right)\right) \cdot \frac{1 + t_2 \cdot \left(t_0 \cdot \left(-1 - \frac{hi}{lo}\right)\right)}{1 - {t_0}^{3}} \end{array} \]

Alternative 8
Error	47.8
Cost	15880

\[\begin{array}{l} t_0 := 1 + \frac{hi}{lo}\\ t_1 := \frac{hi - x}{lo}\\ \mathbf{if}\;x \leq -1.4 \cdot 10^{+154}:\\ \;\;\;\;1 + t_0 \cdot \sqrt{\frac{hi - x}{\frac{\frac{lo}{hi - x}}{\frac{1}{lo}}}}\\ \mathbf{elif}\;x \leq 1.35 \cdot 10^{+154}:\\ \;\;\;\;\left(1 + \left(t_1 \cdot t_0\right) \cdot \mathsf{fma}\left(t_0, t_1, 1\right)\right) \cdot \frac{1 - \frac{x \cdot x}{lo \cdot lo}}{1 - {t_1}^{3}}\\ \mathbf{else}:\\ \;\;\;\;t_1 \cdot \frac{hi}{lo}\\ \end{array} \]

Alternative 9
Error	51.6
Cost	576

\[\frac{hi - x}{lo} \cdot \frac{hi}{lo} \]

Alternative 10
Error	52.0
Cost	256

\[\frac{-lo}{hi} \]

Alternative 11
Error	52.0
Cost	64

\[1 \]

Reproduce

herbie shell --seed 2023012 
(FPCore (lo hi x)
  :name "xlohi (overflows)"
  :precision binary64
  :pre (and (< lo -1e+308) (> hi 1e+308))
  (/ (- x lo) (- hi lo)))