Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.0 → 8.4

Time: 46.0s

Precision: binary64

Cost: 12044

Math

\[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \]

↓

\[\begin{array}{l} t_1 := \frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\\ t_2 := \left(-\frac{x}{z - 1}\right) + \left(-\frac{t - a}{y}\right)\\ \mathbf{if}\;t_1 \leq -\infty:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_1 \leq -2 \cdot 10^{-301}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t_1 \leq 0:\\ \;\;\;\;\left(\frac{t}{b - y} + \left(-\frac{\left(-\frac{y \cdot x}{b - y}\right) + \frac{\left(t - a\right) \cdot y}{{\left(b - y\right)}^{2}}}{z}\right)\right) - \frac{a}{b - y}\\ \mathbf{elif}\;t_1 \leq 4 \cdot 10^{+236}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

FPCore

(FPCore (x y z t a b)
 :precision binary64
 (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))))

↓

(FPCore (x y z t a b)
 :precision binary64
 (let* ((t_1 (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))))
        (t_2 (+ (- (/ x (- z 1.0))) (- (/ (- t a) y)))))
   (if (<= t_1 (- INFINITY))
     t_2
     (if (<= t_1 -2e-301)
       t_1
       (if (<= t_1 0.0)
         (-
          (+
           (/ t (- b y))
           (-
            (/
             (+ (- (/ (* y x) (- b y))) (/ (* (- t a) y) (pow (- b y) 2.0)))
             z)))
          (/ a (- b y)))
         (if (<= t_1 4e+236) t_1 t_2))))))

C

double code(double x, double y, double z, double t, double a, double b) {
	return ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
}

↓

double code(double x, double y, double z, double t, double a, double b) {
	double t_1 = ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
	double t_2 = -(x / (z - 1.0)) + -((t - a) / y);
	double tmp;
	if (t_1 <= -((double) INFINITY)) {
		tmp = t_2;
	} else if (t_1 <= -2e-301) {
		tmp = t_1;
	} else if (t_1 <= 0.0) {
		tmp = ((t / (b - y)) + -((-((y * x) / (b - y)) + (((t - a) * y) / pow((b - y), 2.0))) / z)) - (a / (b - y));
	} else if (t_1 <= 4e+236) {
		tmp = t_1;
	} else {
		tmp = t_2;
	}
	return tmp;
}

Java

public static double code(double x, double y, double z, double t, double a, double b) {
	return ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
}

↓

