Average Error: 3.6 → 0.7
Time: 28.9s
Precision: binary64
Cost: 1740
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y} \]
\[\begin{array}{l} t_1 := \frac{y}{z \cdot 3}\\ t_2 := \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{if}\;z \cdot 3 \leq -4 \cdot 10^{+27}:\\ \;\;\;\;\left(x - t_1\right) + t_2\\ \mathbf{elif}\;z \cdot 3 \leq 2 \cdot 10^{-120}:\\ \;\;\;\;x + \frac{\frac{t}{y} - y}{z \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \begin{array}{l} \mathbf{if}\;y \ne 0:\\ \;\;\;\;\frac{1}{\frac{z \cdot 3}{y}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array}\right) + t_2\\ \end{array} \]
(FPCore (x y z t)
 :precision binary64
 (+ (- x (/ y (* z 3.0))) (/ t (* (* z 3.0) y))))
(FPCore (x y z t)
 :precision binary64
 (let* ((t_1 (/ y (* z 3.0))) (t_2 (/ t (* (* z 3.0) y))))
   (if (<= (* z 3.0) -4e+27)
     (+ (- x t_1) t_2)
     (if (<= (* z 3.0) 2e-120)
       (+ x (/ (- (/ t y) y) (* z 3.0)))
       (+ (- x (if (!= y 0.0) (/ 1.0 (/ (* z 3.0) y)) t_1)) t_2)))))
double code(double x, double y, double z, double t) {
	return (x - (y / (z * 3.0))) + (t / ((z * 3.0) * y));
}
double code(double x, double y, double z, double t) {
	double t_1 = y / (z * 3.0);
	double t_2 = t / ((z * 3.0) * y);
	double tmp;
	if ((z * 3.0) <= -4e+27) {
		tmp = (x - t_1) + t_2;
	} else if ((z * 3.0) <= 2e-120) {
		tmp = x + (((t / y) - y) / (z * 3.0));
	} else {
		double tmp_1;
		if (y != 0.0) {
			tmp_1 = 1.0 / ((z * 3.0) / y);
		} else {
			tmp_1 = t_1;
		}
		tmp = (x - tmp_1) + t_2;
	}
	return tmp;
}
real(8) function code(x, y, z, t)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    code = (x - (y / (z * 3.0d0))) + (t / ((z * 3.0d0) * y))
end function
real(8) function code(x, y, z, t)
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8) :: t_1
    real(8) :: t_2
    real(8) :: tmp
    real(8) :: tmp_1
    t_1 = y / (z * 3.0d0)
    t_2 = t / ((z * 3.0d0) * y)
    if ((z * 3.0d0) <= (-4d+27)) then
        tmp = (x - t_1) + t_2
    else if ((z * 3.0d0) <= 2d-120) then
        tmp = x + (((t / y) - y) / (z * 3.0d0))
    else
        if (y /= 0.0d0) then
            tmp_1 = 1.0d0 / ((z * 3.0d0) / y)
        else
            tmp_1 = t_1
        end if
        tmp = (x - tmp_1) + t_2
    end if
    code = tmp
end function
public static double code(double x, double y, double z, double t) {
	return (x - (y / (z * 3.0))) + (t / ((z * 3.0) * y));
}
public static double code(double x, double y, double z, double t) {
	double t_1 = y / (z * 3.0);
	double t_2 = t / ((z * 3.0) * y);
	double tmp;
	if ((z * 3.0) <= -4e+27) {
		tmp = (x - t_1) + t_2;
	} else if ((z * 3.0) <= 2e-120) {
		tmp = x + (((t / y) - y) / (z * 3.0));
	} else {
		double tmp_1;
		if (y != 0.0) {
			tmp_1 = 1.0 / ((z * 3.0) / y);
		} else {
			tmp_1 = t_1;
		}
		tmp = (x - tmp_1) + t_2;
	}
	return tmp;
}
def code(x, y, z, t):
	return (x - (y / (z * 3.0))) + (t / ((z * 3.0) * y))
def code(x, y, z, t):
	t_1 = y / (z * 3.0)
	t_2 = t / ((z * 3.0) * y)
	tmp = 0
	if (z * 3.0) <= -4e+27:
		tmp = (x - t_1) + t_2
	elif (z * 3.0) <= 2e-120:
		tmp = x + (((t / y) - y) / (z * 3.0))
	else:
		tmp_1 = 0
		if y != 0.0:
			tmp_1 = 1.0 / ((z * 3.0) / y)
		else:
			tmp_1 = t_1
		tmp = (x - tmp_1) + t_2
	return tmp
