Falkner and Boettcher, Appendix B, 2

Time bar (total: 23.1s)

analyze6.0ms (0%)

Algorithm
1×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%100%0%0%0%0%0
0%0%100%0%0%0%0%1
0%0%100%0%0%0%0%2
0%0%50%0%0%50%0%3
50%25%25%0%0%50%0%4
75%37.5%12.5%0%0%50%0%5
87.5%43.7%6.2%0%0%50%0%6
93.8%46.9%3.1%0%0%50%0%7
96.9%48.4%1.6%0%0%50%0%8
98.4%49.2%0.8%0%0%50%0%9
99.2%49.6%0.4%0%0%50%0%10
99.6%49.8%0.2%0%0%50%0%11
99.8%49.9%0.1%0%0%50%0%12
Compiler

Compiled 21 to 15 computations (28.6% saved)

sample22.3s (96.7%)

Results
3.2s8256×0valid
832.0ms8239×0valid-sollya
9.0ms17×0exit-sollya
3.0ms16×0invalid
2.0ms16×0invalid-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(6.629095439362246e-182)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.209678#f
(-3.980588924866062e-268)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.305668#f
(1.1851552574479981e-254)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.21610100000000002#f
(-2.3992295658336464e-185)0.3535533905932738(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.2126148409784782e-204)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.136934#f
(5.726261778072002e-179)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.314666#f
(3.130752147779865e-259)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.127432#f
(2.5572211164207467e-295)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.180482#f
(-3.663968354027647e-280)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.21617699999999998#f
(2.7686755788454647e-218)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.22634200000000002#f
(-4.732665969350928e-238)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.251375#f
(2.938735423388279e-15)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.250817#f
(-8.988489880714934e-151)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.269952#f
(-8.355051403723686e-129)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.221227#f
(-1.4924540870158805e-179)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.28308700000000003#f
(3.7323420583905084e-202)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.220085#f
(5.26108432391192e-190)0.3535533905932738(0.3535533905932738 0.3535533905932738)+nan.0validexit00.201721#f
Sollya timings
Total time spent in Sollya 842.0ms
Bogosity

preprocess562.0ms (2.4%)

Algorithm
1×egg-herbie
Rules
1731×fma-define
509×distribute-lft-in
502×fma-neg
465×distribute-rgt-in
435×unsub-neg
Iterations

Useful iterations: 4 (0.0ms)

IterNodesCost
028280
181276
2199260
3637256
41910244
54131244
65472244
75803244
85857244
95917244
106013244
117603244
Stop Event
1×node limit
Calls
Call 1
Inputs
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))))) (-.f64 #s(literal 1 binary64) (*.f64 (neg.f64 v) (neg.f64 v))))
(neg.f64 (*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))))) (-.f64 #s(literal 1 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))))
Outputs
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (*.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -3 binary64) (*.f64 v v)))) (-.f64 #s(literal 1 binary64) (*.f64 v v))))
(*.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -3 binary64)))) #s(literal 4 binary64))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (*.f64 (sqrt.f64 (fma.f64 (*.f64 v v) #s(literal -3 binary64) #s(literal 1 binary64))) (-.f64 #s(literal 1 binary64) (*.f64 v v))) #s(literal 4 binary64)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (-.f64 #s(literal 1/4 binary64) (/.f64 (*.f64 v v) #s(literal 4 binary64)))))
(*.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) #s(literal -1/4 binary64))) (fma.f64 v v #s(literal -1 binary64)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (*.f64 (fma.f64 v v #s(literal -1 binary64)) #s(literal -1/4 binary64))))
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (*.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -3 binary64) (*.f64 v v)))) (-.f64 #s(literal 1 binary64) (*.f64 v v))))
(*.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -3 binary64)))) #s(literal 4 binary64))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (*.f64 (sqrt.f64 (fma.f64 (*.f64 v v) #s(literal -3 binary64) #s(literal 1 binary64))) (-.f64 #s(literal 1 binary64) (*.f64 v v))) #s(literal 4 binary64)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (-.f64 #s(literal 1/4 binary64) (/.f64 (*.f64 v v) #s(literal 4 binary64)))))
(*.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) #s(literal -1/4 binary64))) (fma.f64 v v #s(literal -1 binary64)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (*.f64 (fma.f64 v v #s(literal -1 binary64)) #s(literal -1/4 binary64))))
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))))) (-.f64 #s(literal 1 binary64) (*.f64 (neg.f64 v) (neg.f64 v))))
(*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (*.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -3 binary64) (*.f64 v v)))) (-.f64 #s(literal 1 binary64) (*.f64 v v))))
(*.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -3 binary64)))) #s(literal 4 binary64))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (/.f64 (*.f64 (sqrt.f64 (fma.f64 (*.f64 v v) #s(literal -3 binary64) #s(literal 1 binary64))) (-.f64 #s(literal 1 binary64) (*.f64 v v))) #s(literal 4 binary64)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (-.f64 #s(literal 1/4 binary64) (/.f64 (*.f64 v v) #s(literal 4 binary64)))))
(*.f64 (*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) #s(literal -1/4 binary64))) (fma.f64 v v #s(literal -1 binary64)))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (*.f64 (fma.f64 v v #s(literal -1 binary64)) #s(literal -1/4 binary64))))
(neg.f64 (*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))))) (-.f64 #s(literal 1 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))))
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -3 binary64) (*.f64 v v))))) (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 v v))))
(*.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -3 binary64)))) (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (+.f64 #s(literal -1 binary64) (*.f64 v v))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (/.f64 (sqrt.f64 (fma.f64 (*.f64 v v) #s(literal -3 binary64) #s(literal 1 binary64))) #s(literal 4 binary64)) (+.f64 (*.f64 v v) #s(literal -1 binary64))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (fma.f64 v v #s(literal -1 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) #s(literal 1/4 binary64))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (/.f64 (fma.f64 v v #s(literal -1 binary64)) #s(literal 4 binary64))))
(*.f64 (sqrt.f64 #s(literal 2 binary64)) (*.f64 (sqrt.f64 (fma.f64 v (*.f64 v #s(literal -3 binary64)) #s(literal 1 binary64))) (*.f64 (fma.f64 v v #s(literal -1 binary64)) #s(literal 1/4 binary64))))
Symmetry

(abs v)

Compiler

Compiled 20 to 14 computations (30% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune4.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
100.0%
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
Compiler

Compiled 40 to 28 computations (30% saved)

simplify11.0ms (0%)

Algorithm
1×egg-herbie
Rules
7×*-commutative
6×sub-neg
6×+-commutative
4×neg-sub0
4×neg-mul-1
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01969
13769
25369
36169
46569
Stop Event
1×saturated
Calls
Call 1
Inputs
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))
Outputs
(*.f64 (*.f64 (/.f64 (sqrt.f64 #s(literal 2 binary64)) #s(literal 4 binary64)) (sqrt.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 3 binary64) (*.f64 v v))))) (-.f64 #s(literal 1 binary64) (*.f64 v v)))

soundness2.0ms (0%)

Stop Event
1×fuel
Compiler

Compiled 20 to 14 computations (30% saved)

preprocess175.0ms (0.8%)

Remove

(abs v)

Compiler

Compiled 160 to 112 computations (30% saved)

end0.0ms (0%)

Profiling

Loading profile data...