2atan (example 3.5)

Time bar (total: 9.7s)

analyze4.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%8.1%91.9%0%0%0%0
0%0%8.1%91.9%0%0%0%1
50%4.1%4.1%91.9%0%0%0%2
75%6.1%2%91.9%0%0%0%3
87.5%7.1%1%91.9%0%0%0%4
93.8%7.6%0.5%91.9%0%0%0%5
96.9%7.9%0.3%91.9%0%0%0%6
98.4%8%0.1%91.9%0%0%0%7
99.2%8%0.1%91.9%0%0%0%8
99.6%8.1%0%91.9%0%0%0%9
99.8%8.1%0%91.9%0%0%0%10
99.9%8.1%0%91.9%0%0%0%11
100%8.1%0%91.9%0%0%0%12
Compiler

Compiled 15 to 10 computations (33.3% saved)

sample9.5s (98%)

Results
2.6s7366×1valid
737.0ms7345×1valid-sollya
271.0ms613×2valid
70.0ms611×2valid-sollya
49.0ms277×0valid
24.0ms275×0valid-sollya
7.0ms21×1exit-sollya
0.0ms2exit-sollya
0.0ms0exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(2459.7173907465)1.6521633272034805e-7(1.652163327202881e-7 1.6521633272050494e-7)+nan.0validexit00.074843#f
(2.1962934096178536e+45)2.0730953772381409e-91(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.07249799999999999#f
(3.258278946905473e+77)9.41940511041673e-156(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.076909#f
(3.932531536452427e+50)6.466295864846294e-102(+nan.0 +nan.0)+nan.0validexit15.0#f
(6.954046995832272e+98)2.067877259601291e-198(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.074723#f
(1.5211632277462298e+88)4.321637778531337e-177(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.08542799999999999#f
(1339.3753269639901)5.570203203873043e-7(5.570203203871795e-7 5.570203203873964e-7)+nan.0validexit00.087606#f
(7.287776074714454e+27)1.8828250167032078e-56(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.124465#f
(4.7381225619379874e+79)4.4543815932938495e-160(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.08105799999999999#f
(2.779845801688475e+64)1.2940724383669598e-129(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.07593#f
(61981653553490485000.0)2.6029970958578842e-40(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.160199#f
(4.46168519666931e+59)5.023450775780858e-120(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.139231#f
(8.584225554828065e+72)1.3570559676146393e-146(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.075496#f
(6.313057943378162e+99)2.5091143203546505e-200(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit20.16766999999999999#f
(2.8019267813739536e+84)1.2737565649005697e-169(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.12768600000000002#f
(4.0249486946049257e+43)6.172758729070354e-88(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.14097200000000001#f
(2.4908238751823865e+87)1.6118104242716614e-175(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.07669#f
(1.6156881473828717e+69)3.830759805869665e-139(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.075748#f
(7.192865115778208e+61)1.9328411692965593e-124(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.164797#f
(180643005789027230.0)3.064486397239936e-35(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.083682#f
(1.2938840782220222e+89)5.973230342667584e-179(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.158703#f
(6.030258881541374e+42)2.7499708230674124e-86(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.08661999999999999#f
(4.04608423707434e+31)6.108437848696496e-64(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.0857#f
(4.62686199309598e+55)4.671183286038019e-112(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.13072499999999998#f
(5.163032400501421e+82)3.7513734384998146e-166(-1.0842021724855044e-19 1.0842021724855044e-19)+nan.0validexit10.13889300000000002#f
Sollya timings
Total time spent in Sollya 839.0ms
Bogosity

preprocess124.0ms (1.3%)

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 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))
(-.f64 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))
(-.f64 (atan.f64 (+.f64 (neg.f64 N) #s(literal 1 binary64))) (atan.f64 (neg.f64 N)))
(neg.f64 (-.f64 (atan.f64 (+.f64 (neg.f64 N) #s(literal 1 binary64))) (atan.f64 (neg.f64 N))))
Outputs
(-.f64 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))
(-.f64 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))
(-.f64 (atan.f64 (+.f64 (neg.f64 N) #s(literal 1 binary64))) (atan.f64 (neg.f64 N)))
(-.f64 (atan.f64 (+.f64 #s(literal 1 binary64) (neg.f64 N))) (atan.f64 (neg.f64 N)))
(-.f64 (atan.f64 (-.f64 #s(literal 1 binary64) N)) (atan.f64 (neg.f64 N)))
(neg.f64 (-.f64 (atan.f64 (+.f64 (neg.f64 N) #s(literal 1 binary64))) (atan.f64 (neg.f64 N))))
(neg.f64 (-.f64 (atan.f64 (+.f64 #s(literal 1 binary64) (neg.f64 N))) (atan.f64 (neg.f64 N))))
(neg.f64 (-.f64 (atan.f64 (-.f64 #s(literal 1 binary64) N)) (atan.f64 (neg.f64 N))))
(-.f64 (atan.f64 (neg.f64 N)) (atan.f64 (-.f64 #s(literal 1 binary64) N)))
Compiler

Compiled 8 to 6 computations (25% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
10.5%
(-.f64 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))
Compiler

Compiled 16 to 12 computations (25% saved)

simplify11.0ms (0.1%)

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 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))
Outputs
(-.f64 (atan.f64 (+.f64 N #s(literal 1 binary64))) (atan.f64 N))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 8 to 6 computations (25% saved)

preprocess52.0ms (0.5%)

Compiler

Compiled 54 to 38 computations (29.6% saved)

end0.0ms (0%)

Profiling

Loading profile data...