tanhf (example 3.4)

Time bar (total: 16.6s)

analyze128.0ms (0.8%)

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)

sample16.3s (98.3%)

Results
1.3s4210×0valid
395.0ms4197×0valid-sollya
633.0ms2056×1valid
211.0ms2048×1valid-sollya
1.7s1985×2valid
243.0ms1912×2valid-sollya
10.0ms73×2exit-sollya
8.0ms13×0exit-sollya
1.0ms1exit-sollya
4.0ms3valid
1.0ms3valid-sollya
0.0ms3exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-5.426120432854159e-258)-2.7130602164270794e-258(-9.990583381828941e+237 0.0)+nan.0validexit20.084757#f
(-3.389505189267775e-262)-1.6947525946338876e-262(-1.599351692864234e+242 0.0)+nan.0validexit20.145947#f
(-9.504518210605802e-298)-4.752259105302901e-298(-5.703614578147035e+277 0.0)+nan.0validexit20.086944#f
(-4.873477398036046e-300)-2.436738699018023e-300(-1.1123496468070471e+280 0.0)+nan.0validexit20.131404#f
(-1.2748140822824026e+308)7.53493261752425(+nan.0 +nan.0)+nan.0validexit05.0#f
(4.104129901857619e-288)2.0520649509288096e-288(0.0 1.3208672707883476e+268)+nan.0validexit20.167871#f
(-1.204327381318847e-32)-6.021636906594235e-33(-4501276767859.439 0.0)+nan.0validexit10.138093#f
(3.7117682472346106e-305)1.8558841236173053e-305(0.0 1.46049281672323e+285)+nan.0validexit20.085786#f
(-1.0439408252099679e-307)-5.219704126049839e-308(-5.1928334743850966e+287 0.0)+nan.0validexit20.184863#f
(-3.319103907269302e-270)-1.659551953634651e-270(-1.6332754303216447e+250 0.0)+nan.0validexit20.159131#f
(-6.981051149586941e-285)-3.4905255747934706e-285(-7.76532179218924e+264 0.0)+nan.0validexit20.086827#f
(-2.359913561045099e-232)-1.1799567805225495e-232(-2.297122636994722e+212 0.0)+nan.0validexit20.166683#f
(3.9205366749957994e-184)1.9602683374978997e-184(0.0 1.3827216301791975e+164)+nan.0validexit20.154034#f
(4.3605365707288576e-260)2.1802682853644288e-260(0.0 1.2431981189694294e+240)+nan.0validexit20.15569#f
(3.1708474121133505e-255)1.5854237060566752e-255(0.0 1.7096410384549068e+235)+nan.0validexit20.157737#f
(1.8633380296106468e-270)9.316690148053234e-271(0.0 2.9093008226533475e+250)+nan.0validexit20.13641599999999998#f
(5.033880948819764e-252)2.516940474409882e-252(0.0 1.076904860791061e+232)+nan.0validexit20.16939099999999999#f
(1.4016326218445977e+282)-0.13024612263938878(-0.13024612263938878 -0.13024612263938878)+nan.0validexit00.25448400000000004#f
(3.3293419579926583e+182)1.1505020062238351(1.1505020062238351 1.1505020062238351)+nan.0validexit00.253137#f
(-2.694342051229826e-287)-1.347171025614913e-287(-2.0119980163443296e+267 0.0)+nan.0validexit20.133374#f
(8.889598832655441e-281)4.4447994163277203e-281(0.0 6.098150169064709e+260)+nan.0validexit20.12710600000000002#f
(-3.7647283282247194e-298)-1.8823641641123597e-298(-1.4399474250998168e+278 0.0)+nan.0validexit20.121849#f
(-2.215656584447601e-263)-1.1078282922238005e-263(-2.4466837056244744e+243 0.0)+nan.0validexit20.165718#f
(-3.1403269377212456e+56)6.881169145697281(6.881169145697281 6.881169145697281)+nan.0validexit00.18143700000000001#f
(-4.3957132667332386e+52)6.304711585717362(6.304711585717362 6.304711585717362)+nan.0validexit00.210616#f
(-1.8870578621743765e-172)-9.435289310871883e-173(-2.872731658679041e+152 0.0)+nan.0validexit20.079058#f
(2.587811737121581e-103)1.2939058685607905e-103(0.0 2.094824281327862e+83)+nan.0validexit10.120652#f
(5.5764822837877995e-282)2.7882411418938998e-282(0.0 9.721201622369946e+261)+nan.0validexit20.084946#f
(4.720856535539711e-302)2.3604282677698557e-302(0.0 1.1483108672370968e+282)+nan.0validexit20.079334#f
(-9.290545678032053e-243)-4.6452728390160266e-243(-5.834975738019098e+222 0.0)+nan.0validexit20.15709299999999998#f
(1.231750063468007e+93)-10.24773624756631(-10.24773624756631 -10.24773624756631)+nan.0validexit00.169784#f
(2.3724836054676104e-303)1.1862418027338052e-303(0.0 2.2849518748767304e+283)+nan.0validexit20.109972#f
(-2.469322801875028e-150)-1.234661400937514e-150(-2.195343135499009e+130 0.0)+nan.0validexit10.078914#f
(5.864256306915066e-163)2.932128153457533e-163(0.0 9.244157449317361e+142)+nan.0validexit20.155282#f
(4.342776370220122e+47)-0.9130627478808566(-0.9130627478808566 -0.9130627478808566)+nan.0validexit00.19573600000000002#f
(-8.929950069093874e-250)-4.464975034546937e-250(-6.070594819101373e+229 0.0)+nan.0validexit20.18478#f
(1.8368709752532966e-298)9.184354876266483e-299(0.0 2.9512202737483986e+278)+nan.0validexit20.129873#f
(-1.180624859698123e-285)-5.903124298490615e-286(-4.591645532361257e+265 0.0)+nan.0validexit20.16761700000000002#f
(2.6329334235302566e+246)0.5353341009291864(0.5353341009291864 0.5353341009291864)+nan.0validexit00.224713#f
(4.03697987496617e-236)2.018489937483085e-236(0.0 1.3428382182541722e+216)+nan.0validexit20.11995#f
(-1.077527499648577e-280)-5.387637498242885e-281(-5.030972169337229e+260 0.0)+nan.0validexit20.130332#f
(1.2432277984363504e-290)6.216138992181752e-291(0.0 4.360432472026213e+270)+nan.0validexit20.162194#f
(1.6929402494392268e-260)8.464701247196134e-261(0.0 3.202127697196159e+240)+nan.0validexit20.1614#f
(1.5285631138738375e-258)7.642815569369187e-259(0.0 3.546474995519848e+238)+nan.0validexit20.15712199999999998#f
(-2.9524673930332384e-219)-1.4762336965166192e-219(-1.8360950827836943e+199 0.0)+nan.0validexit20.126195#f
(3.036485940971574e-243)1.518242970485787e-243(0.0 1.7852909474341185e+223)+nan.0validexit20.137785#f
(4.677767198736858e+298)-9.77790031570687(-9.77790031570687 -9.77790031570687)+nan.0validexit00.15822899999999998#f
(-3.754935805906134e-297)-1.877467902953067e-297(-1.4437026736651053e+277 0.0)+nan.0validexit20.08655299999999999#f
(-3.841423208022202e-197)-1.920711604011101e-197(-1.411198550346289e+177 0.0)+nan.0validexit20.12100999999999999#f
(3.6563378429231733e-258)1.8281689214615867e-258(0.0 1.482634016689641e+238)+nan.0validexit20.09080200000000001#f
(-4.920146457548002e-289)-2.460073228774001e-289(-1.1017986779867383e+269 0.0)+nan.0validexit20.15306799999999998#f
(-3.5649116411939876e-248)-1.7824558205969938e-248(-1.520657847388295e+228 0.0)+nan.0validexit20.171653#f
(5.714052362161074e-295)2.857026181080537e-295(0.0 9.487156432667476e+274)+nan.0validexit20.157935#f
(2.896651254604008e-308)1.448325627302004e-308(0.0 1.871475157325631e+288)+nan.0validexit30.138043#f
(-3.261625460460326e-36)-1.630812730230163e-36(-16620580529998786.0 0.0)+nan.0validexit10.079876#f
(-4.665924449306301e-298)-2.3329622246531503e-298(-1.1618299698859211e+278 0.0)+nan.0validexit20.158179#f
(-3.4462882111347227e-289)-1.7231441055673613e-289(-1.5729998567480818e+269 0.0)+nan.0validexit20.172044#f
(-3.9642662701610856e-238)-1.9821331350805428e-238(-1.3674689067258953e+218 0.0)+nan.0validexit20.155662#f
(-8.036225154664198e-295)-4.018112577332099e-295(-6.7457179933307196e+274 0.0)+nan.0validexit20.103035#f
(4.794926527080671e-103)2.3974632635403356e-103(0.0 1.1305722479397477e+83)+nan.0validexit10.081659#f
(-6.068133738070528e-226)-3.034066869035264e-226(-8.93357183019376e+205 0.0)+nan.0validexit20.076498#f
(-6.971382835810294e-291)-3.485691417905147e-291(-7.776091186071594e+270 0.0)+nan.0validexit20.084261#f
(-2.5090141597146155e+182)0.14379628549274712(0.14379628549274712 0.14379628549274712)+nan.0validexit00.132356#f
(9.330329763911682e+260)-1.1627752334040207(-1.1627752334040207 -1.1627752334040207)+nan.0validexit00.358163#f
(3.913885981875027e-249)1.9569429909375136e-249(0.0 1.3850712278109022e+229)+nan.0validexit20.083672#f
(-1.7424558251251504e-24)-8.712279125625752e-25(-31111.32451256354 0.0)+nan.0validexit10.152888#f
(7.746249463159806e+153)-0.27603269119104623(-0.27603269119104623 -0.27603269119104623)+nan.0validexit00.249347#f
(2.4396041340398098e-203)1.2198020670199049e-203(0.0 2.222086274895229e+183)+nan.0validexit20.154163#f
(7.880981738562296e-217)3.940490869281148e-217(0.0 6.8785984313376434e+196)+nan.0validexit20.12909299999999999#f
(-1.5422439993077144e-192)-7.711219996538572e-193(-3.515015046167089e+172 0.0)+nan.0validexit20.108691#f
(5.8795142406571775e-217)2.9397571203285887e-217(0.0 9.220167926358477e+196)+nan.0validexit20.085441#f
(4.241280444119887e-103)2.1206402220599435e-103(0.0 1.2781543059580542e+83)+nan.0validexit10.082117#f
(-6.331174226615255e-106)-3.1655871133076275e-106(-8.5624098601464e+85 0.0)+nan.0validexit10.075256#f
(1.9446800566031747e-283)9.723400283015873e-284(0.0 2.787610663265889e+263)+nan.0validexit20.202674#f
(-4.847217958560582e-265)-2.423608979280291e-265(-1.1183757175295934e+245 0.0)+nan.0validexit20.15313#f
(4.938522651505196e-298)2.469261325752598e-298(0.0 1.0976988959998533e+278)+nan.0validexit20.157963#f
(-2.719349578998741e-236)-1.3596747894993704e-236(-1.9934953947419765e+216 0.0)+nan.0validexit20.084134#f
(2.4565990823704905e-268)1.2282995411852453e-268(0.0 2.2067137048657236e+248)+nan.0validexit20.1339#f
(2.1088026050764525e+250)-0.22512188743191908(-0.22512188743191908 -0.22512188743191908)+nan.0validexit00.159042#f
(4.5286172586082033e-209)2.2643086293041017e-209(0.0 1.1970565302517044e+189)+nan.0validexit20.082209#f
(-1.8682421675880518e-208)-9.341210837940259e-209(-2.901663904431718e+188 0.0)+nan.0validexit20.122655#f
(1.1783870972584563e-186)5.891935486292281e-187(0.0 4.600365088042481e+166)+nan.0validexit20.11412599999999999#f
(4.3906173430112986e-187)2.1953086715056493e-187(0.0 1.2346807837982824e+167)+nan.0validexit20.132747#f
(-1.3720895709665057e-305)-6.860447854832528e-306(-3.9509161625716163e+285 0.0)+nan.0validexit20.16952499999999998#f
(6.263269443285693e-251)3.1316347216428464e-251(0.0 8.655241342425268e+230)+nan.0validexit20.168259#f
(-2.0740938248986007e-286)-1.0370469124493004e-286(-2.6136767765038535e+266 0.0)+nan.0validexit20.14168899999999998#f
(-7.441199538814677e-278)-3.720599769407339e-278(-7.285130353178307e+257 0.0)+nan.0validexit20.15936499999999998#f
(-9.382643968403708e-217)-4.691321984201854e-217(-5.777700700019008e+196 0.0)+nan.0validexit20.123903#f
(1.1060490218187973e-302)5.5302451090939864e-303(0.0 4.901239235773801e+282)+nan.0validexit20.138113#f
(-1.3239964284135906e-280)-6.619982142067953e-281(-4.094430125406731e+260 0.0)+nan.0validexit20.184593#f
(5.252062262762537e-246)2.6260311313812687e-246(0.0 1.0321680496560068e+226)+nan.0validexit20.12318100000000001#f
(-1.208189217487029e-267)-6.040946087435145e-268(-4.486888960739895e+247 0.0)+nan.0validexit20.129839#f
(-7.430472118351019e-284)-3.715236059175509e-284(-7.295647942799308e+263 0.0)+nan.0validexit20.13348000000000002#f
(-5.533471455909581e-258)-2.7667357279547903e-258(-9.796763036769705e+237 0.0)+nan.0validexit20.127644#f
(-1.4729188182726204e-301)-7.364594091363102e-302(-3.680454615132872e+281 0.0)+nan.0validexit20.17041800000000001#f
Sollya timings
Total time spent in Sollya 868.0ms
Bogosity

preprocess97.0ms (0.6%)

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)

prune1.0ms (0%)

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

Compiled 16 to 12 computations (25% saved)

simplify2.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))

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 8 to 6 computations (25% saved)

preprocess59.0ms (0.4%)

Remove

(negabs x)

Compiler

Compiled 74 to 56 computations (24.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...