Linear.V3:$cdot from linear-1.19.1.3, B

Percentage Accurate: 97.7% → 98.9%

Time: 1.6s

Alternatives: 7

Speedup: 1.1×

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

Specification

Math

\[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (+ (+ (* x y) (* z t)) (* a b)))

C

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

Fortran

real(8) function code(x, y, z, t, a, b)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = ((x * y) + (z * t)) + (a * b)
end function

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	((x * y) + (z * t)) + (a * b)
END code

Initial Program: 97.7% accurate, 1.0× speedup

Math

\[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (+ (+ (* x y) (* z t)) (* a b)))

C

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

Fortran

real(8) function code(x, y, z, t, a, b)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = ((x * y) + (z * t)) + (a * b)
end function

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

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

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	((x * y) + (z * t)) + (a * b)
END code

Alternative 1: 98.9% accurate, 1.1× speedup

Math

\[\mathsf{fma}\left(t, z, \mathsf{fma}\left(b, a, y \cdot x\right)\right) \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (fma t z (fma b a (* y x))))

C

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

Julia

function code(x, y, z, t, a, b)
	return fma(t, z, fma(b, a, Float64(y * x)))
end

Wolfram

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

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	(t * z) + ((b * a) + (y * x))
END code

Derivation

1. Initial program 97.7%

   \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]
2. Step-by-step derivation

3. Applied rewrites 98.9%

   \[\leadsto \mathsf{fma}\left(t, z, \mathsf{fma}\left(b, a, y \cdot x\right)\right) \]
4. Add Preprocessing

Alternative 2: 85.6% accurate, 0.7× speedup

Math