function code(x, y, z, t)
	return Float64(Float64(x - Float64(y / Float64(z * 3.0))) + Float64(t / Float64(Float64(z * 3.0) * y)))
end
function code(x, y, z, t)
	t_1 = Float64(y / Float64(z * 3.0))
	t_2 = Float64(t / Float64(Float64(z * 3.0) * y))
	tmp = 0.0
	if (Float64(z * 3.0) <= -4e+27)
		tmp = Float64(Float64(x - t_1) + t_2);
	elseif (Float64(z * 3.0) <= 2e-120)
		tmp = Float64(x + Float64(Float64(Float64(t / y) - y) / Float64(z * 3.0)));
	else
		tmp_1 = 0.0
		if (y != 0.0)
			tmp_1 = Float64(1.0 / Float64(Float64(z * 3.0) / y));
		else
			tmp_1 = t_1;
		end
		tmp = Float64(Float64(x - tmp_1) + t_2);
	end
	return tmp
end
function tmp = code(x, y, z, t)
	tmp = (x - (y / (z * 3.0))) + (t / ((z * 3.0) * y));
end
function tmp_3 = code(x, y, z, t)
	t_1 = y / (z * 3.0);
	t_2 = t / ((z * 3.0) * y);
	tmp = 0.0;
	if ((z * 3.0) <= -4e+27)
		tmp = (x - t_1) + t_2;
	elseif ((z * 3.0) <= 2e-120)
		tmp = x + (((t / y) - y) / (z * 3.0));
	else
		tmp_2 = 0.0;
		if (y ~= 0.0)
			tmp_2 = 1.0 / ((z * 3.0) / y);
		else
			tmp_2 = t_1;
		end
		tmp = (x - tmp_2) + t_2;
	end
	tmp_3 = tmp;
