2sqrt (example 3.1)

Time bar (total: 20.2s)

analyze9.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%25%75%0%0%0%0
0%0%25%75%0%0%0%1
50%12.5%12.5%75%0%0%0%2
75%18.7%6.2%75%0%0%0%3
87.5%21.9%3.1%75%0%0%0%4
93.8%23.4%1.6%75%0%0%0%5
96.9%24.2%0.8%75%0%0%0%6
98.4%24.6%0.4%75%0%0%0%7
99.2%24.8%0.2%75%0%0%0%8
99.6%24.9%0.1%75%0%0%0%9
99.8%24.9%0%75%0%0%0%10
99.9%25%0%75%0%0%0%11
100%25%0%75%0%0%0%12
Compiler

Compiled 15 to 10 computations (33.3% saved)

sample19.6s (97.3%)

Results
2.4s4700×1valid
447.0ms4692×1valid-sollya
2.7s3361×2valid
482.0ms3349×2valid-sollya
31.0ms195×0valid
14.0ms195×0valid-sollya
2.0ms12×2exit-sollya
6.0ms1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(1.4724724207146529e+262)4.1204668046089893e-132(-9.619630419041621e+111 9.619630419041621e+111)+nan.0validexit20.175212#f
(5.333368647031143e+99)6.846509302393295e-51(-5.070602400912918e+30 1.0141204801825835e+31)+nan.0validexit10.061725999999999996#f
(5.498449321828432e+202)2.132307777757959e-102(-1.517710072051351e+82 1.517710072051351e+82)+nan.0validexit20.16111399999999998#f
(1.790252572463989e+290)3.736911830313704e-146(-1.3538426240824291e+126 1.3538426240824291e+126)+nan.0validexit20.19159#f
(3.983569873896502e+181)7.921980785007527e-92(-4.417117661945961e+71 8.834235323891922e+71)+nan.0validexit10.091437#f
(9.133167376198919e+212)1.654471521367608e-107(-1.9892929456391466e+87 3.978585891278293e+87)+nan.0validexit20.17595999999999998#f
(5.710867508552437e+193)6.616357479907256e-98(-4.631683569492648e+77 4.631683569492648e+77)+nan.0validexit20.173506#f
(9.078890256596826e+89)5.2475141833019356e-46(-7.737125245533627e+25 7.737125245533627e+25)+nan.0validexit10.084553#f
(1.6441693147721782e+177)1.2330955628417446e-89(-3.450873173395282e+69 3.450873173395282e+69)+nan.0validexit10.17493#f
(3.1601560592797864e+194)2.812650300612373e-98(-1.8526734277970591e+78 3.7053468555941183e+78)+nan.0validexit20.184067#f
(1.57215682486624e+216)3.9876962660905247e-109(-1.2731474852090538e+89 1.2731474852090538e+89)+nan.0validexit20.110747#f
(2.7413129784333768e+216)3.019887004676382e-109(-1.2731474852090538e+89 2.5462949704181076e+89)+nan.0validexit20.16231500000000001#f
(3.3339372336454395e+28)2.7383647438613236e-15(+nan.0 +nan.0)+nan.0validexit15.0#f
(6.526202111565752e+78)1.957220449034946e-40(-1.4757395258967641e+20 1.4757395258967641e+20)+nan.0validexit10.072172#f
(2.4833940771811926e+251)1.0033378220834957e-126(-3.6695977855841144e+106 7.339195571168229e+106)+nan.0validexit20.14422600000000002#f
(7.122022212921198e+208)1.8735631779189525e-105(-1.5541351137805833e+85 1.5541351137805833e+85)+nan.0validexit20.104113#f
(1.7597071876587084e+86)3.769205362834399e-44(-1.2089258196146292e+24 1.2089258196146292e+24)+nan.0validexit10.07850599999999999#f
(4.422116416207515e+260)2.377688287991093e-131(-1.2024538023802026e+111 2.4049076047604052e+111)+nan.0validexit20.16185#f
(26999549777.683945)3.0429284675933666e-6(3.042928454988214e-6 3.0429284834099235e-6)+nan.0validexit10.079#f
(5.2360867571682175e+228)2.185076203753171e-115(-1.3349918974505688e+95 2.6699837949011376e+95)+nan.0validexit20.09406199999999999#f
Sollya timings
Total time spent in Sollya 951.0ms
Bogosity

preprocess287.0ms (1.4%)

Algorithm
egg-herbie
Rules
84×fma-define
66×fma-neg
32×sub-neg
22×unsub-neg
20×associate--r+
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
017128
133120
261116
3107116
4173116
5266116
6344116
7402116
8453116
9488116
10514116
11516116
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x))
(-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x))
(-.f64 (sqrt.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64))) (sqrt.f64 (neg.f64 x)))
(neg.f64 (-.f64 (sqrt.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64))) (sqrt.f64 (neg.f64 x))))
Outputs
(-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x))
(-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x))
(-.f64 (sqrt.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64))) (sqrt.f64 (neg.f64 x)))
(-.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x))) (sqrt.f64 (neg.f64 x)))
(-.f64 (sqrt.f64 (-.f64 #s(literal 1 binary64) x)) (sqrt.f64 (neg.f64 x)))
(neg.f64 (-.f64 (sqrt.f64 (+.f64 (neg.f64 x) #s(literal 1 binary64))) (sqrt.f64 (neg.f64 x))))
(neg.f64 (-.f64 (sqrt.f64 (+.f64 #s(literal 1 binary64) (neg.f64 x))) (sqrt.f64 (neg.f64 x))))
(neg.f64 (-.f64 (sqrt.f64 (-.f64 #s(literal 1 binary64) x)) (sqrt.f64 (neg.f64 x))))
(-.f64 (sqrt.f64 (neg.f64 x)) (sqrt.f64 (-.f64 #s(literal 1 binary64) x)))
Compiler

Compiled 8 to 6 computations (25% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune45.0ms (0.2%)

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

Compiled 16 to 12 computations (25% saved)

simplify4.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01127
11927
22327
32527
42627
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x))
Outputs
(-.f64 (sqrt.f64 (+.f64 x #s(literal 1 binary64))) (sqrt.f64 x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 8 to 6 computations (25% saved)

preprocess191.0ms (0.9%)

Compiler

Compiled 52 to 38 computations (26.9% saved)

end0.0ms (0%)

Profiling

Loading profile data...