\[\begin{array}{l} t_1 := \mathsf{fma}\left(a, b, x \cdot y\right)\\ \mathbf{if}\;a \cdot b \leq -4 \cdot 10^{+29}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;a \cdot b \leq 5 \cdot 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(t, z, x \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (let* ((t_1 (fma a b (* x y))))
  (if (<= (* a b) -4e+29)
    t_1
    (if (<= (* a b) 5e-9) (fma t z (* x y)) t_1))))

C

double code(double x, double y, double z, double t, double a, double b) {
	double t_1 = fma(a, b, (x * y));
	double tmp;
	if ((a * b) <= -4e+29) {
		tmp = t_1;
	} else if ((a * b) <= 5e-9) {
		tmp = fma(t, z, (x * y));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Julia

function code(x, y, z, t, a, b)
	t_1 = fma(a, b, Float64(x * y))
	tmp = 0.0
	if (Float64(a * b) <= -4e+29)
		tmp = t_1;
	elseif (Float64(a * b) <= 5e-9)
		tmp = fma(t, z, Float64(x * y));
	else
		tmp = t_1;
	end
	return tmp
end

Wolfram

code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(a * b + N[(x * y), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(a * b), $MachinePrecision], -4e+29], t$95$1, If[LessEqual[N[(a * b), $MachinePrecision], 5e-9], N[(t * z + N[(x * y), $MachinePrecision]), $MachinePrecision], t$95$1]]]

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	LET t_1 = ((a * b) + (x * y)) IN
		LET tmp_1 = IF ((a * b) <= (50000000000000001046128041506423633766331704464391805231571197509765625e-79)) THEN ((t * z) + (x * y)) ELSE t_1 ENDIF IN
		LET tmp = IF ((a * b) <= (-399999999999999965732603428864)) THEN t_1 ELSE tmp_1 ENDIF IN
	tmp
END code

Derivation

1. Split input into 2 regimes

2. if (*.f64 a b) < -3.9999999999999997e29 or 5.0000000000000001e-9 < (*.f64 a b)

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in z around 0

      \[\leadsto a \cdot b + x \cdot y \]
   3. Step-by-step derivation

   4. Applied rewrites 66.9%

      \[\leadsto \mathsf{fma}\left(a, b, x \cdot y\right) \]

   if -3.9999999999999997e29 < (*.f64 a b) < 5.0000000000000001e-9

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]

   5. Taylor expanded in a around 0

      \[\leadsto t \cdot z + x \cdot y \]
   6. Step-by-step derivation

   7. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(t, z, x \cdot y\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 84.8% accurate, 0.7× speedup

Math

\[\begin{array}{l} t_1 := \mathsf{fma}\left(a, b, x \cdot y\right)\\ \mathbf{if}\;x \cdot y \leq -1.2267604479272654 \cdot 10^{+132}:\\ \;\;\;\;t\_1\\ \mathbf{elif}\;x \cdot y \leq 1.0443453315373454 \cdot 10^{+20}:\\ \;\;\;\;\mathsf{fma}\left(a, b, t \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (let* ((t_1 (fma a b (* x y))))
  (if (<= (* x y) -1.2267604479272654e+132)
    t_1
    (if (<= (* x y) 1.0443453315373454e+20) (fma a b (* t z)) t_1))))

C

double code(double x, double y, double z, double t, double a, double b) {
	double t_1 = fma(a, b, (x * y));
	double tmp;
	if ((x * y) <= -1.2267604479272654e+132) {
		tmp = t_1;
	} else if ((x * y) <= 1.0443453315373454e+20) {
		tmp = fma(a, b, (t * z));
	} else {
		tmp = t_1;
	}
	return tmp;
}

Julia

function code(x, y, z, t, a, b)
	t_1 = fma(a, b, Float64(x * y))
	tmp = 0.0
	if (Float64(x * y) <= -1.2267604479272654e+132)
		tmp = t_1;
	elseif (Float64(x * y) <= 1.0443453315373454e+20)
		tmp = fma(a, b, Float64(t * z));
	else
		tmp = t_1;
	end
	return tmp
end

Wolfram

code[x_, y_, z_, t_, a_, b_] := Block[{t$95$1 = N[(a * b + N[(x * y), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(x * y), $MachinePrecision], -1.2267604479272654e+132], t$95$1, If[LessEqual[N[(x * y), $MachinePrecision], 1.0443453315373454e+20], N[(a * b + N[(t * z), $MachinePrecision]), $MachinePrecision], t$95$1]]]

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	LET t_1 = ((a * b) + (x * y)) IN
		LET tmp_1 = IF ((x * y) <= (104434533153734541312)) THEN ((a * b) + (t * z)) ELSE t_1 ENDIF IN
		LET tmp = IF ((x * y) <= (-1226760447927265410168051942599317556772775447675469359741590955268777242255271679108502107488085224326089347671198066563088014901248)) THEN t_1 ELSE tmp_1 ENDIF IN
	tmp
END code

Derivation

1. Split input into 2 regimes

2. if (*.f64 x y) < -1.2267604479272654e132 or 104434533153734540000 < (*.f64 x y)

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in z around 0

      \[\leadsto a \cdot b + x \cdot y \]
   3. Step-by-step derivation

   4. Applied rewrites 66.9%

      \[\leadsto \mathsf{fma}\left(a, b, x \cdot y\right) \]

   if -1.2267604479272654e132 < (*.f64 x y) < 104434533153734540000

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 81.2% accurate, 0.7× speedup

Math

\[\begin{array}{l} \mathbf{if}\;x \cdot y \leq -2.4922992158218926 \cdot 10^{+170}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq 2.7964532433725382 \cdot 10^{+163}:\\ \;\;\;\;\mathsf{fma}\left(a, b, t \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (if (<= (* x y) -2.4922992158218926e+170)
  (* x y)
  (if (<= (* x y) 2.7964532433725382e+163) (fma a b (* t z)) (* x y))))

C

double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if ((x * y) <= -2.4922992158218926e+170) {
		tmp = x * y;
	} else if ((x * y) <= 2.7964532433725382e+163) {
		tmp = fma(a, b, (t * z));
	} else {
		tmp = x * y;
	}
	return tmp;
}

Julia

function code(x, y, z, t, a, b)
	tmp = 0.0
	if (Float64(x * y) <= -2.4922992158218926e+170)
		tmp = Float64(x * y);
	elseif (Float64(x * y) <= 2.7964532433725382e+163)
		tmp = fma(a, b, Float64(t * z));
	else
		tmp = Float64(x * y);
	end
	return tmp
end

Wolfram

code[x_, y_, z_, t_, a_, b_] := If[LessEqual[N[(x * y), $MachinePrecision], -2.4922992158218926e+170], N[(x * y), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 2.7964532433725382e+163], N[(a * b + N[(t * z), $MachinePrecision]), $MachinePrecision], N[(x * y), $MachinePrecision]]]

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	LET tmp_1 = IF ((x * y) <= (27964532433725381743030882621215790283214343602816830094284557029197059376725915606887128744428023393142538870652277238721278308444581385862962517006497736162279424)) THEN ((a * b) + (t * z)) ELSE (x * y) ENDIF IN
	LET tmp = IF ((x * y) <= (-249229921582189255583550949406746638606628457137436858294643921299305127200719576508581922098678911436022899524427197250795402921061674798626459017389758632466348114968576)) THEN (x * y) ELSE tmp_1 ENDIF IN
	tmp
END code

Derivation

1. Split input into 2 regimes

2. if (*.f64 x y) < -2.4922992158218926e170 or 2.7964532433725382e163 < (*.f64 x y)

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]

   5. Taylor expanded in a around 0

      \[\leadsto t \cdot z + x \cdot y \]
   6. Step-by-step derivation

   7. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(t, z, x \cdot y\right) \]
   8. Step-by-step derivation

   9. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(x, y, t \cdot z\right) \]

   10. Taylor expanded in x around inf

       \[\leadsto x \cdot y \]
   11. Step-by-step derivation

   12. Applied rewrites 35.5%

       \[\leadsto x \cdot y \]

   if -2.4922992158218926e170 < (*.f64 x y) < 2.7964532433725382e163

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 5: 53.3% accurate, 0.6× speedup

