Rosa's DopplerBench

Average Error: 18.7 → 1.2

Time: 15.1s

Precision: binary64

Cost: 1032

Math

\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]

↓

\[\begin{array}{l} t_1 := \frac{-t1}{u + t1} \cdot \frac{v}{u + t1}\\ \mathbf{if}\;u \leq -8.2 \cdot 10^{+151}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;u \leq 2 \cdot 10^{-60}:\\ \;\;\;\;\frac{-v}{\left(u + t1\right) \cdot \left(1 + \frac{u}{t1}\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

FPCore

(FPCore (u v t1) :precision binary64 (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))

↓

(FPCore (u v t1)
 :precision binary64
 (let* ((t_1 (* (/ (- t1) (+ u t1)) (/ v (+ u t1)))))
   (if (<= u -8.2e+151)
     t_1
     (if (<= u 2e-60) (/ (- v) (* (+ u t1) (+ 1.0 (/ u t1)))) t_1))))

C

double code(double u, double v, double t1) {
	return (-t1 * v) / ((t1 + u) * (t1 + u));
}

↓

double code(double u, double v, double t1) {
	double t_1 = (-t1 / (u + t1)) * (v / (u + t1));
	double tmp;
	if (u <= -8.2e+151) {
		tmp = t_1;
	} else if (u <= 2e-60) {
		tmp = -v / ((u + t1) * (1.0 + (u / t1)));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Fortran

real(8) function code(u, v, t1)
    real(8), intent (in) :: u
    real(8), intent (in) :: v
    real(8), intent (in) :: t1
    code = (-t1 * v) / ((t1 + u) * (t1 + u))
end function

↓

real(8) function code(u, v, t1)
    real(8), intent (in) :: u
    real(8), intent (in) :: v
    real(8), intent (in) :: t1
    real(8) :: t_1
    real(8) :: tmp
    t_1 = (-t1 / (u + t1)) * (v / (u + t1))
    if (u <= (-8.2d+151)) then
        tmp = t_1
    else if (u <= 2d-60) then
        tmp = -v / ((u + t1) * (1.0d0 + (u / t1)))
    else
        tmp = t_1
    end if
    code = tmp
end function

Java

public static double code(double u, double v, double t1) {
	return (-t1 * v) / ((t1 + u) * (t1 + u));
}

↓

public static double code(double u, double v, double t1) {
	double t_1 = (-t1 / (u + t1)) * (v / (u + t1));
	double tmp;
	if (u <= -8.2e+151) {
		tmp = t_1;
	} else if (u <= 2e-60) {
		tmp = -v / ((u + t1) * (1.0 + (u / t1)));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Python

def code(u, v, t1):
	return (-t1 * v) / ((t1 + u) * (t1 + u))

↓

def code(u, v, t1):
	t_1 = (-t1 / (u + t1)) * (v / (u + t1))
	tmp = 0
	if u <= -8.2e+151:
		tmp = t_1
	elif u <= 2e-60:
		tmp = -v / ((u + t1) * (1.0 + (u / t1)))
	else:
		tmp = t_1
	return tmp

Julia

function code(u, v, t1)
	return Float64(Float64(Float64(-t1) * v) / Float64(Float64(t1 + u) * Float64(t1 + u)))
end

↓

function code(u, v, t1)
	t_1 = Float64(Float64(Float64(-t1) / Float64(u + t1)) * Float64(v / Float64(u + t1)))
	tmp = 0.0
	if (u <= -8.2e+151)
		tmp = t_1;
	elseif (u <= 2e-60)
		tmp = Float64(Float64(-v) / Float64(Float64(u + t1) * Float64(1.0 + Float64(u / t1))));
	else
		tmp = t_1;
	end
	return tmp
end

MATLAB

function tmp = code(u, v, t1)
	tmp = (-t1 * v) / ((t1 + u) * (t1 + u));
end

↓

function tmp_2 = code(u, v, t1)
	t_1 = (-t1 / (u + t1)) * (v / (u + t1));
	tmp = 0.0;
	if (u <= -8.2e+151)
		tmp = t_1;
	elseif (u <= 2e-60)
		tmp = -v / ((u + t1) * (1.0 + (u / t1)));
	else
		tmp = t_1;
	end
	tmp_2 = tmp;
end

Wolfram

code[u_, v_, t1_] := N[(N[((-t1) * v), $MachinePrecision] / N[(N[(t1 + u), $MachinePrecision] * N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[u_, v_, t1_] := Block[{t$95$1 = N[(N[((-t1) / N[(u + t1), $MachinePrecision]), $MachinePrecision] * N[(v / N[(u + t1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[u, -8.2e+151], t$95$1, If[LessEqual[u, 2e-60], N[((-v) / N[(N[(u + t1), $MachinePrecision] * N[(1.0 + N[(u / t1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]

Derivation

1. Split input into 2 regimes

2. if u < -8.1999999999999996e151 or 1.9999999999999999e-60 < u

   1. Initial program 15.3

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]

   2. Simplified 1.2

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
      Proof
      (*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))): 100 points increase in error, 16 points decrease in error

   if -8.1999999999999996e151 < u < 1.9999999999999999e-60

   1. Initial program 21.3

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]

   2. Simplified 1.6

      \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}}} \]
      Proof
      (/.f64 (/.f64 v (+.f64 t1 u)) (-.f64 -1 (/.f64 u t1))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (-.f64 (Rewrite<= metadata-eval (neg.f64 1)) (/.f64 u t1))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (-.f64 (neg.f64 (Rewrite<= *-inverses_binary64 (/.f64 t1 t1))) (/.f64 u t1))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (-.f64 (Rewrite<= distribute-frac-neg_binary64 (/.f64 (neg.f64 t1) t1)) (/.f64 u t1))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (neg.f64 t1) u) t1))): 2 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 t1) (neg.f64 u))) t1)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (Rewrite=> distribute-neg-out_binary64 (neg.f64 (+.f64 t1 u))) t1)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (+.f64 t1 u))) t1)): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (*.f64 -1 (+.f64 t1 u)) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 t1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (*.f64 -1 (+.f64 t1 u)) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (neg.f64 t1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (+.f64 t1 u) (neg.f64 t1))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (+.f64 t1 u) (neg.f64 t1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (Rewrite=> *-lft-identity_binary64 (/.f64 (+.f64 t1 u) (neg.f64 t1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (+.f64 t1 u) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 t1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (/.f64 v (+.f64 t1 u)) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 t1 u) t1) -1))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 v (+.f64 t1 u)) -1) (/.f64 (+.f64 t1 u) t1))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 v (+.f64 t1 u)) (/.f64 -1 (/.f64 (+.f64 t1 u) t1)))): 7 points increase in error, 5 points decrease in error
      (*.f64 (/.f64 v (+.f64 t1 u)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 t1) (+.f64 t1 u)))): 6 points increase in error, 8 points decrease in error
      (*.f64 (/.f64 v (+.f64 t1 u)) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 t1)) (+.f64 t1 u))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 v (neg.f64 t1)) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))): 100 points increase in error, 16 points decrease in error
      (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 t1) v)) (*.f64 (+.f64 t1 u) (+.f64 t1 u))): 0 points increase in error, 0 points decrease in error

   3. Taylor expanded in v around 0 1.2

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{\left(t1 + u\right) \cdot \left(1 + \frac{u}{t1}\right)}} \]

   4. Simplified 1.2

      \[\leadsto \color{blue}{\frac{-v}{\left(t1 + u\right) \cdot \left(1 + \frac{u}{t1}\right)}} \]
      Proof
      (/.f64 (neg.f64 v) (*.f64 (+.f64 t1 u) (+.f64 1 (/.f64 u t1)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 v)) (*.f64 (+.f64 t1 u) (+.f64 1 (/.f64 u t1)))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 v (*.f64 (+.f64 t1 u) (+.f64 1 (/.f64 u t1)))))): 0 points increase in error, 0 points decrease in error
