Diagrams.TwoD.Apollonian:initialConfig from diagrams-contrib-1.3.0.5, A

Percentage Accurate: 68.5% → 99.8%

Time: 1.4min

Alternatives: 10

Speedup: 1.0×

• 59.0% of points produce a very large (infinite) output. You may want to add a precondition.

Specification

Math

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

FPCore

(FPCore (x y z)
  :precision binary64
  (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2)))

C

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

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = (((x * x) + (y * y)) - (z * z)) / (y * 2.0d0)
end function

Java

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

Python

def code(x, y, z):
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0)

Julia

function code(x, y, z)
	return Float64(Float64(Float64(Float64(x * x) + Float64(y * y)) - Float64(z * z)) / Float64(y * 2.0))
end

MATLAB

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

Wolfram

code[x_, y_, z_] := N[(N[(N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision] - N[(z * z), $MachinePrecision]), $MachinePrecision] / N[(y * 2), $MachinePrecision]), $MachinePrecision]

Initial Program: 68.5% accurate, 1.0× speedup

Math

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

FPCore

(FPCore (x y z)
  :precision binary64
  (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2)))

C

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

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = (((x * x) + (y * y)) - (z * z)) / (y * 2.0d0)
end function

Java

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

Python

def code(x, y, z):
	return (((x * x) + (y * y)) - (z * z)) / (y * 2.0)

Julia

function code(x, y, z)
	return Float64(Float64(Float64(Float64(x * x) + Float64(y * y)) - Float64(z * z)) / Float64(y * 2.0))
end

MATLAB

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

Wolfram

code[x_, y_, z_] := N[(N[(N[(N[(x * x), $MachinePrecision] + N[(y * y), $MachinePrecision]), $MachinePrecision] - N[(z * z), $MachinePrecision]), $MachinePrecision] / N[(y * 2), $MachinePrecision]), $MachinePrecision]

Alternative 1: 99.8% accurate, 1.0× speedup

Math

\[\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

FPCore

(FPCore (x y z)
  :precision binary64
  (134-z0z1z2z3z4 (/ 1/2 y) y y (+ z x) (- z x)))

Derivation

1. Initial program 68.5%

   \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
2. Step-by-step derivation

   1. lift-/.f64 N/A

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

   2. mult-flip N/A

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

   3. *-commutative N/A

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

   4. lift--.f64 N/A

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

   5. lift-+.f64 N/A

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

   6. +-commutative N/A

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

   7. associate--l+ N/A

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

   8. add-flip N/A

      \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

   9. lift-*.f64 N/A

      \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

   10. sub-negate-rev N/A

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

   11. lift-*.f64 N/A

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

   12. lift-*.f64 N/A

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

   13. difference-of-squares N/A

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

   14. lower-134-z0z1z2z3z4 N/A

       \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   15. lift-*.f64 N/A

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

   16. *-commutative N/A

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

   17. associate-/r* N/A

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

   18. lower-/.f64 N/A

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

   19. metadata-eval N/A

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

   20. lower-+.f64 N/A

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

   21. lower--.f64 99.8%

       \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

3. Applied rewrites 99.8%

   \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]
4. Add Preprocessing

Alternative 2: 93.6% accurate, 0.2× speedup

Math

