2tan (problem 3.3.2)

Time bar (total: 24.9s)

analyze212.0ms (0.9%)

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)

sample24.2s (97.2%)

Results
7.5s25998×0precondition
2.1s4438×1valid
463.0ms4418×1valid-sollya
1.1s3818×0valid
390.0ms3789×0valid-sollya
20.0ms29×0exit-sollya
13.0ms20×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-1.0972852531084486e-173 4.359199671261908e-180)4.359199671261908e-180(+nan.0 +nan.0)+nan.0validexit05.0#f
(2.726914241081695e-125 4.321493062696554e-139)4.321493062696554e-139(+nan.0 +nan.0)+nan.0validexit15.0#f
(-1.0904187160430754e-131 3.1606520852184275e-140)3.1606520852184275e-140(3.1606520851019254e-140 3.1606520852852216e-140)+nan.0validexit10.11922200000000001#f
(-7.489212238850004e-256 4.935890686534263e-259)4.935890686534263e-259(4.9358906865342626e-259 4.9358906865342637e-259)+nan.0validexit00.214142#f
(-4.159652494177682e-290 9.681918573363738e-299)9.681918573363738e-299(9.68191857301221e-299 9.681918573846613e-299)+nan.0validexit10.20957699999999999#f
(-1.5826165826745392e-287 9.645767826349906e-294)9.645767826349906e-294(9.645767826348265e-294 9.645767826352538e-294)+nan.0validexit00.121354#f
(-1.9618519330553317e-205 2.5970524143799913e-206)2.5970524143799913e-206(2.5970524143799913e-206 2.5970524143799913e-206)+nan.0validexit00.219935#f
(6.022022090143177e-250 2.2065984125286042e-254)2.2065984125286042e-254(+nan.0 +nan.0)+nan.0validexit05.0#f
(-3.729754600520363e-268 2.0399628388939873e-275)2.0399628388939873e-275(2.0399628388912687e-275 2.0399628388991494e-275)+nan.0validexit00.213533#f
(-6.141858092855277e-16 1.5919297861537028e-18)1.5919297861537028e-18(1.5919297861537028e-18 1.5919297861537028e-18)+nan.0validexit00.144499#f
(-1.6004863383546148e-174 5.904208559420117e-182)5.904208559420117e-182(+nan.0 +nan.0)+nan.0validexit15.0#f
(9.175997036159539e-240 5.952482573869105e-244)5.952482573869105e-244(5.9524825738691e-244 5.95248257386911e-244)+nan.0validexit00.111284#f
(1.9353165772177386e-226 1.3161667573965878e-233)1.3161667573965878e-233(1.3161667573932697e-233 1.3161667573987618e-233)+nan.0validexit00.214141#f
(1.3369450698529266e-129 1.3088103457270182e-136)1.3088103457270182e-136(1.3088103457261495e-136 1.3088103457284957e-136)+nan.0validexit00.103626#f
(7.476568040894559e-274 2.309064473498497e-286)2.309064473498497e-286(2.309063494701318e-286 2.309064997827588e-286)+nan.0validexit10.137449#f
(-1.0966162660790255e-220 1.4719653027203904e-222)1.4719653027203904e-222(1.4719653027203904e-222 1.4719653027203904e-222)+nan.0validexit00.209691#f
(2.0524082592628596e-221 3.340189546064972e-231)3.340189546064972e-231(3.3401895440080415e-231 3.340189547607314e-231)+nan.0validexit10.10997699999999999#f
(-7.643386859930042e-292 7.501229477576002e-299)7.501229477576002e-299(7.501229477568407e-299 7.501229477581445e-299)+nan.0validexit00.114356#f
(1.5528712948983125e-274 9.865397241044328e-275)9.865397241044328e-275(9.865397241044328e-275 9.865397241044328e-275)+nan.0validexit00.103523#f
(-4.480631209698749e-38 4.352650791395535e-43)4.352650791395535e-43(4.352650791395509e-43 4.35265079139556e-43)+nan.0validexit00.201709#f
(-6.636160422922087e-115 6.054031140166816e-115)6.054031140166816e-115(6.054031140166816e-115 6.0540311401668165e-115)+nan.0validexit00.247321#f
(9.559082172845132e-119 5.253904275090366e-131)5.253904275090366e-131(5.253903647883942e-131 5.253905260174208e-131)+nan.0validexit10.225232#f
(-1.7520885292768546e-96 3.806442292632514e-104)3.806442292632514e-104(3.806442292619207e-104 3.806442292649662e-104)+nan.0validexit10.217417#f
(4.2564621582836753e-156 5.09699939930737e-157)5.09699939930737e-157(5.09699939930737e-157 5.09699939930737e-157)+nan.0validexit00.159049#f
(7.782300631339085e-175 1.0604271382680433e-190)1.0604271382680433e-190(1.0597398202455629e-190 1.0613836772573192e-190)+nan.0validexit10.206615#f
(-4.5704916605279574e-238 5.192292115927687e-242)5.192292115927687e-242(5.192292115927684e-242 5.19229211592769e-242)+nan.0validexit00.282857#f
(-1.2903987205785379e-257 1.2364110295118753e-262)1.2364110295118753e-262(1.2364110295118615e-262 1.2364110295118886e-262)+nan.0validexit00.17574#f
(5.997562225166075e-195 9.849082752038775e-207)9.849082752038775e-207(9.849082359925329e-207 9.849083473846168e-207)+nan.0validexit10.158883#f
(1.897695513330493e-296 8.661680392456649e-305)8.661680392456649e-305(8.661680392315921e-305 8.661680392713796e-305)+nan.0validexit10.213651#f
(-0.0011353051189661079 3.2879791698653e-16)3.2879834078035343e-16(3.287981789707405e-16 3.2879849660809573e-16)+nan.0validexit10.25005999999999995#f
(1.254748178808562e-74 1.6501128225069443e-78)1.6501128225069443e-78(1.6501128225069426e-78 1.6501128225069455e-78)+nan.0validexit00.16780899999999999#f
(-9.817409313745662e-151 1.530332947725143e-164)1.530332947725143e-164(1.5303212777146553e-164 1.530341150726508e-164)+nan.0validexit10.200669#f
(6.519870100559452e-160 6.067164565376445e-165)6.067164565376445e-165(6.067164565376383e-165 6.067164565376506e-165)+nan.0validexit00.211228#f
(-1.577665923933096e-53 2.1379651246864902e-54)2.1379651246864902e-54(2.1379651246864902e-54 2.1379651246864902e-54)+nan.0validexit00.15030800000000002#f
(5.672452919500615e-189 1.5323454673750942e-193)1.5323454673750942e-193(1.5323454673750888e-193 1.5323454673751005e-193)+nan.0validexit00.20319399999999999#f
(4.760123984281568e-71 4.533159370823303e-85)4.533159370823303e-85(4.533096178603643e-85 4.53321399684681e-85)+nan.0validexit10.101254#f
(-3.9125175426212544e-93 8.040587765406227e-104)8.040587765406227e-104(8.04058769730843e-104 8.040587822053348e-104)+nan.0validexit10.13881000000000002#f
(-6.447488230138817e-243 9.83803882478235e-244)9.83803882478235e-244(9.83803882478235e-244 9.83803882478235e-244)+nan.0validexit00.183506#f
(1.3241560602548326e-249 3.0275290724348123e-256)3.0275290724348123e-256(3.027529072433403e-256 3.027529072437037e-256)+nan.0validexit00.229347#f
(-3.7653126022879506e-285 2.932687581922573e-290)2.932687581922573e-290(2.932687581922502e-290 2.932687581922611e-290)+nan.0validexit00.215088#f
(-2.8992034447525517e-265 5.3641714937932656e-272)5.3641714937932656e-272(5.364171493789827e-272 5.364171493797897e-272)+nan.0validexit00.112061#f
(-2.9725403218394745e-281 8.511863039389448e-289)8.511863039389448e-289(8.511863039351692e-289 8.511863039441286e-289)+nan.0validexit10.254061#f
(9.73091882597129e-99 6.020889400611919e-108)6.020889400611919e-108(6.020889399768899e-108 6.0208894021482196e-108)+nan.0validexit10.104417#f
(1.4302029842904988e-198 4.481316995237064e-208)4.481316995237064e-208(4.481316994066448e-208 4.4813169967859815e-208)+nan.0validexit10.17929900000000001#f
(1.4317532537247445e-235 5.1745549150222066e-247)5.1745549150222066e-247(5.174554762361438e-247 5.17455501810512e-247)+nan.0validexit10.171071#f
(-1.1508221800961144e-168 1.2276746423722535e-172)1.2276746423722535e-172(1.2276746423722515e-172 1.2276746423722549e-172)+nan.0validexit00.231047#f
(-8.674034274833265e-265 5.348622102176717e-267)5.348622102176717e-267(+nan.0 +nan.0)+nan.0validexit05.0#f
(-192.9538755682721 2.865854385294685e-5)0.00045358179688348514(0.00045358179688330955 0.0004535817968835294)+nan.0validexit00.188767#f
(6.111218519834555e-283 1.2290430197170612e-295)1.2290430197170612e-295(1.2290423904836348e-295 1.2290437903790625e-295)+nan.0validexit10.18112999999999999#f
Sollya timings
Total time spent in Sollya 886.0ms
Bogosity