Math

\[\begin{array}{l} \mathbf{if}\;x \cdot y \leq -8.208530573544229 \cdot 10^{+151}:\\ \;\;\;\;x \cdot y\\ \mathbf{elif}\;x \cdot y \leq 4.420125233190628 \cdot 10^{-286}:\\ \;\;\;\;t \cdot z\\ \mathbf{elif}\;x \cdot y \leq 2762318762360.2886:\\ \;\;\;\;a \cdot b\\ \mathbf{else}:\\ \;\;\;\;x \cdot y\\ \end{array} \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (if (<= (* x y) -8.208530573544229e+151)
  (* x y)
  (if (<= (* x y) 4.420125233190628e-286)
    (* t z)
    (if (<= (* x y) 2762318762360.2886) (* a b) (* x y)))))

C

double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if ((x * y) <= -8.208530573544229e+151) {
		tmp = x * y;
	} else if ((x * y) <= 4.420125233190628e-286) {
		tmp = t * z;
	} else if ((x * y) <= 2762318762360.2886) {
		tmp = a * b;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    real(8) :: tmp
    if ((x * y) <= (-8.208530573544229d+151)) then
        tmp = x * y
    else if ((x * y) <= 4.420125233190628d-286) then
        tmp = t * z
    else if ((x * y) <= 2762318762360.2886d0) then
        tmp = a * b
    else
        tmp = x * y
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if ((x * y) <= -8.208530573544229e+151) {
		tmp = x * y;
	} else if ((x * y) <= 4.420125233190628e-286) {
		tmp = t * z;
	} else if ((x * y) <= 2762318762360.2886) {
		tmp = a * b;
	} else {
		tmp = x * y;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b):
	tmp = 0
	if (x * y) <= -8.208530573544229e+151:
		tmp = x * y
	elif (x * y) <= 4.420125233190628e-286:
		tmp = t * z
	elif (x * y) <= 2762318762360.2886:
		tmp = a * b
	else:
		tmp = x * y
	return tmp

Julia

function code(x, y, z, t, a, b)
	tmp = 0.0
	if (Float64(x * y) <= -8.208530573544229e+151)
		tmp = Float64(x * y);
	elseif (Float64(x * y) <= 4.420125233190628e-286)
		tmp = Float64(t * z);
	elseif (Float64(x * y) <= 2762318762360.2886)
		tmp = Float64(a * b);
	else
		tmp = Float64(x * y);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b)
	tmp = 0.0;
	if ((x * y) <= -8.208530573544229e+151)
		tmp = x * y;
	elseif ((x * y) <= 4.420125233190628e-286)
		tmp = t * z;
	elseif ((x * y) <= 2762318762360.2886)
		tmp = a * b;
	else
		tmp = x * y;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_] := If[LessEqual[N[(x * y), $MachinePrecision], -8.208530573544229e+151], N[(x * y), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 4.420125233190628e-286], N[(t * z), $MachinePrecision], If[LessEqual[N[(x * y), $MachinePrecision], 2762318762360.2886], N[(a * b), $MachinePrecision], N[(x * y), $MachinePrecision]]]]

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	LET tmp_2 = IF ((x * y) <= (276231876236028857421875e-11)) THEN (a * b) ELSE (x * y) ENDIF IN
	LET tmp_1 = IF ((x * y) <= (4420125233190628131423912265133010405834708279824358996171251547074654588017894215742486232427748921109751458069153589511587837637077443290463045430524413161149067379620528379654472704867347255685212446181238998110399674195680601292130854974294475530935962074161676096179836316509061523911958532126803648434874806175086518174243043405703164234818837585929736779562855302015453806457493483004044928528711051545108895454905301934577341203271639773475196102249222801116422636388467754925349531588378634924524477172403314015331640283468010710199541772367388840691001170336824342693371273308628796702871748318933235927846828705193319317913470260713954357468231159240104639551673278152765789172917720861732959747314453125e-1000)) THEN (t * z) ELSE tmp_2 ENDIF IN
	LET tmp = IF ((x * y) <= (-82085305735442293477548981116398509254011320577038340037718978130376341868949208881701170449743558859101867893845891515553885947001471416687171326705664)) THEN (x * y) ELSE tmp_1 ENDIF IN
	tmp
