tanhf (example 3.4)

Time bar (total: 21.8s)

analyze120.0ms (0.6%)

Algorithm
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
25%25%75%0%0%0%0%3
37.5%37.5%62.5%0%0%0%0%4
43.8%43.7%56.2%0%0%0%0%5
46.9%46.9%53.1%0%0%0%0%6
48.4%48.4%51.5%0%0%0%0%7
49.2%49.2%50.8%0%0%0%0%8
49.6%49.6%50.4%0%0%0%0%9
49.8%49.8%50.2%0%0%0%0%10
49.9%49.9%50.1%0%0%0%0%11
50%49.9%50%0%0%0%0%12
Compiler

Compiled 9 to 7 computations (22.2% saved)

sample21.5s (98.6%)

Results
1.8s4176×0valid
379.0ms4162×0valid-sollya
975.0ms2097×1valid
213.0ms2084×1valid-sollya
2.3s1981×2valid
235.0ms1923×2valid-sollya
8.0ms58×2exit-sollya
12.0ms14×0exit-sollya
6.0ms13×1exit-sollya
0.0ms3valid-sollya
3.0ms3valid
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(3.961638498990954e+102)-216.999519731647(-216.999519731647 -216.999519731647)+nan.0validexit00.190612#f
(-2.2936334369749944e-102)-1.1468167184874972e-102(-2.3635035899969848e+82 0.0)+nan.0validexit10.172101#f
(2.434632197956838e-285)1.217316098978419e-285(0.0 2.226624155787012e+265)+nan.0validexit20.122962#f
(-7.506636000781934e-273)-3.753318000390967e-273(-7.221624788870592e+252 0.0)+nan.0validexit20.12756#f
(1.0516318968285968e-55)5.258159484142984e-56(0.0 5.1548558756877276e+35)+nan.0validexit10.052628#f
(-1.3976462217485686e-257)-6.988231108742843e-258(-3.878671711103972e+237 0.0)+nan.0validexit20.128357#f
(-3.1738927388327607e-282)-1.5869463694163804e-282(-1.708000650463433e+262 0.0)+nan.0validexit20.136993#f
(9.535868353264892e-277)4.767934176632446e-277(0.0 5.684863361784431e+256)+nan.0validexit20.151735#f
(1.4664292149885105e-266)7.332146074942553e-267(0.0 3.6967422682382904e+246)+nan.0validexit20.129653#f
(-5.18142288876487e-302)-2.590711444382435e-302(-1.0462398030051093e+282 0.0)+nan.0validexit20.10086099999999999#f
(-2.224371673121892e-271)-1.112185836560946e-271(-2.437097598360964e+251 0.0)+nan.0validexit20.159908#f
(-3.225668516970077e-295)-1.6128342584850384e-295(-1.680585228738744e+275 0.0)+nan.0validexit20.085881#f
(-1.2835366467314263e-264)-6.417683233657131e-265(-4.223495196831604e+244 0.0)+nan.0validexit20.154725#f
(7.596478587315018e-302)3.798239293657509e-302(0.0 7.136215550557595e+281)+nan.0validexit20.115611#f
(-3.655695531361777e-293)-1.8278477656808886e-293(-1.4828945178615983e+273 0.0)+nan.0validexit20.16690300000000002#f
(-5.240467711655002e-149)-2.620233855827501e-149(-1.0344517246754493e+129 0.0)+nan.0validexit10.12238299999999999#f
(-8.930451208202852e-233)-4.465225604101426e-233(-6.0702541630239045e+212 0.0)+nan.0validexit20.163663#f
(1.444329043430461e+51)2.650898228571726(2.650898228571726 2.650898228571726)+nan.0validexit00.10314699999999999#f
(-5.444433259500523e-101)-2.7222166297502615e-101(-9.956979182301245e+80 0.0)+nan.0validexit10.081646#f
(-9.737672620205038e-286)-4.868836310102519e-286(-5.567049821719491e+265 0.0)+nan.0validexit20.180093#f
(-6.172258757969692e-130)-3.086129378984846e-130(-8.78286389958595e+109 0.0)+nan.0validexit10.073567#f
(1.8650529014849226e+262)1.2413166430661293(1.2413166430661293 1.2413166430661293)+nan.0validexit00.301869#f
(1.0340197633268579e-303)5.1700988166342895e-304(0.0 5.24265691497612e+283)+nan.0validexit20.095806#f
(1.6240716931219305e+70)0.3507617715158175(+nan.0 +nan.0)+nan.0validexit05.0#f
(-2.1979083071145072e-241)-1.0989541535572536e-241(-2.4664408632880683e+221 0.0)+nan.0validexit20.143276#f
(6.702830941260172e-243)3.351415470630086e-243(0.0 8.087643728350307e+222)+nan.0validexit20.15417#f
(-5.97460384641015e-246)-2.987301923205075e-246(-9.073423111868321e+225 0.0)+nan.0validexit20.16344999999999998#f
(-1.7502267759271666e-265)-8.751133879635833e-266(-3.097319122863831e+245 0.0)+nan.0validexit20.153113#f
(-2.8553400676471445e+211)1.2971860636821468(1.2971860636821468 1.2971860636821468)+nan.0validexit00.127828#f
(-7.736876677207912e-281)-3.868438338603956e-281(-7.006717424354578e+260 0.0)+nan.0validexit20.086827#f
(6.949701104769138e-244)3.474850552384569e-244(0.0 7.800351095254193e+223)+nan.0validexit20.08298#f
(4.0409178812695264e-232)2.0204589406347632e-232(0.0 1.341529578602675e+212)+nan.0validexit20.12717499999999998#f
(-2.0163362439220645e-289)-1.0081681219610322e-289(-2.688545067207082e+269 0.0)+nan.0validexit20.12634#f
(-4.3912135708398e-300)-2.1956067854199e-300(-1.2345131419765534e+280 0.0)+nan.0validexit20.08684700000000001#f
(-1.025850370927124e-283)-5.12925185463562e-284(-5.284406981817652e+263 0.0)+nan.0validexit20.162855#f
(-2.311115568447723e-299)-1.1555577842238614e-299(-2.3456251761864867e+279 0.0)+nan.0validexit20.130869#f
(2.8549680582028825e-279)1.4274840291014412e-279(0.0 1.898799129066224e+259)+nan.0validexit20.169326#f
(-6.718933758282544e-230)-3.359466879141272e-230(-8.06826061612075e+209 0.0)+nan.0validexit20.157607#f
(-2.8128735984395074e-289)-1.4064367992197537e-289(-1.927214527320007e+269 0.0)+nan.0validexit20.17635900000000002#f
(-2.2882091831484528e-240)-1.1441045915742264e-240(-2.369106330990466e+220 0.0)+nan.0validexit20.0833#f
(-1.0925213904405402e-62)-5.462606952202701e-63(+nan.0 +nan.0)+nan.0validexit15.0#f
(-3.0212698037781505e-139)-1.5106349018890752e-139(-1.7942822768256096e+119 0.0)+nan.0validexit10.16595800000000002#f
(-1.428654127581079e-89)-7.143270637905395e-90(-3.7944879434227296e+69 0.0)+nan.0validexit10.116093#f
(-2.1035863962913793e-301)-1.0517931981456897e-301(-2.577032667631222e+281 0.0)+nan.0validexit20.127176#f
(-1.4911373516835538e+210)-0.4440643490238156(-0.4440643490238156 -0.4440643490238156)+nan.0validexit00.129703#f
(1.3796417722755853e-257)6.898208861377927e-258(0.0 3.929288726512021e+237)+nan.0validexit20.14615999999999998#f
(-4.0538656498196914e-287)-2.0269328249098457e-287(-1.3372448252370274e+267 0.0)+nan.0validexit20.08662099999999999#f
(4.258599037102039e-65)2.1292995185510197e-65(0.0 1.2729563913386172e+45)+nan.0validexit10.07620500000000001#f
(2.0341203120984484e-278)1.0170601560492242e-278(0.0 2.6650394424482563e+258)+nan.0validexit20.079545#f
(-9.464311913531483e-198)-4.732155956765741e-198(-5.72784467793892e+177 0.0)+nan.0validexit20.084491#f
(-7.400723736299701e-303)-3.7003618681498505e-303(-7.324973956044442e+282 0.0)+nan.0validexit20.133713#f
(1.4509963597757966e-288)7.254981798878983e-289(0.0 3.736060966593438e+268)+nan.0validexit20.12598199999999998#f
(-1.2359238414124277e-293)-6.179619207062139e-294(-4.386201382952796e+273 0.0)+nan.0validexit20.08538#f
(-6.085990829420094e-256)-3.042995414710047e-256(-8.90735956456258e+235 0.0)+nan.0validexit20.165709#f
(1.2268374042192626e+123)0.4072195152992419(0.4072195152992419 0.4072195152992419)+nan.0validexit00.186#f
(1.6405448047161325e+266)0.6055449362918836(0.6055449362918836 0.6055449362918836)+nan.0validexit00.147101#f
(-6.236824895381938e+167)-18.401970361709147(-18.401970361709147 -18.401970361709147)+nan.0validexit00.1275#f
(-1.4547241163761137e-296)-7.273620581880568e-297(-3.726487243458841e+276 0.0)+nan.0validexit20.127459#f
(6.284321096671998e-292)3.142160548335999e-292(0.0 8.626247416444617e+271)+nan.0validexit20.08518500000000001#f
(6.434726905135384e-200)3.217363452567692e-200(0.0 8.424616836654183e+179)+nan.0validexit20.091867#f
(-6.552612196211234e-297)-3.276306098105617e-297(-8.273053097148017e+276 0.0)+nan.0validexit20.087732#f
(-1.8586883996223394e+296)-5.0091256281679275(-5.0091256281679275 -5.0091256281679275)+nan.0validexit00.241263#f
(7.263062433978403e-263)3.631531216989201e-263(0.0 7.463808705631791e+242)+nan.0validexit20.120512#f
(-1.148378700509894e+239)0.1813088713261446(+nan.0 +nan.0)+nan.0validexit05.0#f
(-6.983572176012366e-236)-3.491786088006183e-236(-7.762518558980413e+215 0.0)+nan.0validexit20.175176#f
(2.9661631652751452e-241)1.4830815826375726e-241(0.0 1.8276172146870624e+221)+nan.0validexit20.15805999999999998#f
(-2.159670956351754e+129)0.03745810527873224(0.03745810527873224 0.03745810527873224)+nan.0validexit00.12331700000000001#f
(7.044486087359406e-260)3.522243043679703e-260(0.0 7.695395796373222e+239)+nan.0validexit20.17328800000000003#f
(-2.802046951610338e-292)-1.401023475805169e-292(-1.9346609660884033e+272 0.0)+nan.0validexit20.189291#f
(9.841350720701714e-227)4.920675360350857e-227(0.0 5.50840125128778e+206)+nan.0validexit20.083914#f
(2.242699359621311e-270)1.1213496798106555e-270(0.0 2.4171812593476113e+250)+nan.0validexit20.140364#f
(8.607181090693601e-301)4.3035905453468005e-301(0.0 6.29824190441272e+280)+nan.0validexit20.176679#f
(-1.5194396780390872e-134)-7.597198390195436e-135(-3.5677697119398694e+114 0.0)+nan.0validexit10.08218800000000001#f
(-1.157971514129332e-120)-5.78985757064666e-121(-4.6814716910402845e+100 0.0)+nan.0validexit10.078982#f
(5.020924315598986e-250)2.510462157799493e-250(0.0 1.079683843388268e+230)+nan.0validexit20.18068199999999998#f
(6.102776371113752e-216)3.051388185556876e-216(0.0 8.8828600833004e+195)+nan.0validexit20.118446#f
(-2.0625619181060858e-147)-1.0312809590530429e-147(-2.6282899993641297e+127 0.0)+nan.0validexit10.083025#f
(-1.0856758955283679e-274)-5.4283794776418393e-275(-4.993212877577308e+254 0.0)+nan.0validexit20.085036#f
(-3.6830286077989614e-252)-1.8415143038994807e-252(-1.4718894257156496e+232 0.0)+nan.0validexit20.152895#f
(-6.490208182992312e-274)-3.245104091496156e-274(-8.352599345939876e+253 0.0)+nan.0validexit20.178317#f
(8.293306159239457e+101)-6.859842647342997(-6.859842647342997 -6.859842647342997)+nan.0validexit00.110778#f
(5.760524306039774e-278)2.880262153019887e-278(0.0 9.41062058664299e+257)+nan.0validexit20.130816#f
(-2.503887083409037e-297)-1.2519435417045185e-297(-2.1650380715438763e+277 0.0)+nan.0validexit20.182704#f
(2.572846703071611e+254)-0.0015955951336124922(-0.0015955951336124989 -0.0015955951336124818)+nan.0validexit00.157596#f
(-5.2155477697541423e-79)-2.6077738848770712e-79(-1.0393943458566126e+59 0.0)+nan.0validexit10.081248#f
Sollya timings
Total time spent in Sollya 852.0ms
Bogosity

