2cos (problem 3.3.5)

Time bar (total: 1.6min)

analyze177.0ms (0.2%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%50.6%49.4%0%0%0%0
0%0%50.6%49.4%0%0%0%1
0%0%50.6%49.4%0%0%0%2
0%0%25.3%74.7%0%0%0%3
0%0%25.3%74.7%0%0%0%4
0%0%19%81%0%0%0%5
0%0%15.8%84.2%0%0%0%6
0%0%11.1%88.9%0%0%0%7
0%0%8.7%91.3%0%0%0%8
0%0%5.9%94.1%0%0%0%9
0%0%4.5%95.5%0%0%0%10
0%0%3.1%96.9%0%0%0%11
0%0%2.7%97.3%0%0%0%12
Compiler

Compiled 28 to 18 computations (35.7% saved)

sample1.6min (99.5%)

Results
14.4s26375×0precondition
14.2s5679×2valid
1.0s5626×2valid-sollya
3.5s2505×1valid
362.0ms2498×1valid-sollya
8.0ms72×0valid-sollya
151.0ms72×0valid
11.0ms53×2exit-sollya
1.0ms1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(2.118428419556549e-287 6.7543466394035005e-292)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.193858#f
(8.629932029588469e-271 7.825921460344053e-276)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.233029#f
(-1.7798090250138906e-205 2.0861917090805378e-209)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.207207#f
(3.714093682991738e-289 5.603162316327987e-299)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.209892#f
(3.3808456870613023e-234 8.070444700646558e-244)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.211032#f
(8.981394635538744e-159 3.3494988449295894e-162)-3.009e-320(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.219753#f
(3.078695699321999e-54 3.888621468783978e-62)-1.1971882267843313e-115(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.175112#f
(-4.365207213974437e-280 3.7229896212596936e-292)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.210994#f
(-1.0845418150926171e-263 1.9055015800585988e-277)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.154336#f
(8.043082012886981e-69 4.4442720393792097e-69)-4.562142148031138e-137(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.08354600000000001#f
(-4.932531915295882e-252 7.376181011668784e-258)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.190118#f
(2.4333869215732098e-273 2.1751847654420335e-288)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.206428#f
(-5.221889292666693e-245 2.08782061301747e-248)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.206288#f
(1.2674677291159725e-170 4.0344279508270984e-179)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.194062#f
(9.069283590648036e-240 2.477212969947122e-241)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.166318#f
(9.844107979461973e-131 8.740877166464562e-133)-8.642815333008686e-263(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.19581700000000002#f
(-3.943369592738993e-304 3.171428937596322e-308)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.210443#f
(1.3020313844108468e-66 3.7697690876169535e-81)-4.908357664059124e-147(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.219379#f
(-6.720697145231209e-279 2.177533135980097e-288)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.205287#f
(-1.0898499393478398e-251 4.05266991148496e-252)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.223911#f
(-1.4110851137647614e-99 1.806269877286105e-100)2.3856699918005667e-199(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.157716#f
(4.991714253563824e-294 3.026684599580713e-296)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.156022#f
(8.704527300565401e-272 1.703316537255315e-279)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.211746#f
(2.1524149986219758e-275 9.574037004857729e-281)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.201123#f
(-1.025676327318141e-113 5.245379568489165e-116)5.3663046477888206e-229(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.20139100000000001#f
(7.334863371776313e-200 9.680299405914255e-203)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.09918500000000001#f
(-4.244865914104617e-210 4.0985316631024913e-221)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.202089#f
(1.645116716895379e-282 1.3643376448805757e-284)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.20461200000000002#f
(6.139937918165003e-209 7.560453563024172e-217)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.167573#f
(3.1393822183528457e-214 6.0707633939354625e-220)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.21432600000000002#f
(4.32737126998721e-69 7.141647342168171e-84)-3.0904559528879087e-152(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.197276#f
(-3.89503655392608e-167 1.0690191829691145e-175)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.209473#f
(-9.762537653944701e-232 2.763896149907515e-240)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.198522#f
(-1.455860204593099e-84 1.3013452855471012e-99)1.8945768136628668e-183(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.21246#f
(-3.679231811801937e-290 1.0709179126518882e-294)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.235636#f
(-7.893248997246804e-277 1.5863501559696163e-279)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.215911#f
(-9.51452239778178e-294 9.978990395493962e-304)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.211979#f
(-8.327678497074663e-234 2.26280614305787e-246)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.230491#f
(-8.594595206456248e-226 5.477034438961051e-239)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.222685#f
(-1.2469502652591593e-278 2.232776993284186e-285)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.24756700000000004#f
(-4.737809274624826e-193 5.386426729545637e-208)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.196364#f
(-7.2250551682623066e-239 3.8581289295323916e-252)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.15495099999999998#f
(6.891799263580863e-245 2.0825033491936425e-246)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.217144#f
(-1.8304686181480243e-265 1.5115781638842552e-273)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.20837899999999998#f
(1.3949049333770092e-279 5.4939851751825346e-291)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.155134#f
(1.0398133781334904e-224 1.0891560978984653e-225)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.23738700000000001#f
(3.3489888138658653e-296 2.9852379804448376e-300)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.205393#f
(-1.8428650929730973e-186 3.2272524758986127e-189)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.15316200000000002#f
(-2.254902338224058e-148 1.757223184121579e-153)3.962351227490679e-301(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.225534#f
(3.939104439905094e-258 8.52136522636112e-269)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.20469299999999999#f
(-6.964536368846647e-233 5.591747349570045e-248)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.182136#f
(7.604587911841732e-134 7.766163526615847e-149)-5.905847327588906e-282(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.194923#f
(3.641867107159998e-279 1.0375094734764692e-290)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.213303#f
(9.836587325951222e-7 9.777814430297984e-13)-9.618037330338413e-19(-1.0299920638612292e-18 -9.215718466126788e-19)+nan.0validexit10.14752400000000002#f
(-4.2627821404478814e-285 8.12396645493325e-291)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.211342#f
(-1.3604719574052636e-80 1.677466322288873e-92)2.2821458909643445e-172(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit10.156139#f
(-7.851160115946187e-225 6.154122675456037e-230)0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.185116#f
(2.3714090667679166e-297 7.00221161190064e-303)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.200218#f
(-4.551436352770009e-291 1.7672502473856194e-295)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.22226#f
(-8.468243486957143e-304 5.946407148289711e-307)-0.0(-5.421010862427522e-20 5.421010862427522e-20)+nan.0validexit20.19737100000000002#f
Sollya timings
Total time spent in Sollya 1.4s
Bogosity

preprocess183.0ms (0.2%)

Algorithm
egg-herbie
Rules
158×fma-neg
91×fma-define
54×sub-neg
41×associate--r+
36×cancel-sign-sub-inv
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
027234
149218
296210
3184210
4349210
5486210
6636210
7761210
8795210
9821210
10827210
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x)))
(-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x))
(neg.f64 (-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x))))
(neg.f64 (-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x)))
(-.f64 (cos.f64 (+.f64 eps x)) (cos.f64 eps))
Outputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x)))
(-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x))
(-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x))
(-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x))
(-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x))
(neg.f64 (-.f64 (cos.f64 (+.f64 (neg.f64 x) eps)) (cos.f64 (neg.f64 x))))
(neg.f64 (-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x)))
(neg.f64 (-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x)))
(-.f64 (cos.f64 x) (cos.f64 (-.f64 eps x)))
(neg.f64 (-.f64 (cos.f64 (+.f64 x (neg.f64 eps))) (cos.f64 x)))
(neg.f64 (-.f64 (cos.f64 (+.f64 eps (neg.f64 x))) (cos.f64 x)))
(neg.f64 (-.f64 (cos.f64 (-.f64 eps x)) (cos.f64 x)))
(-.f64 (cos.f64 x) (cos.f64 (-.f64 eps x)))
(-.f64 (cos.f64 (+.f64 eps x)) (cos.f64 eps))
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 eps))
Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune21.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
52.4%
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
Compiler

Compiled 18 to 12 computations (33.3% saved)

simplify5.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01230
11530
22030
32230
42330
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))
Outputs
(-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 6 computations (33.3% saved)

preprocess124.0ms (0.1%)

Compiler

Compiled 66 to 44 computations (33.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...