public static double code(double x, double y, double z, double t, double a, double b) {
	double t_1 = ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
	double t_2 = -(x / (z - 1.0)) + -((t - a) / y);
	double tmp;
	if (t_1 <= -Double.POSITIVE_INFINITY) {
		tmp = t_2;
	} else if (t_1 <= -2e-301) {
		tmp = t_1;
	} else if (t_1 <= 0.0) {
		tmp = ((t / (b - y)) + -((-((y * x) / (b - y)) + (((t - a) * y) / Math.pow((b - y), 2.0))) / z)) - (a / (b - y));
	} else if (t_1 <= 4e+236) {
		tmp = t_1;
	} else {
		tmp = t_2;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b):
	return ((x * y) + (z * (t - a))) / (y + (z * (b - y)))

↓

def code(x, y, z, t, a, b):
	t_1 = ((x * y) + (z * (t - a))) / (y + (z * (b - y)))
	t_2 = -(x / (z - 1.0)) + -((t - a) / y)
	tmp = 0
	if t_1 <= -math.inf:
		tmp = t_2
	elif t_1 <= -2e-301:
		tmp = t_1
	elif t_1 <= 0.0:
		tmp = ((t / (b - y)) + -((-((y * x) / (b - y)) + (((t - a) * y) / math.pow((b - y), 2.0))) / z)) - (a / (b - y))
	elif t_1 <= 4e+236:
		tmp = t_1
	else:
		tmp = t_2
	return tmp

Julia

function code(x, y, z, t, a, b)
	return Float64(Float64(Float64(x * y) + Float64(z * Float64(t - a))) / Float64(y + Float64(z * Float64(b - y))))
end

↓

function code(x, y, z, t, a, b)
	t_1 = Float64(Float64(Float64(x * y) + Float64(z * Float64(t - a))) / Float64(y + Float64(z * Float64(b - y))))
	t_2 = Float64(Float64(-Float64(x / Float64(z - 1.0))) + Float64(-Float64(Float64(t - a) / y)))
	tmp = 0.0
	if (t_1 <= Float64(-Inf))
		tmp = t_2;
	elseif (t_1 <= -2e-301)
		tmp = t_1;
	elseif (t_1 <= 0.0)
		tmp = Float64(Float64(Float64(t / Float64(b - y)) + Float64(-Float64(Float64(Float64(-Float64(Float64(y * x) / Float64(b - y))) + Float64(Float64(Float64(t - a) * y) / (Float64(b - y) ^ 2.0))) / z))) - Float64(a / Float64(b - y)));
	elseif (t_1 <= 4e+236)
		tmp = t_1;
	else
		tmp = t_2;
	end
	return tmp
end

MATLAB

function tmp = code(x, y, z, t, a, b)
	tmp = ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
end

↓

function tmp_2 = code(x, y, z, t, a, b)
	t_1 = ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
	t_2 = -(x / (z - 1.0)) + -((t - a) / y);
	tmp = 0.0;
	if (t_1 <= -Inf)
		tmp = t_2;
	elseif (t_1 <= -2e-301)
		tmp = t_1;
	elseif (t_1 <= 0.0)
		tmp = ((t / (b - y)) + -((-((y * x) / (b - y)) + (((t - a) * y) / ((b - y) ^ 2.0))) / z)) - (a / (b - y));
	elseif (t_1 <= 4e+236)
		tmp = t_1;
	else
		tmp = t_2;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_] := N[(N[(N[(x * y), $MachinePrecision] + N[(z * N[(t - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(y + N[(z * N[(b - y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(N[(N[(x * y), $MachinePrecision] + N[(z * N[(t - a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(y + N[(z * N[(b - y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[((-N[(x / N[(z - 1.0), $MachinePrecision]), $MachinePrecision]) + (-N[(N[(t - a), $MachinePrecision] / y), $MachinePrecision])), $MachinePrecision]}, If[LessEqual[t$95$1, (-Infinity)], t$95$2, If[LessEqual[t$95$1, -2e-301], t$95$1, If[LessEqual[t$95$1, 0.0], N[(N[(N[(t / N[(b - y), $MachinePrecision]), $MachinePrecision] + (-N[(N[((-N[(N[(y * x), $MachinePrecision] / N[(b - y), $MachinePrecision]), $MachinePrecision]) + N[(N[(N[(t - a), $MachinePrecision] * y), $MachinePrecision] / N[Power[N[(b - y), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / z), $MachinePrecision])), $MachinePrecision] - N[(a / N[(b - y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, 4e+236], t$95$1, t$95$2]]]]]]

Target

Original	23.0
Target	17.9
Herbie	8.4

\[\frac{z \cdot t + y \cdot x}{y + z \cdot \left(b - y\right)} - \frac{a}{\left(b - y\right) + \frac{y}{z}} \]

Derivation

1. Split input into 3 regimes

2. if (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -inf.0 or 4.00000000000000021e236 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y))))

   1. Initial program 59.0

      \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \]

   2. Simplified 59.0

      \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(x, y, z \cdot \left(t - a\right)\right)}{\mathsf{fma}\left(z, b - y, y\right)}} \]
      Proof

   3. Taylor expanded in y around -inf 47.5

      \[\leadsto \color{blue}{-1 \cdot \frac{x}{z - 1} + -1 \cdot \frac{\frac{\left(t - a\right) \cdot z}{z - 1} - -1 \cdot \frac{z \cdot \left(b \cdot x\right)}{{\left(z - 1\right)}^{2}}}{y}} \]

   4. Simplified 47.5

      \[\leadsto \color{blue}{\left(-\frac{x}{z - 1}\right) + \left(-\frac{\frac{\left(t - a\right) \cdot z}{z - 1} + \frac{z \cdot \left(b \cdot x\right)}{{\left(z - 1\right)}^{2}}}{y}\right)} \]
      Proof

   5. Taylor expanded in z around inf 23.2

      \[\leadsto \left(-\frac{x}{z - 1}\right) + \left(-\color{blue}{\frac{t - a}{y}}\right) \]

   if -inf.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -2.00000000000000013e-301 or -0.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < 4.00000000000000021e236

   1. Initial program 0.3

      \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \]

   if -2.00000000000000013e-301 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -0.0

   1. Initial program 46.3

      \[\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \]

   2. Taylor expanded in z around -inf 9.4

      \[\leadsto \color{blue}{\left(\frac{t}{b - y} + -1 \cdot \frac{-1 \cdot \frac{y \cdot x}{b - y} - -1 \cdot \frac{\left(t - a\right) \cdot y}{{\left(b - y\right)}^{2}}}{z}\right) - \frac{a}{b - y}} \]

   3. Simplified 9.4

      \[\leadsto \color{blue}{\left(\frac{t}{b - y} + \left(-\frac{\left(-\frac{y \cdot x}{b - y}\right) + \frac{\left(t - a\right) \cdot y}{{\left(b - y\right)}^{2}}}{z}\right)\right) - \frac{a}{b - y}} \]
      Proof
3. Recombined 3 regimes into one program.

Alternatives

Alternative 1
Error	10.1
Cost	5712

\[\begin{array}{l} t_1 := \frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\\ t_2 := \left(-\frac{x}{z - 1}\right) + \left(-\frac{t - a}{y}\right)\\ \mathbf{if}\;t_1 \leq -\infty:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_1 \leq -2 \cdot 10^{-301}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t_1 \leq 0:\\ \;\;\;\;\frac{t - a}{b}\\ \mathbf{elif}\;t_1 \leq 4 \cdot 10^{+236}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 2
Error	9.9
Cost	5712

\[\begin{array}{l} t_1 := \frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)}\\ t_2 := \left(-\frac{x}{z - 1}\right) + \left(-\frac{t - a}{y}\right)\\ \mathbf{if}\;t_1 \leq -\infty:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_1 \leq -2 \cdot 10^{-301}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t_1 \leq 0:\\ \;\;\;\;\left(-\frac{\left(-\frac{y \cdot x}{b}\right) + \frac{\left(t - a\right) \cdot y}{b \cdot b}}{z}\right) + \frac{t - a}{b}\\ \mathbf{elif}\;t_1 \leq 4 \cdot 10^{+236}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 3
Error	26.6
Cost	1492

\[\begin{array}{l} t_1 := \frac{t - a}{b}\\ t_2 := \left(-\frac{x}{z - 1}\right) + \left(-\frac{t - a}{y}\right)\\ \mathbf{if}\;y \leq -1.35 \cdot 10^{+103}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq -3 \cdot 10^{-122}:\\ \;\;\;\;\frac{y \cdot x}{z \cdot \left(b - y\right) + y}\\ \mathbf{elif}\;y \leq 8 \cdot 10^{-101}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 6 \cdot 10^{-43}:\\ \;\;\;\;\frac{y \cdot x + \left(t - a\right) \cdot z}{y}\\ \mathbf{elif}\;y \leq 1.05 \cdot 10^{+27}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 4
Error	30.1
Cost	1232

\[\begin{array}{l} t_1 := \frac{x}{\left(-z\right) + 1}\\ t_2 := \frac{t - a}{b}\\ \mathbf{if}\;y \leq -4.7 \cdot 10^{+61}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq -1.6 \cdot 10^{-123}:\\ \;\;\;\;\frac{y \cdot x}{z \cdot \left(b - y\right) + y}\\ \mathbf{elif}\;y \leq 1.72 \cdot 10^{-102}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq 2.15 \cdot 10^{-41}:\\ \;\;\;\;\frac{y \cdot x + \left(t - a\right) \cdot z}{y}\\ \mathbf{elif}\;y \leq 1.1 \cdot 10^{+27}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 5
Error	20.0
Cost	1224

\[\begin{array}{l} t_1 := \left(-\frac{x}{z - 1}\right) + \left(-\frac{t - a}{y}\right)\\ \mathbf{if}\;y \leq -1.46 \cdot 10^{+103}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 1.1 \cdot 10^{+18}:\\ \;\;\;\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot b}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 6
Error	31.3
Cost	1176

\[\begin{array}{l} t_1 := \frac{t - a}{b}\\ t_2 := \frac{x}{\left(-z\right) + 1}\\ \mathbf{if}\;y \leq -6 \cdot 10^{+49}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq -1.05 \cdot 10^{-20}:\\ \;\;\;\;\frac{t \cdot z}{y + z \cdot b}\\ \mathbf{elif}\;y \leq -5.5 \cdot 10^{-121}:\\ \;\;\;\;\frac{z}{y} \cdot \left(-a\right) + x\\ \mathbf{elif}\;y \leq 3.4 \cdot 10^{-101}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 4.4 \cdot 10^{-45}:\\ \;\;\;\;x - \frac{z \cdot a}{y}\\ \mathbf{elif}\;y \leq 5.8 \cdot 10^{+27}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 7
Error	30.5
Cost	1044

\[\begin{array}{l} t_1 := \frac{x}{\left(-z\right) + 1}\\ t_2 := \frac{t - a}{b}\\ \mathbf{if}\;y \leq -1.46 \cdot 10^{+50}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq -5.5 \cdot 10^{-121}:\\ \;\;\;\;\frac{y \cdot x}{y + z \cdot b}\\ \mathbf{elif}\;y \leq 1.06 \cdot 10^{-101}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq 1.3 \cdot 10^{-44}:\\ \;\;\;\;x - \frac{z \cdot a}{y}\\ \mathbf{elif}\;y \leq 2.15 \cdot 10^{+27}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 8
Error	30.3
Cost	1044

\[\begin{array}{l} t_1 := \frac{x}{\left(-z\right) + 1}\\ t_2 := \frac{t - a}{b}\\ \mathbf{if}\;y \leq -2.4 \cdot 10^{+60}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq -1.12 \cdot 10^{-122}:\\ \;\;\;\;\frac{y \cdot x}{z \cdot \left(b - y\right) + y}\\ \mathbf{elif}\;y \leq 9 \cdot 10^{-101}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq 4.5 \cdot 10^{-45}:\\ \;\;\;\;x - \frac{z \cdot a}{y}\\ \mathbf{elif}\;y \leq 6.6 \cdot 10^{+27}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 9
Error	30.5
Cost	912

\[\begin{array}{l} t_1 := \frac{t - a}{b}\\ t_2 := \frac{x}{\left(-z\right) + 1}\\ \mathbf{if}\;y \leq -7.5 \cdot 10^{-57}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq 9 \cdot 10^{-101}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 3.5 \cdot 10^{-42}:\\ \;\;\;\;x\\ \mathbf{elif}\;y \leq 1.52 \cdot 10^{+28}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 10
Error	30.2
Cost	912

\[\begin{array}{l} t_1 := \frac{t - a}{b}\\ t_2 := \frac{x}{\left(-z\right) + 1}\\ \mathbf{if}\;y \leq -5.8 \cdot 10^{-57}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;y \leq 4.9 \cdot 10^{-101}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 8 \cdot 10^{-42}:\\ \;\;\;\;\frac{t \cdot z}{y} + x\\ \mathbf{elif}\;y \leq 3.7 \cdot 10^{+27}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]

Alternative 11
Error	40.5
Cost	720

\[\begin{array}{l} \mathbf{if}\;z \leq -4.2 \cdot 10^{+186}:\\ \;\;\;\;\frac{t}{b}\\ \mathbf{elif}\;z \leq -8.2 \cdot 10^{+96}:\\ \;\;\;\;-\frac{a}{b}\\ \mathbf{elif}\;z \leq -6 \cdot 10^{-17}:\\ \;\;\;\;\frac{t}{b}\\ \mathbf{elif}\;z \leq 2.2 \cdot 10^{-44}:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b}\\ \end{array} \]

Alternative 12
Error	30.4
Cost	712

\[\begin{array}{l} t_1 := \frac{t - a}{b}\\ \mathbf{if}\;z \leq -1.55 \cdot 10^{-45}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \leq 4.1 \cdot 10^{-14}:\\ \;\;\;\;x - \frac{z \cdot a}{y}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 13
Error	34.0
Cost	584

\[\begin{array}{l} t_1 := \frac{t - a}{b}\\ \mathbf{if}\;z \leq -1.4 \cdot 10^{-46}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \leq 1.6 \cdot 10^{-44}:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 14
Error	40.7
Cost	456

\[\begin{array}{l} \mathbf{if}\;z \leq -9.2 \cdot 10^{-14}:\\ \;\;\;\;\frac{t}{b}\\ \mathbf{elif}\;z \leq 2.4 \cdot 10^{-44}:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b}\\ \end{array} \]

Alternative 15
Error	47.1
Cost	64

\[x \]

Reproduce

herbie shell --seed 2023010 
(FPCore (x y z t a b)
  :name "Development.Shake.Progress:decay from shake-0.15.5"
  :precision binary64

  :herbie-target
  (- (/ (+ (* z t) (* y x)) (+ y (* z (- b y)))) (/ a (+ (- b y) (/ y z))))

  (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))))