Falkner and Boettcher, Equation (22+)

Percentage Accurate: 98.5% → 100.0%
Time: 3.4s
Alternatives: 7
Speedup: 30.0×

Specification

?
\[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
(FPCore (v)
  :precision binary64
  (/
 4.0
 (* (* (* 3.0 PI) (- 1.0 (* v v))) (sqrt (- 2.0 (* 6.0 (* v v)))))))
double code(double v) {
	return 4.0 / (((3.0 * ((double) M_PI)) * (1.0 - (v * v))) * sqrt((2.0 - (6.0 * (v * v)))));
}
public static double code(double v) {
	return 4.0 / (((3.0 * Math.PI) * (1.0 - (v * v))) * Math.sqrt((2.0 - (6.0 * (v * v)))));
}
def code(v):
	return 4.0 / (((3.0 * math.pi) * (1.0 - (v * v))) * math.sqrt((2.0 - (6.0 * (v * v)))))
function code(v)
	return Float64(4.0 / Float64(Float64(Float64(3.0 * pi) * Float64(1.0 - Float64(v * v))) * sqrt(Float64(2.0 - Float64(6.0 * Float64(v * v))))))
end
function tmp = code(v)
	tmp = 4.0 / (((3.0 * pi) * (1.0 - (v * v))) * sqrt((2.0 - (6.0 * (v * v)))));
end
code[v_] := N[(4.0 / N[(N[(N[(3.0 * Pi), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Sqrt[N[(2.0 - N[(6.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 7 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 98.5% accurate, 1.0× speedup?

\[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
(FPCore (v)
  :precision binary64
  (/
 4.0
 (* (* (* 3.0 PI) (- 1.0 (* v v))) (sqrt (- 2.0 (* 6.0 (* v v)))))))
double code(double v) {
	return 4.0 / (((3.0 * ((double) M_PI)) * (1.0 - (v * v))) * sqrt((2.0 - (6.0 * (v * v)))));
}
public static double code(double v) {
	return 4.0 / (((3.0 * Math.PI) * (1.0 - (v * v))) * Math.sqrt((2.0 - (6.0 * (v * v)))));
}
def code(v):
	return 4.0 / (((3.0 * math.pi) * (1.0 - (v * v))) * math.sqrt((2.0 - (6.0 * (v * v)))))
function code(v)
	return Float64(4.0 / Float64(Float64(Float64(3.0 * pi) * Float64(1.0 - Float64(v * v))) * sqrt(Float64(2.0 - Float64(6.0 * Float64(v * v))))))
end
function tmp = code(v)
	tmp = 4.0 / (((3.0 * pi) * (1.0 - (v * v))) * sqrt((2.0 - (6.0 * (v * v)))));
end
code[v_] := N[(4.0 / N[(N[(N[(3.0 * Pi), $MachinePrecision] * N[(1.0 - N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Sqrt[N[(2.0 - N[(6.0 * N[(v * v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}

Alternative 1: 100.0% accurate, 1.2× speedup?

\[\frac{-1.3333333333333333}{\left(\mathsf{fma}\left(v, v, -1\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
(FPCore (v)
  :precision binary64
  (/
 -1.3333333333333333
 (* (* (fma v v -1.0) PI) (sqrt (fma -6.0 (* v v) 2.0)))))
double code(double v) {
	return -1.3333333333333333 / ((fma(v, v, -1.0) * ((double) M_PI)) * sqrt(fma(-6.0, (v * v), 2.0)));
}
function code(v)
	return Float64(-1.3333333333333333 / Float64(Float64(fma(v, v, -1.0) * pi) * sqrt(fma(-6.0, Float64(v * v), 2.0))))
end
code[v_] := N[(-1.3333333333333333 / N[(N[(N[(v * v + -1.0), $MachinePrecision] * Pi), $MachinePrecision] * N[Sqrt[N[(-6.0 * N[(v * v), $MachinePrecision] + 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{-1.3333333333333333}{\left(\mathsf{fma}\left(v, v, -1\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}
Derivation
  1. Initial program 98.5%

    \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
  2. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    3. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    4. lift-*.f64N/A

      \[\leadsto \frac{4}{\left(\color{blue}{\left(3 \cdot \pi\right)} \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    5. associate-*l*N/A

      \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \left(\pi \cdot \left(1 - v \cdot v\right)\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    6. associate-*l*N/A

      \[\leadsto \frac{4}{\color{blue}{3 \cdot \left(\left(\pi \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
    7. associate-/r*N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3}}{\left(\pi \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    8. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3}}{\left(\pi \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    9. metadata-evalN/A

      \[\leadsto \frac{\color{blue}{\frac{4}{3}}}{\left(\pi \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    10. lower-*.f64N/A

      \[\leadsto \frac{\frac{4}{3}}{\color{blue}{\left(\pi \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    11. *-commutativeN/A

      \[\leadsto \frac{\frac{4}{3}}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot \pi\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    12. lower-*.f64100.0%

      \[\leadsto \frac{1.3333333333333333}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot \pi\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    13. lift--.f64N/A

      \[\leadsto \frac{\frac{4}{3}}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\color{blue}{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    14. lift-*.f64N/A

      \[\leadsto \frac{\frac{4}{3}}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{2 - \color{blue}{6 \cdot \left(v \cdot v\right)}}} \]
    15. fp-cancel-sub-sign-invN/A

      \[\leadsto \frac{\frac{4}{3}}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\color{blue}{2 + \left(\mathsf{neg}\left(6\right)\right) \cdot \left(v \cdot v\right)}}} \]
    16. +-commutativeN/A

      \[\leadsto \frac{\frac{4}{3}}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\color{blue}{\left(\mathsf{neg}\left(6\right)\right) \cdot \left(v \cdot v\right) + 2}}} \]
  3. Applied rewrites100.0%

    \[\leadsto \color{blue}{\frac{1.3333333333333333}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
  4. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3}}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
    2. frac-2negN/A

      \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{4}{3}\right)}{\mathsf{neg}\left(\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)}} \]
    3. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{4}{3}\right)}{\mathsf{neg}\left(\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)}} \]
    4. metadata-evalN/A

      \[\leadsto \frac{\color{blue}{\frac{-4}{3}}}{\mathsf{neg}\left(\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)} \]
    5. lift-*.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\mathsf{neg}\left(\color{blue}{\left(\left(1 - v \cdot v\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}\right)} \]
    6. distribute-lft-neg-inN/A

      \[\leadsto \frac{\frac{-4}{3}}{\color{blue}{\left(\mathsf{neg}\left(\left(1 - v \cdot v\right) \cdot \pi\right)\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
    7. lower-*.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\color{blue}{\left(\mathsf{neg}\left(\left(1 - v \cdot v\right) \cdot \pi\right)\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
    8. lift-*.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\left(\mathsf{neg}\left(\color{blue}{\left(1 - v \cdot v\right) \cdot \pi}\right)\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    9. distribute-lft-neg-outN/A

      \[\leadsto \frac{\frac{-4}{3}}{\color{blue}{\left(\left(\mathsf{neg}\left(\left(1 - v \cdot v\right)\right)\right) \cdot \pi\right)} \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    10. lift--.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\left(\left(\mathsf{neg}\left(\color{blue}{\left(1 - v \cdot v\right)}\right)\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    11. sub-negate-revN/A

      \[\leadsto \frac{\frac{-4}{3}}{\left(\color{blue}{\left(v \cdot v - 1\right)} \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    12. lower-*.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\color{blue}{\left(\left(v \cdot v - 1\right) \cdot \pi\right)} \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    13. sub-flipN/A

      \[\leadsto \frac{\frac{-4}{3}}{\left(\color{blue}{\left(v \cdot v + \left(\mathsf{neg}\left(1\right)\right)\right)} \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    14. lift-*.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\left(\left(\color{blue}{v \cdot v} + \left(\mathsf{neg}\left(1\right)\right)\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    15. lower-fma.f64N/A

      \[\leadsto \frac{\frac{-4}{3}}{\left(\color{blue}{\mathsf{fma}\left(v, v, \mathsf{neg}\left(1\right)\right)} \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    16. metadata-eval100.0%

      \[\leadsto \frac{-1.3333333333333333}{\left(\mathsf{fma}\left(v, v, \color{blue}{-1}\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
  5. Applied rewrites100.0%

    \[\leadsto \color{blue}{\frac{-1.3333333333333333}{\left(\mathsf{fma}\left(v, v, -1\right) \cdot \pi\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
  6. Add Preprocessing

Alternative 2: 100.0% accurate, 1.3× speedup?

\[\frac{\frac{-0.4244131815783876}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)}} \]
(FPCore (v)
  :precision binary64
  (/
 (/ -0.4244131815783876 (fma v v -1.0))
 (sqrt (fma (* v v) -6.0 2.0))))
double code(double v) {
	return (-0.4244131815783876 / fma(v, v, -1.0)) / sqrt(fma((v * v), -6.0, 2.0));
}
function code(v)
	return Float64(Float64(-0.4244131815783876 / fma(v, v, -1.0)) / sqrt(fma(Float64(v * v), -6.0, 2.0)))
end
code[v_] := N[(N[(-0.4244131815783876 / N[(v * v + -1.0), $MachinePrecision]), $MachinePrecision] / N[Sqrt[N[(N[(v * v), $MachinePrecision] * -6.0 + 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]
\frac{\frac{-0.4244131815783876}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)}}
Derivation
  1. Initial program 98.5%

    \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
  2. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    3. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    4. associate-*l*N/A

      \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \pi\right) \cdot \left(\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
    5. associate-/r*N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    6. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    7. lift-*.f64N/A

      \[\leadsto \frac{\frac{4}{\color{blue}{3 \cdot \pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    8. associate-/r*N/A

      \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    9. lower-/.f64N/A

      \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    10. metadata-evalN/A

      \[\leadsto \frac{\frac{\color{blue}{\frac{4}{3}}}{\pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    11. *-commutativeN/A

      \[\leadsto \frac{\frac{\frac{4}{3}}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
    12. lower-*.f64100.0%

      \[\leadsto \frac{\frac{1.3333333333333333}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
  3. Applied rewrites100.0%

    \[\leadsto \color{blue}{\frac{\frac{1.3333333333333333}{\pi}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
  4. Evaluated real constant100.0%

    \[\leadsto \frac{\color{blue}{0.4244131815783876}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)} \]
  5. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{\frac{1911387046407553}{4503599627370496}}{\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
    3. lift--.f64N/A

      \[\leadsto \frac{\frac{1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(1 - v \cdot v\right)}} \]
    4. lift-*.f64N/A

      \[\leadsto \frac{\frac{1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - \color{blue}{v \cdot v}\right)} \]
    5. *-commutativeN/A

      \[\leadsto \frac{\frac{1911387046407553}{4503599627370496}}{\color{blue}{\left(1 - v \cdot v\right) \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
    6. associate-/r*N/A

      \[\leadsto \color{blue}{\frac{\frac{\frac{1911387046407553}{4503599627370496}}{1 - v \cdot v}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
    7. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{\frac{1911387046407553}{4503599627370496}}{1 - v \cdot v}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
    8. frac-2negN/A

      \[\leadsto \frac{\color{blue}{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{neg}\left(\left(1 - v \cdot v\right)\right)}}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    9. lift-*.f64N/A

      \[\leadsto \frac{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{neg}\left(\left(1 - \color{blue}{v \cdot v}\right)\right)}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    10. sub-negate-revN/A

      \[\leadsto \frac{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\color{blue}{v \cdot v - 1}}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    11. metadata-evalN/A

      \[\leadsto \frac{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{v \cdot v - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)}}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    12. add-flipN/A

      \[\leadsto \frac{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\color{blue}{v \cdot v + -1}}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    13. lift-*.f64N/A

      \[\leadsto \frac{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\color{blue}{v \cdot v} + -1}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    14. lift-fma.f64N/A

      \[\leadsto \frac{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\color{blue}{\mathsf{fma}\left(v, v, -1\right)}}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    15. lower-/.f64N/A

      \[\leadsto \frac{\color{blue}{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{fma}\left(v, v, -1\right)}}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    16. metadata-eval100.0%

      \[\leadsto \frac{\frac{\color{blue}{-0.4244131815783876}}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}} \]
    17. lift-fma.f64N/A

      \[\leadsto \frac{\frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\color{blue}{-6 \cdot \left(v \cdot v\right) + 2}}} \]
    18. *-commutativeN/A

      \[\leadsto \frac{\frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\color{blue}{\left(v \cdot v\right) \cdot -6} + 2}} \]
    19. lower-fma.f64100.0%

      \[\leadsto \frac{\frac{-0.4244131815783876}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\color{blue}{\mathsf{fma}\left(v \cdot v, -6, 2\right)}}} \]
  6. Applied rewrites100.0%

    \[\leadsto \color{blue}{\frac{\frac{-0.4244131815783876}{\mathsf{fma}\left(v, v, -1\right)}}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)}}} \]
  7. Add Preprocessing

Alternative 3: 100.0% accurate, 1.3× speedup?

\[\frac{-0.4244131815783876}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
(FPCore (v)
  :precision binary64
  (/
 -0.4244131815783876
 (* (sqrt (fma (* v v) -6.0 2.0)) (fma v v -1.0))))
double code(double v) {
	return -0.4244131815783876 / (sqrt(fma((v * v), -6.0, 2.0)) * fma(v, v, -1.0));
}
function code(v)
	return Float64(-0.4244131815783876 / Float64(sqrt(fma(Float64(v * v), -6.0, 2.0)) * fma(v, v, -1.0)))
end
code[v_] := N[(-0.4244131815783876 / N[(N[Sqrt[N[(N[(v * v), $MachinePrecision] * -6.0 + 2.0), $MachinePrecision]], $MachinePrecision] * N[(v * v + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{-0.4244131815783876}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)} \cdot \mathsf{fma}\left(v, v, -1\right)}
Derivation
  1. Initial program 98.5%

    \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
  2. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    3. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    4. associate-*l*N/A

      \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \pi\right) \cdot \left(\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
    5. associate-/r*N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    6. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    7. lift-*.f64N/A

      \[\leadsto \frac{\frac{4}{\color{blue}{3 \cdot \pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    8. associate-/r*N/A

      \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    9. lower-/.f64N/A

      \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    10. metadata-evalN/A

      \[\leadsto \frac{\frac{\color{blue}{\frac{4}{3}}}{\pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    11. *-commutativeN/A

      \[\leadsto \frac{\frac{\frac{4}{3}}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
    12. lower-*.f64100.0%

      \[\leadsto \frac{\frac{1.3333333333333333}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
  3. Applied rewrites100.0%

    \[\leadsto \color{blue}{\frac{\frac{1.3333333333333333}{\pi}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
  4. Evaluated real constant100.0%

    \[\leadsto \frac{\color{blue}{0.4244131815783876}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)} \]
  5. Step-by-step derivation
    1. lift-/.f64N/A

      \[\leadsto \color{blue}{\frac{\frac{1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
    2. frac-2negN/A

      \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)\right)}} \]
    3. lower-/.f64N/A

      \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)\right)}} \]
    4. metadata-evalN/A

      \[\leadsto \frac{\color{blue}{\frac{-1911387046407553}{4503599627370496}}}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)\right)} \]
    5. lift-*.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{neg}\left(\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}\right)} \]
    6. lift--.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(1 - v \cdot v\right)}\right)} \]
    7. lift-*.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - \color{blue}{v \cdot v}\right)\right)} \]
    8. distribute-rgt-neg-inN/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(\mathsf{neg}\left(\left(1 - v \cdot v\right)\right)\right)}} \]
    9. lift-*.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(\mathsf{neg}\left(\left(1 - \color{blue}{v \cdot v}\right)\right)\right)} \]
    10. sub-negate-revN/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(v \cdot v - 1\right)}} \]
    11. metadata-evalN/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(v \cdot v - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)}\right)} \]
    12. add-flipN/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(v \cdot v + -1\right)}} \]
    13. lift-*.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(\color{blue}{v \cdot v} + -1\right)} \]
    14. lift-fma.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\mathsf{fma}\left(v, v, -1\right)}} \]
    15. lower-*.f64100.0%

      \[\leadsto \frac{-0.4244131815783876}{\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \mathsf{fma}\left(v, v, -1\right)}} \]
    16. lift-fma.f64N/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\color{blue}{-6 \cdot \left(v \cdot v\right) + 2}} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
    17. *-commutativeN/A

      \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\color{blue}{\left(v \cdot v\right) \cdot -6} + 2} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
    18. lower-fma.f64100.0%

      \[\leadsto \frac{-0.4244131815783876}{\sqrt{\color{blue}{\mathsf{fma}\left(v \cdot v, -6, 2\right)}} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
  6. Applied rewrites100.0%

    \[\leadsto \color{blue}{\frac{-0.4244131815783876}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)} \cdot \mathsf{fma}\left(v, v, -1\right)}} \]
  7. Add Preprocessing

Alternative 4: 98.9% accurate, 1.4× speedup?

\[\frac{\frac{4}{3 \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)}}}{\pi} \]
(FPCore (v)
  :precision binary64
  (/ (/ 4.0 (* 3.0 (sqrt (fma (* v v) -6.0 2.0)))) PI))
double code(double v) {
	return (4.0 / (3.0 * sqrt(fma((v * v), -6.0, 2.0)))) / ((double) M_PI);
}
function code(v)
	return Float64(Float64(4.0 / Float64(3.0 * sqrt(fma(Float64(v * v), -6.0, 2.0)))) / pi)
end
code[v_] := N[(N[(4.0 / N[(3.0 * N[Sqrt[N[(N[(v * v), $MachinePrecision] * -6.0 + 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / Pi), $MachinePrecision]
\frac{\frac{4}{3 \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)}}}{\pi}
Derivation
  1. Initial program 98.5%

    \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
  2. Step-by-step derivation
    1. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
    2. lift-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    3. *-commutativeN/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot \left(3 \cdot \pi\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    4. lift-*.f64N/A

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot \color{blue}{\left(3 \cdot \pi\right)}\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    5. associate-*r*N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \pi\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    6. associate-*l*N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
    7. *-commutativeN/A

      \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \left(1 - v \cdot v\right)\right)} \cdot \left(\pi \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)} \]
    8. lower-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \left(1 - v \cdot v\right)\right) \cdot \left(\pi \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
    9. *-commutativeN/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot 3\right)} \cdot \left(\pi \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)} \]
    10. lower-*.f64N/A

      \[\leadsto \frac{4}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot 3\right)} \cdot \left(\pi \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)} \]
    11. lower-*.f6498.5%

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \color{blue}{\left(\pi \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
    12. lift--.f64N/A

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{\color{blue}{2 - 6 \cdot \left(v \cdot v\right)}}\right)} \]
    13. lift-*.f64N/A

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{2 - \color{blue}{6 \cdot \left(v \cdot v\right)}}\right)} \]
    14. fp-cancel-sub-sign-invN/A

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{\color{blue}{2 + \left(\mathsf{neg}\left(6\right)\right) \cdot \left(v \cdot v\right)}}\right)} \]
    15. +-commutativeN/A

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{\color{blue}{\left(\mathsf{neg}\left(6\right)\right) \cdot \left(v \cdot v\right) + 2}}\right)} \]
    16. lower-fma.f64N/A

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{\color{blue}{\mathsf{fma}\left(\mathsf{neg}\left(6\right), v \cdot v, 2\right)}}\right)} \]
    17. metadata-eval98.5%

      \[\leadsto \frac{4}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{\mathsf{fma}\left(\color{blue}{-6}, v \cdot v, 2\right)}\right)} \]
  3. Applied rewrites98.5%

    \[\leadsto \frac{4}{\color{blue}{\left(\left(1 - v \cdot v\right) \cdot 3\right) \cdot \left(\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)}} \]
  4. Taylor expanded in v around 0

    \[\leadsto \frac{4}{\color{blue}{3} \cdot \left(\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)} \]
  5. Step-by-step derivation
    1. Applied rewrites97.4%

      \[\leadsto \frac{4}{\color{blue}{3} \cdot \left(\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)} \]
    2. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{4}{3 \cdot \left(\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{4}{\color{blue}{3 \cdot \left(\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}\right)}} \]
      3. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{4}{3}}{\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
      4. lift-*.f64N/A

        \[\leadsto \frac{\frac{4}{3}}{\color{blue}{\pi \cdot \sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}} \]
      5. *-commutativeN/A

        \[\leadsto \frac{\frac{4}{3}}{\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \pi}} \]
      6. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{\frac{4}{3}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}}{\pi}} \]
      7. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{\frac{4}{3}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)}}}{\pi}} \]
    3. Applied rewrites98.9%

      \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)}}}{\pi}} \]
    4. Add Preprocessing

    Alternative 5: 98.9% accurate, 1.7× speedup?

    \[\frac{0.4244131815783876}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot 1} \]
    (FPCore (v)
      :precision binary64
      (/ 0.4244131815783876 (* (sqrt (fma -6.0 (* v v) 2.0)) 1.0)))
    double code(double v) {
    	return 0.4244131815783876 / (sqrt(fma(-6.0, (v * v), 2.0)) * 1.0);
    }
    
    function code(v)
    	return Float64(0.4244131815783876 / Float64(sqrt(fma(-6.0, Float64(v * v), 2.0)) * 1.0))
    end
    
    code[v_] := N[(0.4244131815783876 / N[(N[Sqrt[N[(-6.0 * N[(v * v), $MachinePrecision] + 2.0), $MachinePrecision]], $MachinePrecision] * 1.0), $MachinePrecision]), $MachinePrecision]
    
    \frac{0.4244131815783876}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot 1}
    
    Derivation
    1. Initial program 98.5%

      \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
    2. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
      3. lift-*.f64N/A

        \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
      4. associate-*l*N/A

        \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \pi\right) \cdot \left(\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
      5. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
      6. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
      7. lift-*.f64N/A

        \[\leadsto \frac{\frac{4}{\color{blue}{3 \cdot \pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
      8. associate-/r*N/A

        \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
      9. lower-/.f64N/A

        \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
      10. metadata-evalN/A

        \[\leadsto \frac{\frac{\color{blue}{\frac{4}{3}}}{\pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
      11. *-commutativeN/A

        \[\leadsto \frac{\frac{\frac{4}{3}}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
      12. lower-*.f64100.0%

        \[\leadsto \frac{\frac{1.3333333333333333}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
    3. Applied rewrites100.0%

      \[\leadsto \color{blue}{\frac{\frac{1.3333333333333333}{\pi}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
    4. Evaluated real constant100.0%

      \[\leadsto \frac{\color{blue}{0.4244131815783876}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)} \]
    5. Taylor expanded in v around 0

      \[\leadsto \frac{0.4244131815783876}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{1}} \]
    6. Step-by-step derivation
      1. Applied rewrites98.9%

        \[\leadsto \frac{0.4244131815783876}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{1}} \]
      2. Add Preprocessing

      Alternative 6: 98.9% accurate, 2.0× speedup?

      \[\frac{-0.4244131815783876}{\sqrt{2} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
      (FPCore (v)
        :precision binary64
        (/ -0.4244131815783876 (* (sqrt 2.0) (fma v v -1.0))))
      double code(double v) {
      	return -0.4244131815783876 / (sqrt(2.0) * fma(v, v, -1.0));
      }
      
      function code(v)
      	return Float64(-0.4244131815783876 / Float64(sqrt(2.0) * fma(v, v, -1.0)))
      end
      
      code[v_] := N[(-0.4244131815783876 / N[(N[Sqrt[2.0], $MachinePrecision] * N[(v * v + -1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
      
      \frac{-0.4244131815783876}{\sqrt{2} \cdot \mathsf{fma}\left(v, v, -1\right)}
      
      Derivation
      1. Initial program 98.5%

        \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
      2. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
        3. lift-*.f64N/A

          \[\leadsto \frac{4}{\color{blue}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right)} \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
        4. associate-*l*N/A

          \[\leadsto \frac{4}{\color{blue}{\left(3 \cdot \pi\right) \cdot \left(\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}\right)}} \]
        5. associate-/r*N/A

          \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
        6. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\frac{4}{3 \cdot \pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}}} \]
        7. lift-*.f64N/A

          \[\leadsto \frac{\frac{4}{\color{blue}{3 \cdot \pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
        8. associate-/r*N/A

          \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
        9. lower-/.f64N/A

          \[\leadsto \frac{\color{blue}{\frac{\frac{4}{3}}{\pi}}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
        10. metadata-evalN/A

          \[\leadsto \frac{\frac{\color{blue}{\frac{4}{3}}}{\pi}}{\left(1 - v \cdot v\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
        11. *-commutativeN/A

          \[\leadsto \frac{\frac{\frac{4}{3}}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
        12. lower-*.f64100.0%

          \[\leadsto \frac{\frac{1.3333333333333333}{\pi}}{\color{blue}{\sqrt{2 - 6 \cdot \left(v \cdot v\right)} \cdot \left(1 - v \cdot v\right)}} \]
      3. Applied rewrites100.0%

        \[\leadsto \color{blue}{\frac{\frac{1.3333333333333333}{\pi}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
      4. Evaluated real constant100.0%

        \[\leadsto \frac{\color{blue}{0.4244131815783876}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)} \]
      5. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\frac{1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}} \]
        2. frac-2negN/A

          \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)\right)}} \]
        3. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{1911387046407553}{4503599627370496}\right)}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)\right)}} \]
        4. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{\frac{-1911387046407553}{4503599627370496}}}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)\right)} \]
        5. lift-*.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{neg}\left(\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - v \cdot v\right)}\right)} \]
        6. lift--.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(1 - v \cdot v\right)}\right)} \]
        7. lift-*.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\mathsf{neg}\left(\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(1 - \color{blue}{v \cdot v}\right)\right)} \]
        8. distribute-rgt-neg-inN/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(\mathsf{neg}\left(\left(1 - v \cdot v\right)\right)\right)}} \]
        9. lift-*.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(\mathsf{neg}\left(\left(1 - \color{blue}{v \cdot v}\right)\right)\right)} \]
        10. sub-negate-revN/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(v \cdot v - 1\right)}} \]
        11. metadata-evalN/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(v \cdot v - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)}\right)} \]
        12. add-flipN/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\left(v \cdot v + -1\right)}} \]
        13. lift-*.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \left(\color{blue}{v \cdot v} + -1\right)} \]
        14. lift-fma.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \color{blue}{\mathsf{fma}\left(v, v, -1\right)}} \]
        15. lower-*.f64100.0%

          \[\leadsto \frac{-0.4244131815783876}{\color{blue}{\sqrt{\mathsf{fma}\left(-6, v \cdot v, 2\right)} \cdot \mathsf{fma}\left(v, v, -1\right)}} \]
        16. lift-fma.f64N/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\color{blue}{-6 \cdot \left(v \cdot v\right) + 2}} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
        17. *-commutativeN/A

          \[\leadsto \frac{\frac{-1911387046407553}{4503599627370496}}{\sqrt{\color{blue}{\left(v \cdot v\right) \cdot -6} + 2} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
        18. lower-fma.f64100.0%

          \[\leadsto \frac{-0.4244131815783876}{\sqrt{\color{blue}{\mathsf{fma}\left(v \cdot v, -6, 2\right)}} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
      6. Applied rewrites100.0%

        \[\leadsto \color{blue}{\frac{-0.4244131815783876}{\sqrt{\mathsf{fma}\left(v \cdot v, -6, 2\right)} \cdot \mathsf{fma}\left(v, v, -1\right)}} \]
      7. Taylor expanded in v around 0

        \[\leadsto \frac{-0.4244131815783876}{\sqrt{\color{blue}{2}} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
      8. Step-by-step derivation
        1. Applied rewrites98.9%

          \[\leadsto \frac{-0.4244131815783876}{\sqrt{\color{blue}{2}} \cdot \mathsf{fma}\left(v, v, -1\right)} \]
        2. Add Preprocessing

        Alternative 7: 98.8% accurate, 30.0× speedup?

        \[0.30010543871903533 \]
        (FPCore (v)
          :precision binary64
          0.30010543871903533)
        double code(double v) {
        	return 0.30010543871903533;
        }
        
        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(v)
        use fmin_fmax_functions
            real(8), intent (in) :: v
            code = 0.30010543871903533d0
        end function
        
        public static double code(double v) {
        	return 0.30010543871903533;
        }
        
        def code(v):
        	return 0.30010543871903533
        
        function code(v)
        	return 0.30010543871903533
        end
        
        function tmp = code(v)
        	tmp = 0.30010543871903533;
        end
        
        code[v_] := 0.30010543871903533
        
        0.30010543871903533
        
        Derivation
        1. Initial program 98.5%

          \[\frac{4}{\left(\left(3 \cdot \pi\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \sqrt{2 - 6 \cdot \left(v \cdot v\right)}} \]
        2. Taylor expanded in v around 0

          \[\leadsto \color{blue}{\frac{\frac{4}{3}}{\pi \cdot \sqrt{2}}} \]
        3. Step-by-step derivation
          1. lower-/.f64N/A

            \[\leadsto \frac{\frac{4}{3}}{\color{blue}{\mathsf{PI}\left(\right) \cdot \sqrt{2}}} \]
          2. lower-*.f64N/A

            \[\leadsto \frac{\frac{4}{3}}{\mathsf{PI}\left(\right) \cdot \color{blue}{\sqrt{2}}} \]
          3. lower-PI.f64N/A

            \[\leadsto \frac{\frac{4}{3}}{\pi \cdot \sqrt{\color{blue}{2}}} \]
          4. lower-sqrt.f6498.8%

            \[\leadsto \frac{1.3333333333333333}{\pi \cdot \sqrt{2}} \]
        4. Applied rewrites98.8%

          \[\leadsto \color{blue}{\frac{1.3333333333333333}{\pi \cdot \sqrt{2}}} \]
        5. Evaluated real constant98.8%

          \[\leadsto 0.30010543871903533 \]
        6. Add Preprocessing

        Reproduce

        ?
        herbie shell --seed 2025210 
        (FPCore (v)
          :name "Falkner and Boettcher, Equation (22+)"
          :precision binary64
          (/ 4.0 (* (* (* 3.0 PI) (- 1.0 (* v v))) (sqrt (- 2.0 (* 6.0 (* v v)))))))