cos2 (problem 3.4.1)

Time bar (total: 14.9s)

analyze2.0ms (0%)

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

Compiled 10 to 7 computations (30% saved)

sample14.7s (98.4%)

Results
1.1s4222×0valid
423.0ms4196×0valid-sollya
750.0ms2092×1valid
233.0ms2075×1valid-sollya
1.8s1942×2valid
276.0ms1924×2valid-sollya
19.0ms26×0exit-sollya
3.0ms18×2exit-sollya
7.0ms17×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-2.4027047733177682e-166)0.5(0.0 +inf.0)+nan.0validexit20.156561#f
(-2.5746030018570557e-252)0.5(0.0 +inf.0)+nan.0validexit20.172099#f
(1.5323299437365497e+258)0.0(0.0 0.0)+nan.0validexit00.267675#f
(1.0089993383465799e-255)0.5(0.0 +inf.0)+nan.0validexit20.140114#f
(-2.1400265770599401e-103)0.5(0.0 1.1837008070228372e+186)+nan.0validexit10.139864#f
(-2.4314479310731036e-139)0.5(0.0 9.169598712631584e+257)+nan.0validexit10.137494#f
(1.4198757341669209e-142)0.5(0.0 2.688930660968908e+264)+nan.0validexit10.128273#f
(4.8496189169261e+180)0.0(0.0 0.0)+nan.0validexit00.13047#f
(-4.877338171476296e-236)0.5(0.0 +inf.0)+nan.0validexit20.168194#f
(-2.3363709996246345e+154)2.915363205810826e-309(2.915363205810826e-309 2.915363205810826e-309)+nan.0validexit00.207848#f
(-1.4151005248343277e+289)0.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(2.3461315818317617e-237)0.5(0.0 +inf.0)+nan.0validexit20.134143#f
(-8.937674729766724e+189)0.0(0.0 0.0)+nan.0validexit00.209781#f
(3.2442707922404366e-164)0.5(0.0 5.150460776850381e+307)+nan.0validexit20.16145800000000002#f
(-1.2720520273893417e-198)0.5(0.0 +inf.0)+nan.0validexit20.155176#f
(7.105477812653783e-267)0.5(0.0 +inf.0)+nan.0validexit20.21074700000000002#f
(2.576840317161853e+169)0.0(0.0 0.0)+nan.0validexit00.173473#f
(-8.970628469250788e+221)0.0(0.0 0.0)+nan.0validexit00.221158#f
(3.598066777428608e+275)0.0(0.0 0.0)+nan.0validexit00.14769#f
(-2.055744363258704e+281)0.0(0.0 0.0)+nan.0validexit00.223107#f
(2.7347142006706667e-112)0.5(0.0 7.248637572959077e+203)+nan.0validexit10.132433#f
(-6.522534932647992e+141)3.988848344791627e-284(3.988848344791627e-284 3.988848344791627e-284)+nan.0validexit00.204928#f
(-7.579757173330355e-55)0.5(0.0 9.435603701664635e+88)+nan.0validexit10.12807500000000002#f
(2.6234443294872722)0.2715217686225347(0.2715217686225347 0.2715217686225347)+nan.0validexit00.13828700000000002#f
(-2.6996443964006343e-305)0.5(0.0 +inf.0)+nan.0validexit20.09464800000000001#f
(-1.4916036302925007e-223)0.5(0.0 +inf.0)+nan.0validexit20.281926#f
(-8.271408526041154e+161)0.0(0.0 0.0)+nan.0validexit00.232514#f
(5.507217967260169e+250)0.0(0.0 0.0)+nan.0validexit00.232533#f
(-5.798405724923611e-292)0.5(0.0 +inf.0)+nan.0validexit20.14159400000000003#f
(-2.260655152653309e+240)0.0(0.0 0.0)+nan.0validexit00.229815#f
(2.202028753649025e-70)0.5(0.0 1.1179807000675992e+120)+nan.0validexit10.080129#f
(-4.539729713180697e-272)0.5(0.0 +inf.0)+nan.0validexit20.084153#f
(5.199960610115882e-203)0.5(0.0 +inf.0)+nan.0validexit20.082621#f
(1.9535253655774852e-104)0.5(0.0 1.4205030420177942e+188)+nan.0validexit10.08383499999999999#f
(2.7695066323576825e+222)0.0(0.0 0.0)+nan.0validexit00.13179000000000002#f
(-8.451106241269274e-300)0.5(0.0 +inf.0)+nan.0validexit20.181866#f
(8.255030489792492e+200)0.0(+nan.0 +nan.0)+nan.0validexit05.0#f
(-3.720685731019113e+149)1.2139929016108134e-299(+nan.0 +nan.0)+nan.0validexit05.0#f
(1.1650246803824978e+61)1.448722764888992e-122(1.448722764888992e-122 1.448722764888992e-122)+nan.0validexit00.109039#f
(-1.8292509990624755e+279)0.0(0.0 0.0)+nan.0validexit00.311363#f
(-2.2256566371417844e-73)0.5(0.0 1.0943694189144305e+126)+nan.0validexit10.152684#f
(5.693384775765079e-165)0.5(0.0 +inf.0)+nan.0validexit20.155356#f
(1.8475720947200462e-104)0.5(0.0 1.5880986962453887e+188)+nan.0validexit10.150531#f
(4.0651156181466185e-5)0.49999999993114513(+nan.0 +nan.0)+nan.0validexit15.0#f
(-5.1630815008630444e-148)0.5(0.0 2.0335849370038062e+275)+nan.0validexit10.156878#f
(-2.316329680465842e-280)0.5(0.0 +inf.0)+nan.0validexit20.186825#f
(4.1730696981012666e+152)3.5195103048712323e-306(3.5195103048712323e-306 3.5195103048712323e-306)+nan.0validexit00.188478#f
(-8.429446983228997e+199)0.0(0.0 0.0)+nan.0validexit00.23120700000000002#f
(1.0867902687858707e+236)0.0(0.0 0.0)+nan.0validexit00.141837#f
(1.029963139816664e+209)0.0(0.0 0.0)+nan.0validexit00.134045#f
(-9.52608059471856e-117)0.5(0.0 5.9738150750264055e+212)+nan.0validexit10.083898#f
(2.2130541017640473e-231)0.5(0.0 +inf.0)+nan.0validexit20.13239499999999998#f
(-2.248091587898497e+72)3.237537274858822e-145(3.237537274858822e-145 3.237537274858822e-145)+nan.0validexit00.20387899999999998#f
(-8.57191661576707e-112)0.5(0.0 7.3777579373539855e+202)+nan.0validexit10.08484#f
(-1.2029627095535825e-74)0.5(0.0 3.746070510696205e+128)+nan.0validexit10.129995#f
(1.6955969632340096e-262)0.5(0.0 +inf.0)+nan.0validexit20.166142#f
(-2.3739189765945102e+131)3.69817235662001e-266(3.69817235662001e-266 3.69817235662001e-266)+nan.0validexit00.18436#f
(-2.3041480218276493e-55)0.5(0.0 1.021079428876705e+90)+nan.0validexit10.134473#f
(2.625328973642084e-54)0.5(0.0 7.865255125556759e+87)+nan.0validexit10.121772#f
(-9.659169428245687e+100)1.6390638049822518e-202(1.6390638049822518e-202 1.6390638049822518e-202)+nan.0validexit00.22664800000000002#f
(1.1955886605792827e-74)0.5(0.0 3.792422397235022e+128)+nan.0validexit10.137057#f
Sollya timings
Total time spent in Sollya 962.0ms
Bogosity

preprocess177.0ms (1.2%)

Algorithm
egg-herbie
Rules
387×fma-define
161×times-frac
137×fma-neg
100×div-sub
90×distribute-rgt-in
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
017132
146132
2118128
3313128
4812128
51454128
61846128
71878128
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (*.f64 (neg.f64 x) (neg.f64 x)))
(neg.f64 (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (*.f64 (neg.f64 x) (neg.f64 x))))
Outputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (*.f64 (neg.f64 x) (neg.f64 x)))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
(neg.f64 (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 (neg.f64 x))) (*.f64 (neg.f64 x) (neg.f64 x))))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (neg.f64 (*.f64 x x)))
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x (neg.f64 x)))
(/.f64 (+.f64 (cos.f64 x) #s(literal -1 binary64)) (*.f64 x x))
Symmetry

(abs x)

Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

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

Compiled 18 to 12 computations (33.3% saved)

simplify2.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01132
11832
22232
32432
42532
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
Outputs
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 6 computations (33.3% saved)

preprocess59.0ms (0.4%)

Remove

(abs x)

Compiler

Compiled 72 to 48 computations (33.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...