ENA, Section 1.4, Mentioned, A

Time bar (total: 17.1s)

analyze6.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%49.6%50.4%0%0%0%0
0%0%49.6%50.4%0%0%0%1
0%0%49.6%50.4%0%0%0%2
50%24.8%24.8%50.4%0%0%0%3
75%37.2%12.4%50.4%0%0%0%4
87.5%43.4%6.2%50.4%0%0%0%5
93.8%46.5%3.1%50.4%0%0%0%6
96.9%48.1%1.6%50.4%0%0%0%7
98.4%48.8%0.8%50.4%0%0%0%8
99.2%49.2%0.4%50.4%0%0%0%9
99.6%49.4%0.2%50.4%0%0%0%10
99.8%49.5%0.1%50.4%0%0%0%11
99.9%49.6%0%50.4%0%0%0%12
Compiler

Compiled 12 to 9 computations (25% saved)

sample16.9s (98.8%)

Results
3.5s8219×1valid
968.0ms8139×1valid-sollya
9.0ms80×1exit-sollya
28.0ms37×0valid
3.0ms37×0valid-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(8.741843594072579e-51)3.820991471161389e-101(0.0 5.421010862427522e-20)+nan.0validexit10.13174#f
(-3.1493692019775336e-219)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.070063#f
(-9.408876686295511e-61)4.4263480248957605e-121(0.0 5.421010862427522e-20)+nan.0validexit10.13415200000000002#f
(-4.4624144596408263e-296)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.093327#f
(1.773912661545769e-257)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132176#f
(-2.931419808215186e-191)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13526400000000002#f
(5.629553136860151e-201)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.073477#f
(1.7674151309525849e-168)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.12843300000000002#f
(2.6032106996938558e-132)3.388352973500287e-264(0.0 5.421010862427522e-20)+nan.0validexit10.064248#f
(-4.9722891180773084e-253)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.134613#f
(9.159901255023456e-289)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13866099999999998#f
(5.109226814430423e-261)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.150127#f
(1.2979284715928923e-266)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13299699999999998#f
(3.334581035823542e-254)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.133183#f
(-6.850180004688287e-284)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.075448#f
(1.1192284564017638e-204)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132461#f
(-2.6294099059817915e-113)3.456898226837587e-226(0.0 5.421010862427522e-20)+nan.0validexit10.12293499999999999#f
(2.6155847003301593e-159)3.420644e-318(0.0 5.421010862427522e-20)+nan.0validexit10.137965#f
(6.021836789843962e-87)1.8131259161759113e-173(0.0 5.421010862427522e-20)+nan.0validexit10.071298#f
(4.1998644030830035e-287)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.125258#f
(-8.795490622578112e-269)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.127274#f
(-4.627706078243044e-90)1.0707831773303806e-179(0.0 5.421010862427522e-20)1.070783177330381e-179validvalid10.122514#f
(4.3871069552653926e-209)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.132174#f
(6.136534267717958e-279)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.114218#f
(3.464791021319129e-218)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.111456#f
(-2.0526073899887925e-17)2.1065985487183013e-34(0.0 5.421010862427522e-20)+nan.0validexit10.06545699999999999#f
(2.0185367941710797e-299)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.105463#f
(6.663421607480722e-243)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07313599999999999#f
(1.941201915016436e-35)1.884132437431739e-70(0.0 5.421010862427522e-20)+nan.0validexit10.073964#f
(5.789146001152089e-284)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.107904#f
(4.027419393164757e-222)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.134096#f
(-1.340605019039333e-85)8.986109085367251e-171(0.0 5.421010862427522e-20)+nan.0validexit10.12692#f
(4.8306025974620436e-245)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.165649#f
(-2.101659596269566e-146)2.208486529295978e-292(0.0 5.421010862427522e-20)+nan.0validexit10.118905#f
(-1.092948231597483e-22)5.972679184760326e-45(0.0 5.421010862427522e-20)+nan.0validexit10.06515599999999999#f
(2.754072234392288e-302)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.135875#f
(-2.7690379368102264e-211)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13169399999999998#f
(-5.4320957458303585e-105)1.4753832095934138e-209(0.0 5.421010862427522e-20)+nan.0validexit10.06546#f
(2.8536447594525935e-210)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.130124#f
(-5.207868488520143e-290)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.151381#f
(-6.19751559822777e-156)1.920459979514e-311(0.0 5.421010862427522e-20)+nan.0validexit10.130801#f
(-2.5823387170191258e-219)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13163000000000002#f
(-3.765979680504707e-294)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.172299#f
(1.3095442298802987e-26)8.574530450063924e-53(0.0 5.421010862427522e-20)+nan.0validexit10.147851#f
(-4.184471514624236e-125)8.754900928350824e-250(0.0 5.421010862427522e-20)+nan.0validexit10.132611#f
(9.490884443195943e-105)4.503844375704938e-209(0.0 5.421010862427522e-20)+nan.0validexit10.071804#f
(7.529132246854853e-254)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07313700000000001#f
(1.0588791596435444e-72)5.6061253736370934e-145(0.0 5.421010862427522e-20)+nan.0validexit10.072255#f
(-6.433954191306387e-304)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.15003#f
(1.6545513542927307e-177)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.10556499999999999#f
(-3.3921561099151343e-187)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.108394#f
(1.5711368231831376e-202)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07263700000000001#f
(6.963904543958772e-11)2.4247983248684815e-21(0.0 5.421010862427522e-20)+nan.0validexit10.070219#f
(-1.7429324427658228e-289)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.133525#f
(-7.470293675560416e-201)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.074469#f
(3.0755485650342603e-279)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.152069#f
(-3.980749084837155e-212)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.063705#f
(-5.701796683295484e-296)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.089715#f
(2.6720554026339903e-153)3.569940037372748e-306(0.0 5.421010862427522e-20)+nan.0validexit10.070035#f
(-1.003834652421197e-294)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.143549#f
(-4.265198206409997e-285)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.131106#f
(5.787787020025393e-283)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.147763#f
(-7.926653076826778e-248)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.111753#f
(1.1310634428188389e-274)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07607699999999999#f
(-1.0464495704321998e-252)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13483599999999998#f
(1.0133155205596122e-280)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.13255799999999998#f
(5.206618298025449e-231)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.10892099999999999#f
(1.7521536917155642e-187)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.10266499999999999#f
(-1.642240251813484e-21)1.3484765223382077e-42(0.0 5.421010862427522e-20)+nan.0validexit10.163644#f
(-2.685302872353258e-241)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.126471#f
(1.1235746187218632e-299)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.07522899999999999#f
(1.9052112292054042e-136)1.8149149139451837e-272(0.0 5.421010862427522e-20)+nan.0validexit10.129916#f
(6.804174891606374e-148)2.3148397977783306e-295(0.0 5.421010862427522e-20)+nan.0validexit10.137219#f
(-8.211519123595765e-70)3.371452315858948e-139(0.0 5.421010862427522e-20)+nan.0validexit10.109153#f
(-1.2014505967352347e-150)7.217417681977258e-301(0.0 5.421010862427522e-20)+nan.0validexit10.137869#f
(1.3083230623302837e-297)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.12670499999999998#f
(9.453531253156073e-302)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.137563#f
(1.572866299456827e-276)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.145167#f
(-3.926846693297201e-127)7.71006247632958e-254(0.0 5.421010862427522e-20)+nan.0validexit10.073947#f
(2.292669632430161e-193)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.075423#f
(5.492384499501878e-255)-0.0(0.0 5.421010862427522e-20)+nan.0validexit10.133481#f
Sollya timings
Total time spent in Sollya 980.0ms
Bogosity

preprocess132.0ms (0.8%)

Algorithm
egg-herbie
Rules
16×fma-neg
11×fma-define
sub-neg
associate--r+
associate-+l-
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
01360
12556
24456
36656
410656
513156
614156
714356
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x)))
(neg.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))))
Outputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x)))
(-.f64 #s(literal 1 binary64) (cos.f64 x))
(neg.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))))
(neg.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)))
(+.f64 #s(literal -1 binary64) (cos.f64 x))
(+.f64 (cos.f64 x) #s(literal -1 binary64))
Symmetry

(abs x)

Compiler

Compiled 5 to 4 computations (20% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
57.8%
(-.f64 #s(literal 1 binary64) (cos.f64 x))
Compiler

Compiled 10 to 8 computations (20% saved)

simplify2.0ms (0%)

Algorithm
egg-herbie
Rules
1-exp
sub-neg
+-commutative
*-commutative
neg-sub0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0914
11614
22014
32214
42314
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))
Outputs
(-.f64 #s(literal 1 binary64) (cos.f64 x))

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 5 to 4 computations (20% saved)

preprocess60.0ms (0.4%)

Remove

(abs x)

Compiler

Compiled 62 to 46 computations (25.8% saved)

end0.0ms (0%)

Profiling

Loading profile data...