preprocess110.0ms (0.5%)

Algorithm
egg-herbie
Rules
199×fma-define
83×fma-neg
47×times-frac
47×div-sub
37×distribute-rgt-in
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
01760
14660
28556
319156
447056
581556
698156
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (sin.f64 x))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (sin.f64 x))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (sin.f64 (neg.f64 x)))
(neg.f64 (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (sin.f64 (neg.f64 x))))
Outputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (sin.f64 x))
(tan.f64 (/.f64 x #s(literal 2 binary64)))
(tan.f64 (*.f64 x #s(literal 1/2 binary64)))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (sin.f64 x))
(tan.f64 (/.f64 x #s(literal 2 binary64)))
(tan.f64 (*.f64 x #s(literal 1/2 binary64)))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (sin.f64 (neg.f64 x)))
(tan.f64 (/.f64 (neg.f64 x) #s(literal 2 binary64)))
(neg.f64 (tan.f64 (/.f64 x #s(literal 2 binary64))))
(tan.f64 (*.f64 x #s(literal -1/2 binary64)))
(neg.f64 (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (sin.f64 (neg.f64 x))))
(tan.f64 (/.f64 x #s(literal 2 binary64)))
(tan.f64 (*.f64 x #s(literal 1/2 binary64)))
Symmetry

(negabs x)

Compiler

Compiled 8 to 6 computations (25% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune15.0ms (0.1%)

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

Compiled 16 to 12 computations (25% saved)

simplify6.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01127
11827
22227
32427
42527
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (sin.f64 x))
Outputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (sin.f64 x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 8 to 6 computations (25% saved)

preprocess63.0ms (0.3%)

Remove

(negabs x)

Compiler

Compiled 74 to 56 computations (24.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...