Rosa's DopplerBench

Average Error: 18.2 → 9.4

Time: 7.2s

Precision: binary64

Cost: 1288

Math

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

↓

\[\begin{array}{l} t_1 := -\frac{v}{t1 + u \cdot 2}\\ \mathbf{if}\;t1 \leq -2.3 \cdot 10^{+48}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t1 \leq 1.7 \cdot 10^{+67}:\\ \;\;\;\;\frac{\left(-t1\right) \cdot v}{u \cdot \left(t1 + \left(t1 + u\right)\right) + t1 \cdot t1}\\ \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 (- (/ v (+ t1 (* u 2.0))))))
   (if (<= t1 -2.3e+48)
     t_1
     (if (<= t1 1.7e+67)
       (/ (* (- t1) v) (+ (* u (+ t1 (+ t1 u))) (* t1 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 = -(v / (t1 + (u * 2.0)));
	double tmp;
	if (t1 <= -2.3e+48) {
		tmp = t_1;
	} else if (t1 <= 1.7e+67) {
		tmp = (-t1 * v) / ((u * (t1 + (t1 + u))) + (t1 * 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 = -(v / (t1 + (u * 2.0d0)))
    if (t1 <= (-2.3d+48)) then
        tmp = t_1
    else if (t1 <= 1.7d+67) then
        tmp = (-t1 * v) / ((u * (t1 + (t1 + u))) + (t1 * 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 = -(v / (t1 + (u * 2.0)));
	double tmp;
	if (t1 <= -2.3e+48) {
		tmp = t_1;
	} else if (t1 <= 1.7e+67) {
		tmp = (-t1 * v) / ((u * (t1 + (t1 + u))) + (t1 * 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 = -(v / (t1 + (u * 2.0)))
	tmp = 0
	if t1 <= -2.3e+48:
		tmp = t_1
	elif t1 <= 1.7e+67:
		tmp = (-t1 * v) / ((u * (t1 + (t1 + u))) + (t1 * 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(v / Float64(t1 + Float64(u * 2.0))))
	tmp = 0.0
	if (t1 <= -2.3e+48)
		tmp = t_1;
	elseif (t1 <= 1.7e+67)
		tmp = Float64(Float64(Float64(-t1) * v) / Float64(Float64(u * Float64(t1 + Float64(t1 + u))) + Float64(t1 * 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 = -(v / (t1 + (u * 2.0)));
	tmp = 0.0;
	if (t1 <= -2.3e+48)
		tmp = t_1;
	elseif (t1 <= 1.7e+67)
		tmp = (-t1 * v) / ((u * (t1 + (t1 + u))) + (t1 * 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[(v / N[(t1 + N[(u * 2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision])}, If[LessEqual[t1, -2.3e+48], t$95$1, If[LessEqual[t1, 1.7e+67], N[(N[((-t1) * v), $MachinePrecision] / N[(N[(u * N[(t1 + N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(t1 * t1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]

Derivation

1. Split input into 2 regimes

2. if t1 < -2.3e48 or 1.7000000000000001e67 < t1

   1. Initial program 29.6

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

   2. Applied egg-rr 32.0

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

   3. Taylor expanded in t1 around inf 34.8

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

   4. Simplified 34.8

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

      [Start] 34.8	\[ \frac{\left(-t1\right) \cdot v}{u \cdot \left(2 \cdot t1\right) + t1 \cdot t1} \]
      rational_best_oopsla_all_46_json_45_simplify-74 [=>] 34.8	\[ \frac{\left(-t1\right) \cdot v}{u \cdot \color{blue}{\left(t1 \cdot 2\right)} + t1 \cdot t1} \]

   5. Applied egg-rr 31.4

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

   6. Taylor expanded in v around 0 8.7

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1 + 2 \cdot u}} \]

   7. Simplified 8.7

      \[\leadsto \color{blue}{-\frac{v}{t1 + u \cdot 2}} \]
      Proof

      [Start] 8.7	\[ -1 \cdot \frac{v}{t1 + 2 \cdot u} \]
      rational_best_oopsla_all_46_json_45_simplify-74 [=>] 8.7	\[ \color{blue}{\frac{v}{t1 + 2 \cdot u} \cdot -1} \]
      rational_best_oopsla_all_46_json_45_simplify-92 [=>] 8.7	\[ \color{blue}{-\frac{v}{t1 + 2 \cdot u}} \]
      rational_best_oopsla_all_46_json_45_simplify-74 [=>] 8.7	\[ -\frac{v}{t1 + \color{blue}{u \cdot 2}} \]

   if -2.3e48 < t1 < 1.7000000000000001e67

   1. Initial program 9.9

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

   2. Applied egg-rr 9.9

      \[\leadsto \frac{\left(-t1\right) \cdot v}{\color{blue}{u \cdot \left(t1 + \left(t1 + u\right)\right) + t1 \cdot t1}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 9.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \leq -2.3 \cdot 10^{+48}:\\ \;\;\;\;-\frac{v}{t1 + u \cdot 2}\\ \mathbf{elif}\;t1 \leq 1.7 \cdot 10^{+67}:\\ \;\;\;\;\frac{\left(-t1\right) \cdot v}{u \cdot \left(t1 + \left(t1 + u\right)\right) + t1 \cdot t1}\\ \mathbf{else}:\\ \;\;\;\;-\frac{v}{t1 + u \cdot 2}\\ \end{array} \]

Alternatives

Alternative 1
Error	9.3
Cost	1032

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

Alternative 2
Error	28.1
Cost	584

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

Alternative 3
Error	25.1
Cost	512

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

Alternative 4
Error	30.8
Cost	256

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

Reproduce

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