end
code[x_, y_, z_, t_] := N[(N[(x - N[(y / N[(z * 3.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(t / N[(N[(z * 3.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[x_, y_, z_, t_] := Block[{t$95$1 = N[(y / N[(z * 3.0), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(t / N[(N[(z * 3.0), $MachinePrecision] * y), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(z * 3.0), $MachinePrecision], -4e+27], N[(N[(x - t$95$1), $MachinePrecision] + t$95$2), $MachinePrecision], If[LessEqual[N[(z * 3.0), $MachinePrecision], 2e-120], N[(x + N[(N[(N[(t / y), $MachinePrecision] - y), $MachinePrecision] / N[(z * 3.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(x - If[Unequal[y, 0.0], N[(1.0 / N[(N[(z * 3.0), $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision], t$95$1]), $MachinePrecision] + t$95$2), $MachinePrecision]]]]]
\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}
\begin{array}{l}
t_1 := \frac{y}{z \cdot 3}\\
t_2 := \frac{t}{\left(z \cdot 3\right) \cdot y}\\
\mathbf{if}\;z \cdot 3 \leq -4 \cdot 10^{+27}:\\
\;\;\;\;\left(x - t_1\right) + t_2\\

\mathbf{elif}\;z \cdot 3 \leq 2 \cdot 10^{-120}:\\
\;\;\;\;x + \frac{\frac{t}{y} - y}{z \cdot 3}\\

\mathbf{else}:\\
\;\;\;\;\left(x - \begin{array}{l}
\mathbf{if}\;y \ne 0:\\
\;\;\;\;\frac{1}{\frac{z \cdot 3}{y}}\\

\mathbf{else}:\\
\;\;\;\;t_1\\


\end{array}\right) + t_2\\


\end{array}

Error

Target

Original3.6
Target1.6
Herbie0.7
\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y} \]

Derivation

  1. Split input into 3 regimes
  2. if (*.f64 z 3) < -4.0000000000000001e27

    1. Initial program 0.5

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

    if -4.0000000000000001e27 < (*.f64 z 3) < 1.99999999999999996e-120

    1. Initial program 11.5

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y} \]
    2. Simplified0.4

      \[\leadsto \color{blue}{x + \frac{0.3333333333333333}{z} \cdot \left(\frac{t}{y} - y\right)} \]
      Proof
    3. Applied egg-rr0.3

      \[\leadsto x + \color{blue}{\frac{\frac{t}{y} - y}{z \cdot 3}} \]

    if 1.99999999999999996e-120 < (*.f64 z 3)

    1. Initial program 1.1

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y} \]
    2. Applied egg-rr1.1

      \[\leadsto \left(x - \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;y \ne 0:\\ \;\;\;\;{\left(\frac{z \cdot 3}{y}\right)}^{-1}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{z \cdot 3}\\ } \end{array}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y} \]
    3. Simplified1.1

      \[\leadsto \left(x - \color{blue}{\begin{array}{l} \color{blue}{\mathbf{if}\;y \ne 0:\\ \;\;\;\;\frac{1}{\frac{z \cdot 3}{y}}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{z \cdot 3}\\ } \end{array}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y} \]
      Proof
  3. Recombined 3 regimes into one program.

Alternatives

Alternative 1
Error0.7
Cost1480
\[\begin{array}{l} t_1 := \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{if}\;z \cdot 3 \leq -4 \cdot 10^{+27}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \cdot 3 \leq 2 \cdot 10^{-120}:\\ \;\;\;\;x + \frac{\frac{t}{y} - y}{z \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 2
Error1.7
Cost968
\[\begin{array}{l} t_1 := x + \frac{0.3333333333333333}{z} \cdot \left(\frac{t}{y} - y\right)\\ \mathbf{if}\;y \leq -1.9 \cdot 10^{-119}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 7.2 \cdot 10^{-58}:\\ \;\;\;\;x + \frac{\frac{t}{z}}{y \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 3
Error1.6
Cost968
\[\begin{array}{l} t_1 := x + \frac{\frac{t}{y} - y}{z \cdot 3}\\ \mathbf{if}\;y \leq -1.3 \cdot 10^{-119}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 2 \cdot 10^{-59}:\\ \;\;\;\;x + \frac{\frac{t}{z}}{y \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 4
Error12.3
Cost840
\[\begin{array}{l} t_1 := x - \frac{y}{z \cdot 3}\\ \mathbf{if}\;x \leq -2.1 \cdot 10^{+47}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;x \leq 9.5 \cdot 10^{-132}:\\ \;\;\;\;\frac{0.3333333333333333}{z} \cdot \left(\frac{t}{y} - y\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 5
Error9.5
Cost840
\[\begin{array}{l} t_1 := x - \frac{y}{z \cdot 3}\\ \mathbf{if}\;y \leq -4.2 \cdot 10^{+53}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 4.4 \cdot 10^{+67}:\\ \;\;\;\;x + \frac{t}{\left(y \cdot z\right) \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 6
Error7.2
Cost840
\[\begin{array}{l} t_1 := x - \frac{y}{z \cdot 3}\\ \mathbf{if}\;y \leq -5.5 \cdot 10^{+50}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 4.4 \cdot 10^{+67}:\\ \;\;\;\;x + \frac{\frac{0.3333333333333333}{z} \cdot t}{y}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 7
Error7.2
Cost840
\[\begin{array}{l} t_1 := x - \frac{y}{z \cdot 3}\\ \mathbf{if}\;y \leq -5.5 \cdot 10^{+50}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 4.4 \cdot 10^{+67}:\\ \;\;\;\;x + \frac{\frac{t}{z}}{y \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 8
Error29.1
Cost584
\[\begin{array}{l} \mathbf{if}\;x \leq -1.3 \cdot 10^{+78}:\\ \;\;\;\;x\\ \mathbf{elif}\;x \leq 1.52 \cdot 10^{-128}:\\ \;\;\;\;-0.3333333333333333 \cdot \frac{y}{z}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]
Alternative 9
Error29.1
Cost584
\[\begin{array}{l} \mathbf{if}\;x \leq -1.3 \cdot 10^{+78}:\\ \;\;\;\;x\\ \mathbf{elif}\;x \leq 1.52 \cdot 10^{-128}:\\ \;\;\;\;\frac{-0.3333333333333333}{z} \cdot y\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]
Alternative 10
Error29.1
Cost584
\[\begin{array}{l} \mathbf{if}\;x \leq -1.3 \cdot 10^{+78}:\\ \;\;\;\;x\\ \mathbf{elif}\;x \leq 1.52 \cdot 10^{-128}:\\ \;\;\;\;\frac{y}{z \cdot -3}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]
Alternative 11
Error17.8
Cost448
\[x - \frac{y}{z \cdot 3} \]
Alternative 12
Error37.7
Cost64
\[x \]

Error

Reproduce

herbie shell --seed 2023010 
(FPCore (x y z t)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, H"
  :precision binary64

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

  (+ (- x (/ y (* z 3.0))) (/ t (* (* z 3.0) y))))