END code

Derivation

1. Split input into 3 regimes

2. if (*.f64 x y) < -8.2085305735442293e151 or 2762318762360.2886 < (*.f64 x y)

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]

   5. Taylor expanded in a around 0

      \[\leadsto t \cdot z + x \cdot y \]
   6. Step-by-step derivation

   7. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(t, z, x \cdot y\right) \]
   8. Step-by-step derivation

   9. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(x, y, t \cdot z\right) \]

   10. Taylor expanded in x around inf

       \[\leadsto x \cdot y \]
   11. Step-by-step derivation

   12. Applied rewrites 35.5%

       \[\leadsto x \cdot y \]

   if -8.2085305735442293e151 < (*.f64 x y) < 4.4201252331906281e-286

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]

   5. Taylor expanded in a around 0

      \[\leadsto t \cdot z + x \cdot y \]
   6. Step-by-step derivation

   7. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(t, z, x \cdot y\right) \]

   8. Taylor expanded in x around 0

      \[\leadsto t \cdot z \]
   9. Step-by-step derivation

   10. Applied rewrites 36.0%

       \[\leadsto t \cdot z \]

   if 4.4201252331906281e-286 < (*.f64 x y) < 2762318762360.2886

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in z around 0

      \[\leadsto a \cdot b + x \cdot y \]
   3. Step-by-step derivation

   4. Applied rewrites 66.9%

      \[\leadsto \mathsf{fma}\left(a, b, x \cdot y\right) \]

   5. Taylor expanded in x around 0

      \[\leadsto a \cdot b \]
   6. Step-by-step derivation

   7. Applied rewrites 34.8%

      \[\leadsto a \cdot b \]
3. Recombined 3 regimes into one program.
4. Add Preprocessing

Alternative 6: 53.0% accurate, 0.9× speedup

Math

\[\begin{array}{l} \mathbf{if}\;a \cdot b \leq -1.581414972194181 \cdot 10^{+149}:\\ \;\;\;\;a \cdot b\\ \mathbf{elif}\;a \cdot b \leq 762.4978094571832:\\ \;\;\;\;t \cdot z\\ \mathbf{else}:\\ \;\;\;\;a \cdot b\\ \end{array} \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (if (<= (* a b) -1.581414972194181e+149)
  (* a b)
  (if (<= (* a b) 762.4978094571832) (* t z) (* a b))))

C

double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if ((a * b) <= -1.581414972194181e+149) {
		tmp = a * b;
	} else if ((a * b) <= 762.4978094571832) {
		tmp = t * z;
	} else {
		tmp = a * b;
	}
	return tmp;
}

Fortran

real(8) function code(x, y, z, t, a, b)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    real(8) :: tmp
    if ((a * b) <= (-1.581414972194181d+149)) then
        tmp = a * b
    else if ((a * b) <= 762.4978094571832d0) then
        tmp = t * z
    else
        tmp = a * b
    end if
    code = tmp
end function

Java

public static double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if ((a * b) <= -1.581414972194181e+149) {
		tmp = a * b;
	} else if ((a * b) <= 762.4978094571832) {
		tmp = t * z;
	} else {
		tmp = a * b;
	}
	return tmp;
}

Python

def code(x, y, z, t, a, b):
	tmp = 0
	if (a * b) <= -1.581414972194181e+149:
		tmp = a * b
	elif (a * b) <= 762.4978094571832:
		tmp = t * z
	else:
		tmp = a * b
	return tmp

Julia

function code(x, y, z, t, a, b)
	tmp = 0.0
	if (Float64(a * b) <= -1.581414972194181e+149)
		tmp = Float64(a * b);
	elseif (Float64(a * b) <= 762.4978094571832)
		tmp = Float64(t * z);
	else
		tmp = Float64(a * b);
	end
	return tmp