preprocess278.0ms (1.1%)

Algorithm
egg-herbie
Rules
154×fma-neg
59×fma-define
49×sub-neg
39×cancel-sign-sub-inv
35×associate--r+
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
027226
149210
2101210
3201210
4378210
5481210
6638210
7720210
8762210
9768210
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x)))
(-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x))
(neg.f64 (-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x))))
(neg.f64 (-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x)))
(-.f64 (tan.f64 (+.f64 eps x)) (tan.f64 eps))
Outputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x)))
(-.f64 (tan.f64 (+.f64 eps (neg.f64 x))) (neg.f64 (tan.f64 x)))
(+.f64 (tan.f64 x) (tan.f64 (-.f64 eps x)))
(-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x))
(-.f64 (tan.f64 (-.f64 x eps)) (tan.f64 x))
(neg.f64 (-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x))))
(-.f64 (tan.f64 (-.f64 x eps)) (tan.f64 x))
(neg.f64 (-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x)))
(-.f64 (tan.f64 (+.f64 eps (neg.f64 x))) (neg.f64 (tan.f64 x)))
(+.f64 (tan.f64 x) (tan.f64 (-.f64 eps x)))
(-.f64 (tan.f64 (+.f64 eps x)) (tan.f64 eps))
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 eps))
Compiler

Compiled 9 to 6 computations (33.3% saved)

eval1.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune3.0ms (0%)

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

Compiled 18 to 12 computations (33.3% saved)

simplify6.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 (tan.f64 (+.f64 x eps)) (tan.f64 x))
Outputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 6 computations (33.3% saved)

preprocess192.0ms (0.8%)

Compiler

Compiled 60 to 40 computations (33.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...