Average Error: 0.0 → 0.0
Time: 1.5m
Precision: 64
Internal Precision: 128
\[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
\[\sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \frac{\left(1 - {v}^{6}\right) \cdot \left(1 - {v}^{6}\right)}{(\left(v \cdot v\right) \cdot \left((v \cdot v + 1)_*\right) + 1)_* \cdot (\left(v \cdot v\right) \cdot \left((v \cdot v + 1)_*\right) + 1)_*}\right)}\]

Error

Bits error versus v

Derivation

  1. Initial program 0.0

    \[\left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \left(1 - v \cdot v\right)\]
  2. Using strategy rm
  3. Applied add-cbrt-cube0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \color{blue}{\sqrt[3]{\left(\left(1 - v \cdot v\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \left(1 - v \cdot v\right)}}\]
  4. Applied add-cbrt-cube0.0

    \[\leadsto \left(\frac{\sqrt{2}}{4} \cdot \color{blue}{\sqrt[3]{\left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}}}\right) \cdot \sqrt[3]{\left(\left(1 - v \cdot v\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \left(1 - v \cdot v\right)}\]
  5. Applied add-cbrt-cube0.0

    \[\leadsto \left(\color{blue}{\sqrt[3]{\left(\frac{\sqrt{2}}{4} \cdot \frac{\sqrt{2}}{4}\right) \cdot \frac{\sqrt{2}}{4}}} \cdot \sqrt[3]{\left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}}\right) \cdot \sqrt[3]{\left(\left(1 - v \cdot v\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \left(1 - v \cdot v\right)}\]
  6. Applied cbrt-unprod0.0

    \[\leadsto \color{blue}{\sqrt[3]{\left(\left(\frac{\sqrt{2}}{4} \cdot \frac{\sqrt{2}}{4}\right) \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(\left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)}} \cdot \sqrt[3]{\left(\left(1 - v \cdot v\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \left(1 - v \cdot v\right)}\]
  7. Applied cbrt-unprod0.0

    \[\leadsto \color{blue}{\sqrt[3]{\left(\left(\left(\frac{\sqrt{2}}{4} \cdot \frac{\sqrt{2}}{4}\right) \cdot \frac{\sqrt{2}}{4}\right) \cdot \left(\left(\sqrt{1 - 3 \cdot \left(v \cdot v\right)} \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right) \cdot \sqrt{1 - 3 \cdot \left(v \cdot v\right)}\right)\right) \cdot \left(\left(\left(1 - v \cdot v\right) \cdot \left(1 - v \cdot v\right)\right) \cdot \left(1 - v \cdot v\right)\right)}}\]
  8. Simplified0.0

    \[\leadsto \sqrt[3]{\color{blue}{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \left(\left(1 - v \cdot v\right) \cdot \left(1 - v \cdot v\right)\right)\right)}}\]
  9. Using strategy rm
  10. Applied flip3--0.0

    \[\leadsto \sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \left(\left(1 - v \cdot v\right) \cdot \color{blue}{\frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}}\right)\right)}\]
  11. Applied flip3--0.0

    \[\leadsto \sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \left(\color{blue}{\frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}} \cdot \frac{{1}^{3} - {\left(v \cdot v\right)}^{3}}{1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)}\right)\right)}\]
  12. Applied frac-times0.0

    \[\leadsto \sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \color{blue}{\frac{\left({1}^{3} - {\left(v \cdot v\right)}^{3}\right) \cdot \left({1}^{3} - {\left(v \cdot v\right)}^{3}\right)}{\left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)}}\right)}\]
  13. Simplified0.0

    \[\leadsto \sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \frac{\color{blue}{\left(1 - {v}^{6}\right) \cdot \left(1 - {v}^{6}\right)}}{\left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right) \cdot \left(1 \cdot 1 + \left(\left(v \cdot v\right) \cdot \left(v \cdot v\right) + 1 \cdot \left(v \cdot v\right)\right)\right)}\right)}\]
  14. Simplified0.0

    \[\leadsto \sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \frac{\left(1 - {v}^{6}\right) \cdot \left(1 - {v}^{6}\right)}{\color{blue}{(\left(v \cdot v\right) \cdot \left((v \cdot v + 1)_*\right) + 1)_* \cdot (\left(v \cdot v\right) \cdot \left((v \cdot v + 1)_*\right) + 1)_*}}\right)}\]
  15. Final simplification0.0

    \[\leadsto \sqrt[3]{\left(\sqrt{(-3 \cdot \left(v \cdot v\right) + 1)_*} \cdot \frac{\frac{1}{2} \cdot \sqrt{2}}{16}\right) \cdot \left(\left((-3 \cdot \left(v \cdot v\right) + 1)_* \cdot \left(1 - v \cdot v\right)\right) \cdot \frac{\left(1 - {v}^{6}\right) \cdot \left(1 - {v}^{6}\right)}{(\left(v \cdot v\right) \cdot \left((v \cdot v + 1)_*\right) + 1)_* \cdot (\left(v \cdot v\right) \cdot \left((v \cdot v + 1)_*\right) + 1)_*}\right)}\]