3. Recombined 2 regimes into one program.

4. Final simplification 1.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -8.2 \cdot 10^{+151}:\\ \;\;\;\;\frac{-t1}{u + t1} \cdot \frac{v}{u + t1}\\ \mathbf{elif}\;u \leq 2 \cdot 10^{-60}:\\ \;\;\;\;\frac{-v}{\left(u + t1\right) \cdot \left(1 + \frac{u}{t1}\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{-t1}{u + t1} \cdot \frac{v}{u + t1}\\ \end{array} \]

Alternatives

Alternative 1
Error	15.5
Cost	1232

\[\begin{array}{l} \mathbf{if}\;u \leq -1.6 \cdot 10^{-33}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 1.22 \cdot 10^{-33}:\\ \;\;\;\;\frac{v}{u + t1} \cdot \left(\frac{u}{t1} + -1\right)\\ \mathbf{elif}\;u \leq 8.2 \cdot 10^{+93}:\\ \;\;\;\;\frac{t1}{\frac{u + t1}{v} \cdot \left(t1 - u\right)}\\ \mathbf{elif}\;u \leq 1.6 \cdot 10^{+119}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{v \cdot \frac{t1}{u + t1}}{t1 - u}\\ \end{array} \]

Alternative 2
Error	16.2
Cost	1104

\[\begin{array}{l} \mathbf{if}\;u \leq -5.2 \cdot 10^{-29}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 4.1 \cdot 10^{-35}:\\ \;\;\;\;\frac{v}{u + t1} \cdot \left(\frac{u}{t1} + -1\right)\\ \mathbf{elif}\;u \leq 8.2 \cdot 10^{+93}:\\ \;\;\;\;t1 \cdot \frac{-v}{u \cdot u}\\ \mathbf{elif}\;u \leq 2.65 \cdot 10^{+119}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{v}{u}}{-1 - \frac{u}{t1}}\\ \end{array} \]

Alternative 3
Error	15.5
Cost	1104