\[\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq 67999999999999999997356342651593264772972582088995194366329756249849399718025586198815286776698430670817592209299575576165557411144388298946043864628100133467138359752110239654230651181165405274112:\\ \;\;\;\;\left(\left|y\right| + \frac{\left(x + z\right) \cdot \left(x - z\right)}{\left|y\right|}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\left|y\right| \cdot \frac{1}{2} - \frac{z}{\frac{\left|y\right| + \left|y\right|}{z}}\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (*
 (copysign 1 y)
 (if (<=
      (fabs y)
      67999999999999999997356342651593264772972582088995194366329756249849399718025586198815286776698430670817592209299575576165557411144388298946043864628100133467138359752110239654230651181165405274112)
   (* (+ (fabs y) (/ (* (+ x z) (- x z)) (fabs y))) 1/2)
   (- (* (fabs y) 1/2) (/ z (/ (+ (fabs y) (fabs y)) z))))))

C

double code(double x, double y, double z) {
	double tmp;
	if (fabs(y) <= 6.8e+196) {
		tmp = (fabs(y) + (((x + z) * (x - z)) / fabs(y))) * 0.5;
	} else {
		tmp = (fabs(y) * 0.5) - (z / ((fabs(y) + fabs(y)) / z));
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double tmp;
	if (Math.abs(y) <= 6.8e+196) {
		tmp = (Math.abs(y) + (((x + z) * (x - z)) / Math.abs(y))) * 0.5;
	} else {
		tmp = (Math.abs(y) * 0.5) - (z / ((Math.abs(y) + Math.abs(y)) / z));
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	tmp = 0
	if math.fabs(y) <= 6.8e+196:
		tmp = (math.fabs(y) + (((x + z) * (x - z)) / math.fabs(y))) * 0.5
	else:
		tmp = (math.fabs(y) * 0.5) - (z / ((math.fabs(y) + math.fabs(y)) / z))
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	tmp = 0.0
	if (abs(y) <= 6.8e+196)
		tmp = Float64(Float64(abs(y) + Float64(Float64(Float64(x + z) * Float64(x - z)) / abs(y))) * 0.5);
	else
		tmp = Float64(Float64(abs(y) * 0.5) - Float64(z / Float64(Float64(abs(y) + abs(y)) / z)));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	tmp = 0.0;
	if (abs(y) <= 6.8e+196)
		tmp = (abs(y) + (((x + z) * (x - z)) / abs(y))) * 0.5;
	else
		tmp = (abs(y) * 0.5) - (z / ((abs(y) + abs(y)) / z));
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 67999999999999999997356342651593264772972582088995194366329756249849399718025586198815286776698430670817592209299575576165557411144388298946043864628100133467138359752110239654230651181165405274112], N[(N[(N[Abs[y], $MachinePrecision] + N[(N[(N[(x + z), $MachinePrecision] * N[(x - z), $MachinePrecision]), $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * 1/2), $MachinePrecision], N[(N[(N[Abs[y], $MachinePrecision] * 1/2), $MachinePrecision] - N[(z / N[(N[(N[Abs[y], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]

Derivation

1. Split input into 2 regimes

2. if y < 6.8e196

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. associate-/r* N/A

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

      4. mult-flip N/A

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

      5. lower-*.f64 N/A

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

   3. Applied rewrites 88.9%

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

   if 6.8e196 < y

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. lift--.f64 N/A

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

      3. div-sub N/A

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

      4. lower--.f64 N/A

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

      5. lift-*.f64 N/A

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

      6. associate-/r* N/A

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

      7. mult-flip N/A

         \[\leadsto \color{blue}{\frac{x \cdot x + y \cdot y}{y} \cdot \frac{1}{2}} - \frac{z \cdot z}{y \cdot 2} \]

      8. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{x \cdot x + y \cdot y}{y} \cdot \frac{1}{2}} - \frac{z \cdot z}{y \cdot 2} \]

      9. lift-+.f64 N/A

         \[\leadsto \frac{\color{blue}{x \cdot x + y \cdot y}}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      10. +-commutative N/A

          \[\leadsto \frac{\color{blue}{y \cdot y + x \cdot x}}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      11. lift-*.f64 N/A

          \[\leadsto \frac{\color{blue}{y \cdot y} + x \cdot x}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      12. add-to-fraction-rev N/A

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

      13. lower-+.f64 N/A

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

      14. lower-/.f64 N/A

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

      15. metadata-eval N/A

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

      16. lift-*.f64 N/A

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

      17. associate-/l* N/A

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

      18. *-commutative N/A

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

      19. lower-*.f64 N/A

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

   3. Applied rewrites 85.8%

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

   4. Taylor expanded in x around 0

      \[\leadsto \color{blue}{y} \cdot \frac{1}{2} - \frac{z}{y + y} \cdot z \]
   5. Step-by-step derivation

   6. Applied rewrites 67.6%

      \[\leadsto \color{blue}{y} \cdot \frac{1}{2} - \frac{z}{y + y} \cdot z \]
   7. Step-by-step derivation

      1. lift-/.f64 N/A

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{z}{y + y}} \cdot z \]

      2. div-flip N/A

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{1}{\frac{y + y}{z}}} \cdot z \]

      3. lower-unsound-/.f64 N/A

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{1}{\frac{y + y}{z}}} \cdot z \]

      4. lower-unsound-/.f64 67.6%

         \[\leadsto y \cdot \frac{1}{2} - \frac{1}{\color{blue}{\frac{y + y}{z}}} \cdot z \]

   8. Applied rewrites 67.6%

      \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{1}{\frac{y + y}{z}}} \cdot z \]
   9. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{1}{\frac{y + y}{z}} \cdot z} \]

      2. *-commutative N/A

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{z \cdot \frac{1}{\frac{y + y}{z}}} \]

      3. lift-/.f64 N/A

         \[\leadsto y \cdot \frac{1}{2} - z \cdot \color{blue}{\frac{1}{\frac{y + y}{z}}} \]

      4. mult-flip-rev N/A

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{z}{\frac{y + y}{z}}} \]

      5. lower-/.f64 67.6%

         \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{z}{\frac{y + y}{z}}} \]

   10. Applied rewrites 67.6%

       \[\leadsto y \cdot \frac{1}{2} - \color{blue}{\frac{z}{\frac{y + y}{z}}} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 93.6% accurate, 0.3× speedup

Math

\[\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq 67999999999999999997356342651593264772972582088995194366329756249849399718025586198815286776698430670817592209299575576165557411144388298946043864628100133467138359752110239654230651181165405274112:\\ \;\;\;\;\left(\left|y\right| + \frac{\left(x + z\right) \cdot \left(x - z\right)}{\left|y\right|}\right) \cdot \frac{1}{2}\\ \mathbf{else}:\\ \;\;\;\;\left|y\right| \cdot \frac{1}{2} - \frac{z}{\left|y\right| + \left|y\right|} \cdot z\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (*
 (copysign 1 y)
 (if (<=
      (fabs y)
      67999999999999999997356342651593264772972582088995194366329756249849399718025586198815286776698430670817592209299575576165557411144388298946043864628100133467138359752110239654230651181165405274112)
   (* (+ (fabs y) (/ (* (+ x z) (- x z)) (fabs y))) 1/2)
   (- (* (fabs y) 1/2) (* (/ z (+ (fabs y) (fabs y))) z)))))

C

double code(double x, double y, double z) {
	double tmp;
	if (fabs(y) <= 6.8e+196) {
		tmp = (fabs(y) + (((x + z) * (x - z)) / fabs(y))) * 0.5;
	} else {
		tmp = (fabs(y) * 0.5) - ((z / (fabs(y) + fabs(y))) * z);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double tmp;
	if (Math.abs(y) <= 6.8e+196) {
		tmp = (Math.abs(y) + (((x + z) * (x - z)) / Math.abs(y))) * 0.5;
	} else {
		tmp = (Math.abs(y) * 0.5) - ((z / (Math.abs(y) + Math.abs(y))) * z);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	tmp = 0
	if math.fabs(y) <= 6.8e+196:
		tmp = (math.fabs(y) + (((x + z) * (x - z)) / math.fabs(y))) * 0.5
	else:
		tmp = (math.fabs(y) * 0.5) - ((z / (math.fabs(y) + math.fabs(y))) * z)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	tmp = 0.0
	if (abs(y) <= 6.8e+196)
		tmp = Float64(Float64(abs(y) + Float64(Float64(Float64(x + z) * Float64(x - z)) / abs(y))) * 0.5);
	else
		tmp = Float64(Float64(abs(y) * 0.5) - Float64(Float64(z / Float64(abs(y) + abs(y))) * z));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	tmp = 0.0;
	if (abs(y) <= 6.8e+196)
		tmp = (abs(y) + (((x + z) * (x - z)) / abs(y))) * 0.5;
	else
		tmp = (abs(y) * 0.5) - ((z / (abs(y) + abs(y))) * z);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 67999999999999999997356342651593264772972582088995194366329756249849399718025586198815286776698430670817592209299575576165557411144388298946043864628100133467138359752110239654230651181165405274112], N[(N[(N[Abs[y], $MachinePrecision] + N[(N[(N[(x + z), $MachinePrecision] * N[(x - z), $MachinePrecision]), $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * 1/2), $MachinePrecision], N[(N[(N[Abs[y], $MachinePrecision] * 1/2), $MachinePrecision] - N[(N[(z / N[(N[Abs[y], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]

Derivation

1. Split input into 2 regimes

2. if y < 6.8e196

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. lift-*.f64 N/A

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

      3. associate-/r* N/A

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

      4. mult-flip N/A

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

      5. lower-*.f64 N/A

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

   3. Applied rewrites 88.9%

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

   if 6.8e196 < y

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. lift--.f64 N/A

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

      3. div-sub N/A

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

      4. lower--.f64 N/A

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

      5. lift-*.f64 N/A

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

      6. associate-/r* N/A

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

      7. mult-flip N/A

         \[\leadsto \color{blue}{\frac{x \cdot x + y \cdot y}{y} \cdot \frac{1}{2}} - \frac{z \cdot z}{y \cdot 2} \]

      8. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{x \cdot x + y \cdot y}{y} \cdot \frac{1}{2}} - \frac{z \cdot z}{y \cdot 2} \]

      9. lift-+.f64 N/A

         \[\leadsto \frac{\color{blue}{x \cdot x + y \cdot y}}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      10. +-commutative N/A

          \[\leadsto \frac{\color{blue}{y \cdot y + x \cdot x}}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      11. lift-*.f64 N/A

          \[\leadsto \frac{\color{blue}{y \cdot y} + x \cdot x}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      12. add-to-fraction-rev N/A

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

      13. lower-+.f64 N/A

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

      14. lower-/.f64 N/A

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

      15. metadata-eval N/A

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

      16. lift-*.f64 N/A

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

      17. associate-/l* N/A

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

      18. *-commutative N/A

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

      19. lower-*.f64 N/A

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

   3. Applied rewrites 85.8%

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

   4. Taylor expanded in x around 0

      \[\leadsto \color{blue}{y} \cdot \frac{1}{2} - \frac{z}{y + y} \cdot z \]
   5. Step-by-step derivation

   6. Applied rewrites 67.6%

      \[\leadsto \color{blue}{y} \cdot \frac{1}{2} - \frac{z}{y + y} \cdot z \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 85.6% accurate, 0.3× speedup

Math

\[\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq 1850000000000000033402373643528915459041328072999225067970158895561157806923972608:\\ \;\;\;\;\frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{\left|y\right|}\right)\\ \mathbf{else}:\\ \;\;\;\;\left|y\right| \cdot \frac{1}{2} - \frac{z}{\left|y\right| + \left|y\right|} \cdot z\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (*
 (copysign 1 y)
 (if (<=
      (fabs y)
      1850000000000000033402373643528915459041328072999225067970158895561157806923972608)
   (* -1/2 (* (- z x) (/ (+ z x) (fabs y))))
   (- (* (fabs y) 1/2) (* (/ z (+ (fabs y) (fabs y))) z)))))

C

double code(double x, double y, double z) {
	double tmp;
	if (fabs(y) <= 1.85e+81) {
		tmp = -0.5 * ((z - x) * ((z + x) / fabs(y)));
	} else {
		tmp = (fabs(y) * 0.5) - ((z / (fabs(y) + fabs(y))) * z);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double tmp;
	if (Math.abs(y) <= 1.85e+81) {
		tmp = -0.5 * ((z - x) * ((z + x) / Math.abs(y)));
	} else {
		tmp = (Math.abs(y) * 0.5) - ((z / (Math.abs(y) + Math.abs(y))) * z);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	tmp = 0
	if math.fabs(y) <= 1.85e+81:
		tmp = -0.5 * ((z - x) * ((z + x) / math.fabs(y)))
	else:
		tmp = (math.fabs(y) * 0.5) - ((z / (math.fabs(y) + math.fabs(y))) * z)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	tmp = 0.0
	if (abs(y) <= 1.85e+81)
		tmp = Float64(-0.5 * Float64(Float64(z - x) * Float64(Float64(z + x) / abs(y))));
	else
		tmp = Float64(Float64(abs(y) * 0.5) - Float64(Float64(z / Float64(abs(y) + abs(y))) * z));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	tmp = 0.0;
	if (abs(y) <= 1.85e+81)
		tmp = -0.5 * ((z - x) * ((z + x) / abs(y)));
	else
		tmp = (abs(y) * 0.5) - ((z / (abs(y) + abs(y))) * z);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 1850000000000000033402373643528915459041328072999225067970158895561157806923972608], N[(-1/2 * N[(N[(z - x), $MachinePrecision] * N[(N[(z + x), $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(N[Abs[y], $MachinePrecision] * 1/2), $MachinePrecision] - N[(N[(z / N[(N[Abs[y], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * z), $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]

Derivation

1. Split input into 2 regimes

2. if y < 1.85e81

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   7. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. associate-*l* N/A

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

      6. lower-*.f64 N/A

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

      7. mult-flip-rev N/A

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

      8. lower-/.f64 66.1%

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

      9. lift-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x + z}{y}\right) \]

      10. +-commutative N/A

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

      11. lower-+.f64 66.1%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

   8. Applied rewrites 66.1%

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

   if 1.85e81 < y

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. lift--.f64 N/A

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

      3. div-sub N/A

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

      4. lower--.f64 N/A

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

      5. lift-*.f64 N/A

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

      6. associate-/r* N/A

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

      7. mult-flip N/A

         \[\leadsto \color{blue}{\frac{x \cdot x + y \cdot y}{y} \cdot \frac{1}{2}} - \frac{z \cdot z}{y \cdot 2} \]

      8. lower-*.f64 N/A

         \[\leadsto \color{blue}{\frac{x \cdot x + y \cdot y}{y} \cdot \frac{1}{2}} - \frac{z \cdot z}{y \cdot 2} \]

      9. lift-+.f64 N/A

         \[\leadsto \frac{\color{blue}{x \cdot x + y \cdot y}}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      10. +-commutative N/A

          \[\leadsto \frac{\color{blue}{y \cdot y + x \cdot x}}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      11. lift-*.f64 N/A

          \[\leadsto \frac{\color{blue}{y \cdot y} + x \cdot x}{y} \cdot \frac{1}{2} - \frac{z \cdot z}{y \cdot 2} \]

      12. add-to-fraction-rev N/A

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

      13. lower-+.f64 N/A

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

      14. lower-/.f64 N/A

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

      15. metadata-eval N/A

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

      16. lift-*.f64 N/A

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

      17. associate-/l* N/A

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

      18. *-commutative N/A

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

      19. lower-*.f64 N/A

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

   3. Applied rewrites 85.8%

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

   4. Taylor expanded in x around 0

      \[\leadsto \color{blue}{y} \cdot \frac{1}{2} - \frac{z}{y + y} \cdot z \]
   5. Step-by-step derivation

   6. Applied rewrites 67.6%

      \[\leadsto \color{blue}{y} \cdot \frac{1}{2} - \frac{z}{y + y} \cdot z \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 80.1% accurate, 0.3× speedup

Math

\[\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960:\\ \;\;\;\;\frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{\left|y\right|}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot \left|y\right|\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (*
 (copysign 1 y)
 (if (<=
      (fabs y)
      11999999999999999830481025428570286999902722740524588088787880837518228612887567400960)
   (* -1/2 (* (- z x) (/ (+ z x) (fabs y))))
   (* 1/2 (fabs y)))))

C

double code(double x, double y, double z) {
	double tmp;
	if (fabs(y) <= 1.2e+85) {
		tmp = -0.5 * ((z - x) * ((z + x) / fabs(y)));
	} else {
		tmp = 0.5 * fabs(y);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double tmp;
	if (Math.abs(y) <= 1.2e+85) {
		tmp = -0.5 * ((z - x) * ((z + x) / Math.abs(y)));
	} else {
		tmp = 0.5 * Math.abs(y);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	tmp = 0
	if math.fabs(y) <= 1.2e+85:
		tmp = -0.5 * ((z - x) * ((z + x) / math.fabs(y)))
	else:
		tmp = 0.5 * math.fabs(y)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	tmp = 0.0
	if (abs(y) <= 1.2e+85)
		tmp = Float64(-0.5 * Float64(Float64(z - x) * Float64(Float64(z + x) / abs(y))));
	else
		tmp = Float64(0.5 * abs(y));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	tmp = 0.0;
	if (abs(y) <= 1.2e+85)
		tmp = -0.5 * ((z - x) * ((z + x) / abs(y)));
	else
		tmp = 0.5 * abs(y);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960], N[(-1/2 * N[(N[(z - x), $MachinePrecision] * N[(N[(z + x), $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1/2 * N[Abs[y], $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]

Derivation

1. Split input into 2 regimes

2. if y < 1.2e85

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   7. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. associate-*l* N/A

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

      6. lower-*.f64 N/A

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

      7. mult-flip-rev N/A

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

      8. lower-/.f64 66.1%

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

      9. lift-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x + z}{y}\right) \]

      10. +-commutative N/A

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

      11. lower-+.f64 66.1%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

   8. Applied rewrites 66.1%

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

   if 1.2e85 < y

   1. Initial program 68.5%

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

   2. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
   3. Step-by-step derivation

      1. lower-*.f64 35.5%

         \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]

   4. Applied rewrites 35.5%

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 6: 78.5% accurate, 0.3× speedup

Math

\[\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960:\\ \;\;\;\;\frac{\left(x - z\right) \cdot \left(z + x\right)}{\left|y\right| + \left|y\right|}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot \left|y\right|\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (*
 (copysign 1 y)
 (if (<=
      (fabs y)
      11999999999999999830481025428570286999902722740524588088787880837518228612887567400960)
   (/ (* (- x z) (+ z x)) (+ (fabs y) (fabs y)))
   (* 1/2 (fabs y)))))

C

double code(double x, double y, double z) {
	double tmp;
	if (fabs(y) <= 1.2e+85) {
		tmp = ((x - z) * (z + x)) / (fabs(y) + fabs(y));
	} else {
		tmp = 0.5 * fabs(y);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double tmp;
	if (Math.abs(y) <= 1.2e+85) {
		tmp = ((x - z) * (z + x)) / (Math.abs(y) + Math.abs(y));
	} else {
		tmp = 0.5 * Math.abs(y);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	tmp = 0
	if math.fabs(y) <= 1.2e+85:
		tmp = ((x - z) * (z + x)) / (math.fabs(y) + math.fabs(y))
	else:
		tmp = 0.5 * math.fabs(y)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	tmp = 0.0
	if (abs(y) <= 1.2e+85)
		tmp = Float64(Float64(Float64(x - z) * Float64(z + x)) / Float64(abs(y) + abs(y)));
	else
		tmp = Float64(0.5 * abs(y));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	tmp = 0.0;
	if (abs(y) <= 1.2e+85)
		tmp = ((x - z) * (z + x)) / (abs(y) + abs(y));
	else
		tmp = 0.5 * abs(y);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960], N[(N[(N[(x - z), $MachinePrecision] * N[(z + x), $MachinePrecision]), $MachinePrecision] / N[(N[Abs[y], $MachinePrecision] + N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1/2 * N[Abs[y], $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]

Derivation

1. Split input into 2 regimes

2. if y < 1.2e85

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lower-*.f64 N/A

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

      5. lift-*.f64 N/A

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

      6. *-commutative N/A

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

      7. associate-/r* N/A

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

      8. lower-/.f64 N/A

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

      9. metadata-eval 68.4%

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

      10. lift--.f64 N/A

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

      11. lift-+.f64 N/A

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

      12. associate--l+ N/A

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

      13. +-commutative N/A

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

      14. associate-+l- N/A

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

      15. lower--.f64 N/A

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

      16. lift-*.f64 N/A

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

      17. lift-*.f64 N/A

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

      18. difference-of-squares N/A

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

      19. lower-*.f64 N/A

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

      20. lower-+.f64 N/A

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

      21. lower--.f64 73.5%

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

   3. Applied rewrites 73.5%

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

   4. Taylor expanded in y around 0

      \[\leadsto \frac{\frac{1}{2}}{y} \cdot \color{blue}{\left(-1 \cdot \left(\left(x + z\right) \cdot \left(z - x\right)\right)\right)} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-*.f64 N/A

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

      3. lower-+.f64 N/A

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

      4. lower--.f64 60.7%

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

   6. Applied rewrites 60.7%

      \[\leadsto \frac{\frac{1}{2}}{y} \cdot \color{blue}{\left(-1 \cdot \left(\left(x + z\right) \cdot \left(z - x\right)\right)\right)} \]
   7. Step-by-step derivation

      1. lift-*.f64 N/A

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

      2. *-commutative N/A

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

      3. lift-/.f64 N/A

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

      4. metadata-eval N/A

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

      5. associate-/r* N/A

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

      6. count-2 N/A

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

      7. lift-+.f64 N/A

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

      8. mult-flip-rev N/A

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

      9. lower-/.f64 60.7%

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

   8. Applied rewrites 60.7%

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

   if 1.2e85 < y

   1. Initial program 68.5%

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

   2. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
   3. Step-by-step derivation

      1. lower-*.f64 35.5%

         \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]

   4. Applied rewrites 35.5%

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 64.7% accurate, 0.2× speedup

Math

\[\begin{array}{l} t_0 := \left|z\right| - \left|x\right|\\ \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq \frac{1162941958872971}{726838724295606890549323807888004534353641360687318060281490199180639288113397923326191050713763565560762521606266177933534601628614656}:\\ \;\;\;\;\left(\frac{t\_0}{\left|y\right|} \cdot \left|z\right|\right) \cdot \frac{-1}{2}\\ \mathbf{elif}\;\left|y\right| \leq 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960:\\ \;\;\;\;\frac{-1}{2} \cdot \left(t\_0 \cdot \frac{\left|x\right|}{\left|y\right|}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot \left|y\right|\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (let* ((t_0 (- (fabs z) (fabs x))))
  (*
   (copysign 1 y)
   (if (<=
        (fabs y)
        1162941958872971/726838724295606890549323807888004534353641360687318060281490199180639288113397923326191050713763565560762521606266177933534601628614656)
     (* (* (/ t_0 (fabs y)) (fabs z)) -1/2)
     (if (<=
          (fabs y)
          11999999999999999830481025428570286999902722740524588088787880837518228612887567400960)
       (* -1/2 (* t_0 (/ (fabs x) (fabs y))))
       (* 1/2 (fabs y)))))))

C

double code(double x, double y, double z) {
	double t_0 = fabs(z) - fabs(x);
	double tmp;
	if (fabs(y) <= 1.6e-120) {
		tmp = ((t_0 / fabs(y)) * fabs(z)) * -0.5;
	} else if (fabs(y) <= 1.2e+85) {
		tmp = -0.5 * (t_0 * (fabs(x) / fabs(y)));
	} else {
		tmp = 0.5 * fabs(y);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double t_0 = Math.abs(z) - Math.abs(x);
	double tmp;
	if (Math.abs(y) <= 1.6e-120) {
		tmp = ((t_0 / Math.abs(y)) * Math.abs(z)) * -0.5;
	} else if (Math.abs(y) <= 1.2e+85) {
		tmp = -0.5 * (t_0 * (Math.abs(x) / Math.abs(y)));
	} else {
		tmp = 0.5 * Math.abs(y);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	t_0 = math.fabs(z) - math.fabs(x)
	tmp = 0
	if math.fabs(y) <= 1.6e-120:
		tmp = ((t_0 / math.fabs(y)) * math.fabs(z)) * -0.5
	elif math.fabs(y) <= 1.2e+85:
		tmp = -0.5 * (t_0 * (math.fabs(x) / math.fabs(y)))
	else:
		tmp = 0.5 * math.fabs(y)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	t_0 = Float64(abs(z) - abs(x))
	tmp = 0.0
	if (abs(y) <= 1.6e-120)
		tmp = Float64(Float64(Float64(t_0 / abs(y)) * abs(z)) * -0.5);
	elseif (abs(y) <= 1.2e+85)
		tmp = Float64(-0.5 * Float64(t_0 * Float64(abs(x) / abs(y))));
	else
		tmp = Float64(0.5 * abs(y));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	t_0 = abs(z) - abs(x);
	tmp = 0.0;
	if (abs(y) <= 1.6e-120)
		tmp = ((t_0 / abs(y)) * abs(z)) * -0.5;
	elseif (abs(y) <= 1.2e+85)
		tmp = -0.5 * (t_0 * (abs(x) / abs(y)));
	else
		tmp = 0.5 * abs(y);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[(N[Abs[z], $MachinePrecision] - N[Abs[x], $MachinePrecision]), $MachinePrecision]}, N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 1162941958872971/726838724295606890549323807888004534353641360687318060281490199180639288113397923326191050713763565560762521606266177933534601628614656], N[(N[(N[(t$95$0 / N[Abs[y], $MachinePrecision]), $MachinePrecision] * N[Abs[z], $MachinePrecision]), $MachinePrecision] * -1/2), $MachinePrecision], If[LessEqual[N[Abs[y], $MachinePrecision], 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960], N[(-1/2 * N[(t$95$0 * N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1/2 * N[Abs[y], $MachinePrecision]), $MachinePrecision]]]), $MachinePrecision]]

Derivation

1. Split input into 3 regimes

2. if y < 1.6e-120

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

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

   7. Taylor expanded in x around 0

      \[\leadsto \frac{-1}{2} \cdot \frac{z \cdot \left(z - x\right)}{y} \]
   8. Step-by-step derivation

   9. Applied rewrites 35.1%

      \[\leadsto \frac{-1}{2} \cdot \frac{z \cdot \left(z - x\right)}{y} \]
   10. Step-by-step derivation

       1. lift-*.f64 N/A

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

       2. *-commutative N/A

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

       3. lower-*.f64 35.1%

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

       4. lift-/.f64 N/A

          \[\leadsto \frac{z \cdot \left(z - x\right)}{y} \cdot \frac{-1}{2} \]

       5. lift-*.f64 N/A

          \[\leadsto \frac{z \cdot \left(z - x\right)}{y} \cdot \frac{-1}{2} \]

       6. associate-/l* N/A

          \[\leadsto \left(z \cdot \frac{z - x}{y}\right) \cdot \frac{-1}{2} \]

       7. *-commutative N/A

          \[\leadsto \left(\frac{z - x}{y} \cdot z\right) \cdot \frac{-1}{2} \]

       8. lower-*.f64 N/A

          \[\leadsto \left(\frac{z - x}{y} \cdot z\right) \cdot \frac{-1}{2} \]

       9. lower-/.f64 39.8%

          \[\leadsto \left(\frac{z - x}{y} \cdot z\right) \cdot \frac{-1}{2} \]

   11. Applied rewrites 39.8%

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

   if 1.6e-120 < y < 1.2e85

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   7. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. associate-*l* N/A

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

      6. lower-*.f64 N/A

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

      7. mult-flip-rev N/A

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

      8. lower-/.f64 66.1%

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

      9. lift-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x + z}{y}\right) \]

      10. +-commutative N/A

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

      11. lower-+.f64 66.1%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

   8. Applied rewrites 66.1%

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

   9. Taylor expanded in x around inf

      \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x}{\color{blue}{y}}\right) \]
   10. Step-by-step derivation

       1. lower-/.f64 38.2%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x}{y}\right) \]

   11. Applied rewrites 38.2%

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

   if 1.2e85 < y

   1. Initial program 68.5%

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

   2. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
   3. Step-by-step derivation

      1. lower-*.f64 35.5%

         \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]

   4. Applied rewrites 35.5%

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 8: 61.8% accurate, 0.2× speedup

Math

\[\begin{array}{l} t_0 := \left|z\right| - \left|x\right|\\ \mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq \frac{1804760880651433}{97554642197374757230674913431036447054643691958280348464348654988292866838117675628759565720734124098744591597543956965482749239977758915821568}:\\ \;\;\;\;\frac{-1}{2} \cdot \frac{\left|z\right| \cdot t\_0}{\left|y\right|}\\ \mathbf{elif}\;\left|y\right| \leq 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960:\\ \;\;\;\;\frac{-1}{2} \cdot \left(t\_0 \cdot \frac{\left|x\right|}{\left|y\right|}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot \left|y\right|\\ \end{array} \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (let* ((t_0 (- (fabs z) (fabs x))))
  (*
   (copysign 1 y)
   (if (<=
        (fabs y)
        1804760880651433/97554642197374757230674913431036447054643691958280348464348654988292866838117675628759565720734124098744591597543956965482749239977758915821568)
     (* -1/2 (/ (* (fabs z) t_0) (fabs y)))
     (if (<=
          (fabs y)
          11999999999999999830481025428570286999902722740524588088787880837518228612887567400960)
       (* -1/2 (* t_0 (/ (fabs x) (fabs y))))
       (* 1/2 (fabs y)))))))

C

double code(double x, double y, double z) {
	double t_0 = fabs(z) - fabs(x);
	double tmp;
	if (fabs(y) <= 1.85e-128) {
		tmp = -0.5 * ((fabs(z) * t_0) / fabs(y));
	} else if (fabs(y) <= 1.2e+85) {
		tmp = -0.5 * (t_0 * (fabs(x) / fabs(y)));
	} else {
		tmp = 0.5 * fabs(y);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double t_0 = Math.abs(z) - Math.abs(x);
	double tmp;
	if (Math.abs(y) <= 1.85e-128) {
		tmp = -0.5 * ((Math.abs(z) * t_0) / Math.abs(y));
	} else if (Math.abs(y) <= 1.2e+85) {
		tmp = -0.5 * (t_0 * (Math.abs(x) / Math.abs(y)));
	} else {
		tmp = 0.5 * Math.abs(y);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	t_0 = math.fabs(z) - math.fabs(x)
	tmp = 0
	if math.fabs(y) <= 1.85e-128:
		tmp = -0.5 * ((math.fabs(z) * t_0) / math.fabs(y))
	elif math.fabs(y) <= 1.2e+85:
		tmp = -0.5 * (t_0 * (math.fabs(x) / math.fabs(y)))
	else:
		tmp = 0.5 * math.fabs(y)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	t_0 = Float64(abs(z) - abs(x))
	tmp = 0.0
	if (abs(y) <= 1.85e-128)
		tmp = Float64(-0.5 * Float64(Float64(abs(z) * t_0) / abs(y)));
	elseif (abs(y) <= 1.2e+85)
		tmp = Float64(-0.5 * Float64(t_0 * Float64(abs(x) / abs(y))));
	else
		tmp = Float64(0.5 * abs(y));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	t_0 = abs(z) - abs(x);
	tmp = 0.0;
	if (abs(y) <= 1.85e-128)
		tmp = -0.5 * ((abs(z) * t_0) / abs(y));
	elseif (abs(y) <= 1.2e+85)
		tmp = -0.5 * (t_0 * (abs(x) / abs(y)));
	else
		tmp = 0.5 * abs(y);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := Block[{t$95$0 = N[(N[Abs[z], $MachinePrecision] - N[Abs[x], $MachinePrecision]), $MachinePrecision]}, N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 1804760880651433/97554642197374757230674913431036447054643691958280348464348654988292866838117675628759565720734124098744591597543956965482749239977758915821568], N[(-1/2 * N[(N[(N[Abs[z], $MachinePrecision] * t$95$0), $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[N[Abs[y], $MachinePrecision], 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960], N[(-1/2 * N[(t$95$0 * N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1/2 * N[Abs[y], $MachinePrecision]), $MachinePrecision]]]), $MachinePrecision]]

Derivation

1. Split input into 3 regimes

2. if y < 1.85e-128

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

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

   7. Taylor expanded in x around 0

      \[\leadsto \frac{-1}{2} \cdot \frac{z \cdot \left(z - x\right)}{y} \]
   8. Step-by-step derivation

   9. Applied rewrites 35.1%

      \[\leadsto \frac{-1}{2} \cdot \frac{z \cdot \left(z - x\right)}{y} \]

   if 1.85e-128 < y < 1.2e85

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   7. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. associate-*l* N/A

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

      6. lower-*.f64 N/A

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

      7. mult-flip-rev N/A

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

      8. lower-/.f64 66.1%

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

      9. lift-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x + z}{y}\right) \]

      10. +-commutative N/A

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

      11. lower-+.f64 66.1%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

   8. Applied rewrites 66.1%

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

   9. Taylor expanded in x around inf

      \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x}{\color{blue}{y}}\right) \]
   10. Step-by-step derivation

       1. lower-/.f64 38.2%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x}{y}\right) \]

   11. Applied rewrites 38.2%

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

   if 1.2e85 < y

   1. Initial program 68.5%

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

   2. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
   3. Step-by-step derivation

      1. lower-*.f64 35.5%

         \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]

   4. Applied rewrites 35.5%

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 9: 60.9% accurate, 0.3× speedup

Math

\[\mathsf{copysign}\left(1, y\right) \cdot \begin{array}{l} \mathbf{if}\;\left|y\right| \leq 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960:\\ \;\;\;\;\frac{-1}{2} \cdot \left(\left(\left|z\right| - \left|x\right|\right) \cdot \frac{\left|x\right|}{\left|y\right|}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{2} \cdot \left|y\right|\\ \end{array} \]

FPCore

(FPCore (x y z)
  :precision binary64
  (*
 (copysign 1 y)
 (if (<=
      (fabs y)
      11999999999999999830481025428570286999902722740524588088787880837518228612887567400960)
   (* -1/2 (* (- (fabs z) (fabs x)) (/ (fabs x) (fabs y))))
   (* 1/2 (fabs y)))))

C

double code(double x, double y, double z) {
	double tmp;
	if (fabs(y) <= 1.2e+85) {
		tmp = -0.5 * ((fabs(z) - fabs(x)) * (fabs(x) / fabs(y)));
	} else {
		tmp = 0.5 * fabs(y);
	}
	return copysign(1.0, y) * tmp;
}

Java

public static double code(double x, double y, double z) {
	double tmp;
	if (Math.abs(y) <= 1.2e+85) {
		tmp = -0.5 * ((Math.abs(z) - Math.abs(x)) * (Math.abs(x) / Math.abs(y)));
	} else {
		tmp = 0.5 * Math.abs(y);
	}
	return Math.copySign(1.0, y) * tmp;
}

Python

def code(x, y, z):
	tmp = 0
	if math.fabs(y) <= 1.2e+85:
		tmp = -0.5 * ((math.fabs(z) - math.fabs(x)) * (math.fabs(x) / math.fabs(y)))
	else:
		tmp = 0.5 * math.fabs(y)
	return math.copysign(1.0, y) * tmp

Julia

function code(x, y, z)
	tmp = 0.0
	if (abs(y) <= 1.2e+85)
		tmp = Float64(-0.5 * Float64(Float64(abs(z) - abs(x)) * Float64(abs(x) / abs(y))));
	else
		tmp = Float64(0.5 * abs(y));
	end
	return Float64(copysign(1.0, y) * tmp)
end

MATLAB

function tmp_2 = code(x, y, z)
	tmp = 0.0;
	if (abs(y) <= 1.2e+85)
		tmp = -0.5 * ((abs(z) - abs(x)) * (abs(x) / abs(y)));
	else
		tmp = 0.5 * abs(y);
	end
	tmp_2 = (sign(y) * abs(1.0)) * tmp;
end

Wolfram

code[x_, y_, z_] := N[(N[With[{TMP1 = Abs[1], TMP2 = Sign[y]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision] * If[LessEqual[N[Abs[y], $MachinePrecision], 11999999999999999830481025428570286999902722740524588088787880837518228612887567400960], N[(-1/2 * N[(N[(N[Abs[z], $MachinePrecision] - N[Abs[x], $MachinePrecision]), $MachinePrecision] * N[(N[Abs[x], $MachinePrecision] / N[Abs[y], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(1/2 * N[Abs[y], $MachinePrecision]), $MachinePrecision]]), $MachinePrecision]

Derivation

1. Split input into 2 regimes

2. if y < 1.2e85

   1. Initial program 68.5%

      \[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
   2. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. *-commutative N/A

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

      4. lift--.f64 N/A

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

      5. lift-+.f64 N/A

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

      6. +-commutative N/A

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

      7. associate--l+ N/A

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

      8. add-flip N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \color{blue}{\left(y \cdot y - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right)} \]

      9. lift-*.f64 N/A

         \[\leadsto \frac{1}{y \cdot 2} \cdot \left(\color{blue}{y \cdot y} - \left(\mathsf{neg}\left(\left(x \cdot x - z \cdot z\right)\right)\right)\right) \]

      10. sub-negate-rev N/A

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

      11. lift-*.f64 N/A

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

      12. lift-*.f64 N/A

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

      13. difference-of-squares N/A

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

      14. lower-134-z0z1z2z3z4 N/A

          \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{y \cdot 2}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

      15. lift-*.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{y \cdot 2}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      16. *-commutative N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{1}{\color{blue}{2 \cdot y}}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      17. associate-/r* N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      18. lower-/.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\color{blue}{\left(\frac{\frac{1}{2}}{y}\right)}, y, y, \left(z + x\right), \left(z - x\right)\right) \]

      19. metadata-eval N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\color{blue}{\frac{1}{2}}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right) \]

      20. lower-+.f64 N/A

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \color{blue}{\left(z + x\right)}, \left(z - x\right)\right) \]

      21. lower--.f64 99.8%

          \[\leadsto \mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \color{blue}{\left(z - x\right)}\right) \]

   3. Applied rewrites 99.8%

      \[\leadsto \color{blue}{\mathsf{134\_z0z1z2z3z4}\left(\left(\frac{\frac{1}{2}}{y}\right), y, y, \left(z + x\right), \left(z - x\right)\right)} \]

   4. Taylor expanded in y around 0

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   5. Step-by-step derivation

      1. lower-*.f64 N/A

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

      2. lower-/.f64 N/A

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

      3. lower-*.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      4. lower-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

      5. lower--.f64 60.7%

         \[\leadsto \frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y} \]

   6. Applied rewrites 60.7%

      \[\leadsto \color{blue}{\frac{-1}{2} \cdot \frac{\left(x + z\right) \cdot \left(z - x\right)}{y}} \]
   7. Step-by-step derivation

      1. lift-/.f64 N/A

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

      2. mult-flip N/A

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

      3. lift-*.f64 N/A

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

      4. *-commutative N/A

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

      5. associate-*l* N/A

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

      6. lower-*.f64 N/A

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

      7. mult-flip-rev N/A

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

      8. lower-/.f64 66.1%

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

      9. lift-+.f64 N/A

         \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x + z}{y}\right) \]

      10. +-commutative N/A

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

      11. lower-+.f64 66.1%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{z + x}{y}\right) \]

   8. Applied rewrites 66.1%

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

   9. Taylor expanded in x around inf

      \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x}{\color{blue}{y}}\right) \]
   10. Step-by-step derivation

       1. lower-/.f64 38.2%

          \[\leadsto \frac{-1}{2} \cdot \left(\left(z - x\right) \cdot \frac{x}{y}\right) \]

   11. Applied rewrites 38.2%

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

   if 1.2e85 < y

   1. Initial program 68.5%

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

   2. Taylor expanded in y around inf

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
   3. Step-by-step derivation

      1. lower-*.f64 35.5%

         \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]

   4. Applied rewrites 35.5%

      \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 10: 35.5% accurate, 6.3× speedup

Math

\[\frac{1}{2} \cdot y \]

FPCore

(FPCore (x y z)
  :precision binary64
  (* 1/2 y))

C

double code(double x, double y, double z) {
	return 0.5 * y;
}

Fortran

module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(x, y, z)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    code = 0.5d0 * y
end function

Java

public static double code(double x, double y, double z) {
	return 0.5 * y;
}

Python

def code(x, y, z):
	return 0.5 * y

Julia

function code(x, y, z)
	return Float64(0.5 * y)
end

MATLAB

function tmp = code(x, y, z)
	tmp = 0.5 * y;
end

Wolfram

code[x_, y_, z_] := N[(1/2 * y), $MachinePrecision]

Derivation

1. Initial program 68.5%

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

2. Taylor expanded in y around inf

   \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
3. Step-by-step derivation

   1. lower-*.f64 35.5%

      \[\leadsto \frac{1}{2} \cdot \color{blue}{y} \]

4. Applied rewrites 35.5%

   \[\leadsto \color{blue}{\frac{1}{2} \cdot y} \]
5. Add Preprocessing

Reproduce

herbie shell --seed 2025271 -o generate:evaluate
(FPCore (x y z)
  :name "Diagrams.TwoD.Apollonian:initialConfig from diagrams-contrib-1.3.0.5, A"
  :precision binary64
  (/ (- (+ (* x x) (* y y)) (* z z)) (* y 2)))