Reproduce

herbie shell --seed 2019010 +o rules:numerics
(FPCore (v)
  :name "Falkner and Boettcher, Appendix B, 2"
  (* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v))))

Details

Time bar (total: 1.5m)Debug log

sample140.0ms

Algorithm
intervals

simplify202.0ms

Counts
1 → 1
Calls
1 calls:
Slowest
202.0ms
(* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))

prune10.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 0.0b

localize25.0ms

Local error

Found 4 expressions with local error:

0.2b
(* 3 (* v v))
0.0b
(* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))
0.0b
(sqrt (- 1 (* 3 (* v v))))
0.0b
(* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))

rewrite24.0ms

Algorithm
rewrite-expression-head
Rules
18×sqrt-div
18×frac-times
15×flip--
15×flip3--
11×add-exp-log
11×add-cbrt-cube
11×pow1
10×associate-*r/
10×associate-*r*
10×add-sqr-sqrt
add-cube-cbrt
associate-*l/
*-un-lft-identity
sqrt-prod
associate-*l*
add-log-exp
log1p-expm1-u
cbrt-unprod
prod-exp
pow-prod-down
expm1-log1p-u
*-commutative
distribute-lft-in
sub-neg
distribute-rgt-in
div-inv
pow1/2
rem-sqrt-square
Counts
4 → 96
Calls
4 calls:
Slowest
14.0ms
(* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))
6.0ms
(* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
1.0ms
(sqrt (- 1 (* 3 (* v v))))
1.0ms
(* 3 (* v v))

series249.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
128.0ms
(* (* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v))))) (- 1 (* v v)))
73.0ms
(* (/ (sqrt 2) 4) (sqrt (- 1 (* 3 (* v v)))))
37.0ms
(sqrt (- 1 (* 3 (* v v))))
12.0ms
(* 3 (* v v))

simplify14.5s

Counts
78 → 108
Calls
78 calls:
Slowest
1.0s
(* (* (* (/ (sqrt 2) 4) (/ (sqrt 2) 4)) (/ (sqrt 2) 4)) (* (* (sqrt (- 1 (* 3 (* v v)))) (sqrt (- 1 (* 3 (* v v))))) (sqrt (- 1 (* 3 (* v v))))))
763.0ms
(* (* (sqrt 2) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (- (pow 1 3) (pow (* v v) 3)))
580.0ms
(* (* 4 (sqrt (+ 1 (* 3 (* v v))))) (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))))
469.0ms
(* (sqrt (+ (* 1 1) (+ (* (* 3 (* v v)) (* 3 (* v v))) (* 1 (* 3 (* v v)))))) (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))))
430.0ms
(* (* (/ (sqrt 2) 4) (sqrt (- (pow 1 3) (pow (* 3 (* v v)) 3)))) (- 1 (* v v)))

prune1.3s

Pruning

3 alts after pruning (2 fresh and 1 done)

Merged error: 0b

localize39.0ms

Local error

Found 4 expressions with local error:

0.0b
(* (fma -3 (* v v) 1) (- 1 (* v v)))
0.0b
(* (- 1 (* v v)) (- 1 (* v v)))
0.0b
(* (* (fma -3 (* v v) 1) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))
0.0b
(cbrt (* (* (sqrt (fma -3 (* v v) 1)) (/ (* 1/2 (sqrt 2)) 16)) (* (* (fma -3 (* v v) 1) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))))

rewrite101.0ms

Algorithm
rewrite-expression-head
Rules
153×associate-*r/
114×frac-times
88×flip--
88×flip3--
53×cbrt-div
27×associate-*l/
23×pow1
20×add-exp-log
20×add-cbrt-cube
12×distribute-lft-in
12×distribute-rgt-in
10×cbrt-unprod
10×prod-exp
10×pow-prod-down
add-cube-cbrt
*-un-lft-identity
sub-neg
add-sqr-sqrt
associate-*l*
associate-*r*
add-log-exp
log1p-expm1-u
expm1-log1p-u
*-commutative
pow-prod-up
pow1/3
pow-plus
pow2
cbrt-prod
Counts
4 → 181
Calls
4 calls:
Slowest
66.0ms
(cbrt (* (* (sqrt (fma -3 (* v v) 1)) (/ (* 1/2 (sqrt 2)) 16)) (* (* (fma -3 (* v v) 1) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))))
18.0ms
(* (* (fma -3 (* v v) 1) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))
5.0ms
(* (- 1 (* v v)) (- 1 (* v v)))
4.0ms
(* (fma -3 (* v v) 1) (- 1 (* v v)))

