?

Average Error: 0.1 → 0.2
Time: 32.7s
Precision: binary64
Cost: 14272

?

\[\left(\left(\left(-65504 \leq ax \land ax \leq 65504\right) \land \left(-65504 \leq ay \land ay \leq 65504\right)\right) \land \left(-65504 \leq az \land az \leq 65504\right)\right) \land \left(-1 \leq s \land s \leq 1\right)\]
\[ \begin{array}{c}[ax, ay, az] = \mathsf{sort}([ax, ay, az])\\ \end{array} \]
\[\frac{\left(\left(ax + ay\right) + az\right) + s \cdot \sqrt{\left(\left(ax + ay\right) + az\right) \cdot \left(\left(ax + ay\right) + az\right) - 3 \cdot \left(\left(\left(ax \cdot ax + ay \cdot ay\right) + az \cdot az\right) - 1\right)}}{3} \]
↓
\[\frac{ax + \mathsf{fma}\left(s, \sqrt{az \cdot az + -3 \cdot \left(ax \cdot ax + \left(az \cdot az + -1\right)\right)}, az + ay\right)}{3} \]
(FPCore (ax ay az s)
 :precision binary64
 (/
  (+
   (+ (+ ax ay) az)
   (*
    s
    (sqrt
     (-
      (* (+ (+ ax ay) az) (+ (+ ax ay) az))
      (* 3.0 (- (+ (+ (* ax ax) (* ay ay)) (* az az)) 1.0))))))
  3.0))
↓
(FPCore (ax ay az s)
 :precision binary64
 (/
  (+
   ax
   (fma
    s
    (sqrt (+ (* az az) (* -3.0 (+ (* ax ax) (+ (* az az) -1.0)))))
    (+ az ay)))
  3.0))
double code(double ax, double ay, double az, double s) {
	return (((ax + ay) + az) + (s * sqrt(((((ax + ay) + az) * ((ax + ay) + az)) - (3.0 * ((((ax * ax) + (ay * ay)) + (az * az)) - 1.0)))))) / 3.0;
}
↓
double code(double ax, double ay, double az, double s) {
	return (ax + fma(s, sqrt(((az * az) + (-3.0 * ((ax * ax) + ((az * az) + -1.0))))), (az + ay))) / 3.0;
}

function code(ax, ay, az, s)
	return Float64(Float64(Float64(Float64(ax + ay) + az) + Float64(s * sqrt(Float64(Float64(Float64(Float64(ax + ay) + az) * Float64(Float64(ax + ay) + az)) - Float64(3.0 * Float64(Float64(Float64(Float64(ax * ax) + Float64(ay * ay)) + Float64(az * az)) - 1.0)))))) / 3.0)
end
↓
function code(ax, ay, az, s)
	return Float64(Float64(ax + fma(s, sqrt(Float64(Float64(az * az) + Float64(-3.0 * Float64(Float64(ax * ax) + Float64(Float64(az * az) + -1.0))))), Float64(az + ay))) / 3.0)
end