end

MATLAB

function tmp_2 = code(x, y, z, t, a, b)
	tmp = 0.0;
	if ((a * b) <= -1.581414972194181e+149)
		tmp = a * b;
	elseif ((a * b) <= 762.4978094571832)
		tmp = t * z;
	else
		tmp = a * b;
	end
	tmp_2 = tmp;
end

Wolfram

code[x_, y_, z_, t_, a_, b_] := If[LessEqual[N[(a * b), $MachinePrecision], -1.581414972194181e+149], N[(a * b), $MachinePrecision], If[LessEqual[N[(a * b), $MachinePrecision], 762.4978094571832], N[(t * z), $MachinePrecision], N[(a * b), $MachinePrecision]]]

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	LET tmp_1 = IF ((a * b) <= (762497809457183166159666143357753753662109375e-42)) THEN (t * z) ELSE (a * b) ENDIF IN
	LET tmp = IF ((a * b) <= (-158141497219418101452136639324165613452360734511951917448657143747372265127962552404497376881770038521206320724156666344909610389158610148053363982336)) THEN (a * b) ELSE tmp_1 ENDIF IN
	tmp
END code

Derivation

1. Split input into 2 regimes

2. if (*.f64 a b) < -1.581414972194181e149 or 762.49780945718317 < (*.f64 a b)

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in z around 0

      \[\leadsto a \cdot b + x \cdot y \]
   3. Step-by-step derivation

   4. Applied rewrites 66.9%

      \[\leadsto \mathsf{fma}\left(a, b, x \cdot y\right) \]

   5. Taylor expanded in x around 0

      \[\leadsto a \cdot b \]
   6. Step-by-step derivation

   7. Applied rewrites 34.8%

      \[\leadsto a \cdot b \]

   if -1.581414972194181e149 < (*.f64 a b) < 762.49780945718317

   1. Initial program 97.7%

      \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

   2. Taylor expanded in x around 0

      \[\leadsto a \cdot b + t \cdot z \]
   3. Step-by-step derivation

   4. Applied rewrites 67.4%

      \[\leadsto \mathsf{fma}\left(a, b, t \cdot z\right) \]

   5. Taylor expanded in a around 0

      \[\leadsto t \cdot z + x \cdot y \]
   6. Step-by-step derivation

   7. Applied rewrites 68.2%

      \[\leadsto \mathsf{fma}\left(t, z, x \cdot y\right) \]

   8. Taylor expanded in x around 0

      \[\leadsto t \cdot z \]
   9. Step-by-step derivation

   10. Applied rewrites 36.0%

       \[\leadsto t \cdot z \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 7: 34.8% accurate, 3.8× speedup

Math

\[a \cdot b \]

FPCore

(FPCore (x y z t a b)
  :precision binary64
  :pre TRUE
  (* a b))

C

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

Fortran

real(8) function code(x, y, z, t, a, b)
use fmin_fmax_functions
    real(8), intent (in) :: x
    real(8), intent (in) :: y
    real(8), intent (in) :: z
    real(8), intent (in) :: t
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = a * b
end function

Java

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

Python

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

Julia

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

MATLAB

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

Wolfram

code[x_, y_, z_, t_, a_, b_] := N[(a * b), $MachinePrecision]

ReFlow

f(x, y, z, t, a, b):
	x in [-inf, +inf],
	y in [-inf, +inf],
	z in [-inf, +inf],
	t in [-inf, +inf],
	a in [-inf, +inf],
	b in [-inf, +inf]
code: THEORY
BEGIN
f(x, y, z, t, a, b: real): real =
	a * b
END code

Derivation

1. Initial program 97.7%

   \[\left(x \cdot y + z \cdot t\right) + a \cdot b \]

2. Taylor expanded in z around 0

   \[\leadsto a \cdot b + x \cdot y \]
3. Step-by-step derivation

4. Applied rewrites 66.9%

   \[\leadsto \mathsf{fma}\left(a, b, x \cdot y\right) \]

5. Taylor expanded in x around 0

   \[\leadsto a \cdot b \]
6. Step-by-step derivation

7. Applied rewrites 34.8%

   \[\leadsto a \cdot b \]
8. Add Preprocessing

Reproduce

herbie shell --seed 2026092 
(FPCore (x y z t a b)
  :name "Linear.V3:$cdot from linear-1.19.1.3, B"
  :precision binary64
  (+ (+ (* x y) (* z t)) (* a b)))