series407.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
298.0ms
(cbrt (* (* (sqrt (fma -3 (* v v) 1)) (/ (* 1/2 (sqrt 2)) 16)) (* (* (fma -3 (* v v) 1) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))))
50.0ms
(* (* (fma -3 (* v v) 1) (- 1 (* v v))) (* (- 1 (* v v)) (- 1 (* v v))))
36.0ms
(* (fma -3 (* v v) 1) (- 1 (* v v)))
22.0ms
(* (- 1 (* v v)) (- 1 (* v v)))

simplify49.9s

Counts
171 → 193
Calls
171 calls:
Slowest
1.5s
(* (+ 1 (* v v)) (* (+ 1 (* v v)) (+ 1 (* v v))))
1.3s
(* (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))) (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))))
1.3s
(* (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))) (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))))
1.2s
(* (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))) (+ (* 1 1) (+ (* (* v v) (* v v)) (* 1 (* v v)))))
1.1s
(* (* (- 1 (* v v)) (- (* v v))) (* (fma -3 (* v v) 1) (- 1 (* v v))))

prune2.8s

Pruning

2 alts after pruning (1 fresh and 1 done)

Merged error: 0b

localize54.0ms

Local error

Found 4 expressions with local error:

0.0b
(/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1)))
0.0b
(* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))
0.0b
(* (fma -3 (* v v) 1) (- 1 (* v v)))
0.0b
(* (* (fma -3 (* v v) 1) (- 1 (* v v))) (/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))))

rewrite51.0ms

Algorithm
rewrite-expression-head
Rules
61×add-exp-log
61×add-cbrt-cube
29×cbrt-unprod
29×prod-exp
16×pow1
12×div-exp
12×cbrt-undiv
11×associate-*r*
flip--
add-cube-cbrt
associate-*r/
flip3--
*-un-lft-identity
add-sqr-sqrt
associate-/l/
associate-*l*
frac-times
pow-prod-down
add-log-exp
log1p-expm1-u
associate-*l/
expm1-log1p-u
*-commutative
distribute-lft-in
distribute-rgt-in
div-inv
fma-udef
times-frac
sub-neg
associate-/l*
pow-prod-up
pow-plus
frac-2neg
associate-/r*
clear-num
pow2
Counts
4 → 123
Calls
4 calls:
Slowest
18.0ms
(* (* (fma -3 (* v v) 1) (- 1 (* v v))) (/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))))
15.0ms
(/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1)))
8.0ms
(* (fma -3 (* v v) 1) (- 1 (* v v)))
8.0ms
(* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))

series174.0ms

Counts
4 → 12
Calls
4 calls:
Slowest
73.0ms
(* (* (fma -3 (* v v) 1) (- 1 (* v v))) (/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))))
44.0ms
(/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1)))
36.0ms
(* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))
21.0ms
(* (fma -3 (* v v) 1) (- 1 (* v v)))

simplify14.9s

Counts
94 → 135
Calls
94 calls:
Slowest
684.0ms
(- (log (* (- 1 (pow v 6)) (- 1 (pow v 6)))) (log (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))))
651.0ms
(- (+ (log (- 1 (pow v 6))) (log (- 1 (pow v 6)))) (log (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))))
554.0ms
(* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))
553.0ms
(* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))
481.0ms
(* (* (* (* (fma -3 (* v v) 1) (fma -3 (* v v) 1)) (fma -3 (* v v) 1)) (* (* (- 1 (* v v)) (- 1 (* v v))) (- 1 (* v v)))) (* (* (/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1))) (/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1)))) (/ (* (- 1 (pow v 6)) (- 1 (pow v 6))) (* (fma (* v v) (fma v v 1) 1) (fma (* v v) (fma v v 1) 1)))))

prune1.8s

Pruning

2 alts after pruning (0 fresh and 2 done)

Merged error: 0b

regimes59.0ms

Accuracy

0% (0.0b remaining)

Error of 0.0b against oracle of 0.0b and baseline of 0.0b

bsearch3.0ms

end0.0ms

sample2.0s

Algorithm
intervals