\[\begin{array}{l} \mathbf{if}\;u \leq -9 \cdot 10^{-29}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 2.9 \cdot 10^{-34}:\\ \;\;\;\;\frac{v}{u + t1} \cdot \left(\frac{u}{t1} + -1\right)\\ \mathbf{elif}\;u \leq 7.6 \cdot 10^{+93}:\\ \;\;\;\;\frac{t1}{\frac{u + t1}{v} \cdot \left(t1 - u\right)}\\ \mathbf{elif}\;u \leq 1.9 \cdot 10^{+119}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{v}{u}}{-1 - \frac{u}{t1}}\\ \end{array} \]

Alternative 4
Error	16.1
Cost	1040

\[\begin{array}{l} t_1 := \frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{if}\;u \leq -1.05 \cdot 10^{-28}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;u \leq 3.9 \cdot 10^{-34}:\\ \;\;\;\;\frac{-v}{u + t1}\\ \mathbf{elif}\;u \leq 8.2 \cdot 10^{+93}:\\ \;\;\;\;t1 \cdot \frac{-v}{u \cdot u}\\ \mathbf{elif}\;u \leq 2.65 \cdot 10^{+119}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 5
Error	15.9
Cost	1040

\[\begin{array}{l} \mathbf{if}\;u \leq -2.55 \cdot 10^{-29}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 1.3 \cdot 10^{-34}:\\ \;\;\;\;\frac{-v}{u + t1}\\ \mathbf{elif}\;u \leq 8.2 \cdot 10^{+93}:\\ \;\;\;\;t1 \cdot \frac{-v}{u \cdot u}\\ \mathbf{elif}\;u \leq 1.6 \cdot 10^{+119}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \frac{v}{u}}{-u}\\ \end{array} \]

Alternative 6
Error	16.1
Cost	904

\[\begin{array}{l} \mathbf{if}\;u \leq -6 \cdot 10^{-30}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 4.2 \cdot 10^{+125}:\\ \;\;\;\;\frac{-t1}{u + t1} \cdot \frac{v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{v}{u}}{-1 - \frac{u}{t1}}\\ \end{array} \]

Alternative 7
Error	16.0
Cost	840

\[\begin{array}{l} \mathbf{if}\;u \leq -4.1 \cdot 10^{-31}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 9.2 \cdot 10^{+126}:\\ \;\;\;\;\frac{\frac{v}{t1}}{-1 - \frac{u}{t1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \frac{v}{u}}{-u}\\ \end{array} \]

Alternative 8
Error	16.1
Cost	840

\[\begin{array}{l} t_1 := -1 - \frac{u}{t1}\\ \mathbf{if}\;u \leq -2.5 \cdot 10^{-35}:\\ \;\;\;\;\frac{-v}{u} \cdot \frac{t1}{u}\\ \mathbf{elif}\;u \leq 4.3 \cdot 10^{+125}:\\ \;\;\;\;\frac{\frac{v}{t1}}{t_1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{v}{u}}{t_1}\\ \end{array} \]

Alternative 9
Error	15.4
Cost	776

\[\begin{array}{l} t_1 := \frac{-v}{u + t1}\\ \mathbf{if}\;t1 \leq -1.7 \cdot 10^{-25}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t1 \leq 4.6 \cdot 10^{-64}:\\ \;\;\;\;t1 \cdot \frac{-v}{u \cdot u}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 10
Error	15.6
Cost	776

\[\begin{array}{l} t_1 := \frac{-v}{u + t1}\\ \mathbf{if}\;t1 \leq -6.2 \cdot 10^{-25}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t1 \leq 2.25 \cdot 10^{-64}:\\ \;\;\;\;v \cdot \frac{-t1}{u \cdot u}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 11
Error	1.4
Cost	768

\[\frac{-t1}{u + t1} \cdot \frac{v}{u + t1} \]

Alternative 12
Error	20.2
Cost	712

\[\begin{array}{l} t_1 := t1 \cdot \frac{v}{u \cdot u}\\ \mathbf{if}\;u \leq -1.55 \cdot 10^{+166}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;u \leq 1.85 \cdot 10^{+145}:\\ \;\;\;\;\frac{-v}{u + t1}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 13
Error	1.5
Cost	704

\[\frac{\frac{v}{u + t1}}{-1 - \frac{u}{t1}} \]

Alternative 14
Error	27.1
Cost	584

\[\begin{array}{l} \mathbf{if}\;u \leq -2 \cdot 10^{+239}:\\ \;\;\;\;\frac{-v}{u}\\ \mathbf{elif}\;u \leq 1.1 \cdot 10^{+131}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{v}{u + t1}\\ \end{array} \]

Alternative 15
Error	27.2
Cost	520

\[\begin{array}{l} t_1 := \frac{-v}{u}\\ \mathbf{if}\;u \leq -2.1 \cdot 10^{+239}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;u \leq 8.5 \cdot 10^{+129}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 16
Error	24.4
Cost	384

\[\frac{-v}{u + t1} \]

Alternative 17
Error	29.6
Cost	256

\[\frac{-v}{t1} \]

Alternative 18
Error	54.4
Cost	192

\[\frac{v}{t1} \]

Reproduce

herbie shell --seed 2022321 
(FPCore (u v t1)
  :name "Rosa's DopplerBench"
  :precision binary64
  (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))