code[ax_, ay_, az_, s_] := N[(N[(N[(N[(ax + ay), $MachinePrecision] + az), $MachinePrecision] + N[(s * N[Sqrt[N[(N[(N[(N[(ax + ay), $MachinePrecision] + az), $MachinePrecision] * N[(N[(ax + ay), $MachinePrecision] + az), $MachinePrecision]), $MachinePrecision] - N[(3.0 * N[(N[(N[(N[(ax * ax), $MachinePrecision] + N[(ay * ay), $MachinePrecision]), $MachinePrecision] + N[(az * az), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / 3.0), $MachinePrecision]
↓
code[ax_, ay_, az_, s_] := N[(N[(ax + N[(s * N[Sqrt[N[(N[(az * az), $MachinePrecision] + N[(-3.0 * N[(N[(ax * ax), $MachinePrecision] + N[(N[(az * az), $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] + N[(az + ay), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / 3.0), $MachinePrecision]

\frac{\left(\left(ax + ay\right) + az\right) + s \cdot \sqrt{\left(\left(ax + ay\right) + az\right) \cdot \left(\left(ax + ay\right) + az\right) - 3 \cdot \left(\left(\left(ax \cdot ax + ay \cdot ay\right) + az \cdot az\right) - 1\right)}}{3}
↓
\frac{ax + \mathsf{fma}\left(s, \sqrt{az \cdot az + -3 \cdot \left(ax \cdot ax + \left(az \cdot az + -1\right)\right)}, az + ay\right)}{3}

Error?

Derivation?

  1. Initial program 0.1

    \[\frac{\left(\left(ax + ay\right) + az\right) + s \cdot \sqrt{\left(\left(ax + ay\right) + az\right) \cdot \left(\left(ax + ay\right) + az\right) - 3 \cdot \left(\left(\left(ax \cdot ax + ay \cdot ay\right) + az \cdot az\right) - 1\right)}}{3} \]

  2. Simplified0.1

    \[\leadsto \color{blue}{\frac{ax + \mathsf{fma}\left(s, \sqrt{\mathsf{fma}\left(ax + \left(ay + az\right), ax + \left(ay + az\right), \mathsf{fma}\left(ax, ax, \mathsf{fma}\left(ay, ay, \mathsf{fma}\left(az, az, -1\right)\right)\right) \cdot -3\right)}, ay + az\right)}{3}} \]
    Proof

    [Start]0.1

    \[ \frac{\left(\left(ax + ay\right) + az\right) + s \cdot \sqrt{\left(\left(ax + ay\right) + az\right) \cdot \left(\left(ax + ay\right) + az\right) - 3 \cdot \left(\left(\left(ax \cdot ax + ay \cdot ay\right) + az \cdot az\right) - 1\right)}}{3} \]

  3. Taylor expanded in ay around 0 0.1

    \[\leadsto \frac{ax + \mathsf{fma}\left(s, \color{blue}{\sqrt{{\left(az + ax\right)}^{2} + -3 \cdot \left(\left({ax}^{2} + {az}^{2}\right) - 1\right)}}, ay + az\right)}{3} \]

  4. Simplified0.1

    \[\leadsto \frac{ax + \mathsf{fma}\left(s, \color{blue}{\sqrt{{\left(az + ax\right)}^{2} + -3 \cdot \left(ax \cdot ax + \left(az \cdot az - 1\right)\right)}}, ay + az\right)}{3} \]
    Proof

    [Start]0.1

    \[ \frac{ax + \mathsf{fma}\left(s, \sqrt{{\left(az + ax\right)}^{2} + -3 \cdot \left(\left({ax}^{2} + {az}^{2}\right) - 1\right)}, ay + az\right)}{3} \]

    associate--l+ [=>]0.1

    \[ \frac{ax + \mathsf{fma}\left(s, \sqrt{{\left(az + ax\right)}^{2} + -3 \cdot \color{blue}{\left({ax}^{2} + \left({az}^{2} - 1\right)\right)}}, ay + az\right)}{3} \]

    unpow2 [=>]0.1

    \[ \frac{ax + \mathsf{fma}\left(s, \sqrt{{\left(az + ax\right)}^{2} + -3 \cdot \left(\color{blue}{ax \cdot ax} + \left({az}^{2} - 1\right)\right)}, ay + az\right)}{3} \]

    unpow2 [=>]0.1

    \[ \frac{ax + \mathsf{fma}\left(s, \sqrt{{\left(az + ax\right)}^{2} + -3 \cdot \left(ax \cdot ax + \left(\color{blue}{az \cdot az} - 1\right)\right)}, ay + az\right)}{3} \]

  5. Taylor expanded in az around inf 0.2

    \[\leadsto \frac{ax + \mathsf{fma}\left(s, \sqrt{\color{blue}{{az}^{2}} + -3 \cdot \left(ax \cdot ax + \left(az \cdot az - 1\right)\right)}, ay + az\right)}{3} \]

  6. Simplified0.2

    \[\leadsto \frac{ax + \mathsf{fma}\left(s, \sqrt{\color{blue}{az \cdot az} + -3 \cdot \left(ax \cdot ax + \left(az \cdot az - 1\right)\right)}, ay + az\right)}{3} \]
    Proof

    [Start]0.2

    \[ \frac{ax + \mathsf{fma}\left(s, \sqrt{{az}^{2} + -3 \cdot \left(ax \cdot ax + \left(az \cdot az - 1\right)\right)}, ay + az\right)}{3} \]

    unpow2 [=>]0.2

    \[ \frac{ax + \mathsf{fma}\left(s, \sqrt{\color{blue}{az \cdot az} + -3 \cdot \left(ax \cdot ax + \left(az \cdot az - 1\right)\right)}, ay + az\right)}{3} \]

  7. Final simplification0.2

    \[\leadsto \frac{ax + \mathsf{fma}\left(s, \sqrt{az \cdot az + -3 \cdot \left(ax \cdot ax + \left(az \cdot az + -1\right)\right)}, az + ay\right)}{3} \]

Alternatives

Alternative 1
Error9.5
Cost8269
\[\begin{array}{l} \mathbf{if}\;ax \leq -1.22 \cdot 10^{-110} \lor \neg \left(ax \leq -4 \cdot 10^{-134}\right) \land ax \leq -9 \cdot 10^{-159}:\\ \;\;\;\;\frac{az + \left(ax + ay\right)}{3}\\ \mathbf{else}:\\ \;\;\;\;\frac{az + \left(ay + s \cdot \sqrt{az \cdot az + -3 \cdot \left(\left(az \cdot az + -1\right) + ay \cdot ay\right)}\right)}{3}\\ \end{array} \]
Alternative 2
Error0.2
Cost8256
\[\frac{s \cdot \sqrt{az \cdot az + -3 \cdot \left(\left(az \cdot az + \left(ax \cdot ax + ay \cdot ay\right)\right) + -1\right)} + \left(az + \left(ax + ay\right)\right)}{3} \]
Alternative 3
Error27.4
Cost589
\[\begin{array}{l} \mathbf{if}\;az \leq 2 \cdot 10^{-155} \lor \neg \left(az \leq 10^{-123}\right) \land az \leq 1.02 \cdot 10^{-106}:\\ \;\;\;\;ax \cdot 0.3333333333333333\\ \mathbf{else}:\\ \;\;\;\;az \cdot 0.3333333333333333\\ \end{array} \]
Alternative 4
Error17.1
Cost448
\[\left(az + \left(ax + ay\right)\right) \cdot 0.3333333333333333 \]
Alternative 5
Error16.8
Cost448
\[\frac{az + \left(ax + ay\right)}{3} \]
Alternative 6
Error18.3
Cost320
\[0.3333333333333333 \cdot \left(ax + az\right) \]
Alternative 7
Error40.1
Cost192
\[ax \cdot 0.3333333333333333 \]

Error

Reproduce?

herbie shell --seed 1 
(FPCore (ax ay az s)
  :name "((ax+ay+az) + s*sqrt((ax+ay+az)*(ax+ay+az) - 3.0*((ax*ax + ay*ay + az*az) - 1.0))) / 3.0"
  :precision binary64
  :pre (and (and (and (and (<= -65504.0 ax) (<= ax 65504.0)) (and (<= -65504.0 ay) (<= ay 65504.0))) (and (<= -65504.0 az) (<= az 65504.0))) (and (<= -1.0 s) (<= s 1.0)))
  (/ (+ (+ (+ ax ay) az) (* s (sqrt (- (* (+ (+ ax ay) az) (+ (+ ax ay) az)) (* 3.0 (- (+ (+ (* ax ax) (* ay ay)) (* az az)) 1.0)))))) 3.0))