VandenBroeck and Keller, Equation (24)

Time bar (total: 13.0s)

analyze169.0ms (1.3%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
0%0%99.9%0.1%0%0%0%1
0%0%99.9%0.1%0%0%0%2
0%0%99.9%0.1%0%0%0%3
25%25%74.9%0.1%0%0%0%4
25%25%74.9%0.1%0%0%0%5
37.5%37.5%62.4%0.1%0%0%0%6
37.5%37.5%62.4%0.1%0%0%0%7
43.8%43.7%56.2%0.1%0%0%0%8
43.8%43.7%56.2%0.1%0%0%0%9
46.9%46.8%53.1%0.1%0%0%0%10
46.9%46.8%53.1%0.1%0%0%0%11
48.4%48.4%51.5%0.1%0%0%0%12
Compiler

Compiled 15 to 11 computations (26.7% saved)

sample12.7s (97.5%)

Results
2.4s8256×0valid
973.0ms8238×0valid-sollya
4.0ms18×0exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-5.247351337928393e-290 -2.4282606907318444e+163)-inf.0(-inf.0 -inf.0)+nan.0validexit00.254272#f
(7.501778245136372e+214 -3.107117089638758e-106)1.1281349798048932(1.1281349798048932 1.1281349798048932)+nan.0validexit00.17360699999999998#f
(-3.521518188487381e+20 -2.2098228273887469e-60)-1.0030056699864394(-1.0030056699864394 -1.0030056699864394)+nan.0validexit00.20039600000000002#f
(-1002587724383.6624 -4.930210451709451e+286)8.2921836556468e+286(8.2921836556468e+286 8.2921836556468e+286)+nan.0validexit00.275688#f
(-2.2152067370948476e+164 -1.4868582453165114e+105)9.427974326381034e+105(9.427974326381034e+105 9.427974326381034e+105)+nan.0validexit00.156613#f
(8.722047183464892e+24 4.275878156476777e-65)3.756076498343931(3.756076498343931 3.756076498343931)+nan.0validexit00.259098#f
(2.0672561542386146e-230 -2.4467043096593595e+76)1.1835515906641469e+306(1.1835515906641469e+306 1.1835515906641469e+306)+nan.0validexit00.244666#f
(-3.7081025911121944e-239 -2.535596889254729e+242)-inf.0(-inf.0 -inf.0)+nan.0validexit00.20851499999999998#f
(-4.097740638743653e+162 3.268614630469811e-85)1.8528049178608503(1.8528049178608503 1.8528049178608503)+nan.0validexit00.31560099999999996#f
(7.569022702680529e+214 1.4843596984245922e+114)4.99609888658209e+112(4.99609888658209e+112 4.99609888658209e+112)+nan.0validexit00.285645#f
(1.578540127604132e+149 -2.4021492592481474e+246)-9.273479359543595e+245(-9.273479359543595e+245 -9.273479359543595e+245)+nan.0validexit00.26303699999999997#f
(-3.506672333349939e-17 -1.0589067446408431e+198)-3.0196911601069524e+214(-3.0196911601069524e+214 -3.0196911601069524e+214)+nan.0validexit00.207069#f
(2.5396095355533392e-269 -1.5457761799895743e+64)+inf.0(+inf.0 +inf.0)+nan.0validexit00.151595#f
(-4.610770508060124e+100 -6.898064649090368e-230)-1.0652416170626036(-1.0652416170626036 -1.0652416170626036)+nan.0validexit00.27160900000000004#f
(1.9020173078268283e+288 -3.044178204704498e-237)-1.010422926266425(-1.010422926266425 -1.010422926266425)+nan.0validexit00.337818#f
(-2.3070607517175373e+22 2.9078402182741228e-213)-1.080613649373176(-1.080613649373176 -1.080613649373176)+nan.0validexit00.195785#f
(8.179890250132308e-304 8.792569003013448e+84)-inf.0(-inf.0 -inf.0)+nan.0validexit00.133866#f
(-1.2031592236910127e+82 -2.5569677981992688e+138)-1.0370379029107992e+138(-1.0370379029107992e+138 -1.0370379029107992e+138)+nan.0validexit00.236286#f
Sollya timings
Total time spent in Sollya 977.0ms
Bogosity

preprocess110.0ms (0.8%)

Algorithm
egg-herbie
Rules
233×fma-define
186×fma-neg
54×distribute-lft-neg-in
41×sub-neg
37×cancel-sign-sub-inv
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
037342
194252
2257252
3520252
4812252
51028252
61154252
71284252
81294252
Stop Event
saturated
Calls
Call 1
Inputs
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 B))))) (/.f64 #s(literal 1 binary64) (sin.f64 (neg.f64 B))))
(+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(neg.f64 (+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 B))))) (/.f64 #s(literal 1 binary64) (sin.f64 (neg.f64 B)))))
(neg.f64 (+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B))))
(+.f64 (neg.f64 (*.f64 B (/.f64 #s(literal 1 binary64) (tan.f64 x)))) (/.f64 #s(literal 1 binary64) (sin.f64 x)))
Outputs
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(+.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 (*.f64 (neg.f64 x) #s(literal 1 binary64)) (tan.f64 B)))
(-.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(+.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 (*.f64 (neg.f64 x) #s(literal 1 binary64)) (tan.f64 B)))
(-.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 B))))) (/.f64 #s(literal 1 binary64) (sin.f64 (neg.f64 B))))
(+.f64 (*.f64 x (neg.f64 (/.f64 #s(literal 1 binary64) (neg.f64 (tan.f64 B))))) (/.f64 #s(literal 1 binary64) (neg.f64 (sin.f64 B))))
(+.f64 (/.f64 #s(literal -1 binary64) (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(+.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (*.f64 (neg.f64 x) (neg.f64 (/.f64 #s(literal 1 binary64) (tan.f64 B)))))
(+.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 x (tan.f64 B)))
(neg.f64 (+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 B))))) (/.f64 #s(literal 1 binary64) (sin.f64 (neg.f64 B)))))
(+.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 (*.f64 (neg.f64 x) #s(literal 1 binary64)) (tan.f64 B)))
(-.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (/.f64 x (tan.f64 B)))
(neg.f64 (+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B))))
(neg.f64 (+.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (*.f64 (neg.f64 x) (neg.f64 (/.f64 #s(literal 1 binary64) (tan.f64 B))))))
(-.f64 (/.f64 #s(literal -1 binary64) (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 B (/.f64 #s(literal 1 binary64) (tan.f64 x)))) (/.f64 #s(literal 1 binary64) (sin.f64 x)))
(+.f64 (*.f64 B (neg.f64 (/.f64 #s(literal 1 binary64) (tan.f64 x)))) (/.f64 #s(literal 1 binary64) (sin.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) (sin.f64 x)) (/.f64 B (tan.f64 x)))
Symmetry

(negabs B)

Compiler

Compiled 14 to 10 computations (28.6% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
99.7%
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
Compiler

Compiled 28 to 20 computations (28.6% saved)

simplify5.0ms (0%)

Algorithm
egg-herbie
Rules
14×neg-mul-1
12×unsub-neg
distribute-lft-neg-in
distribute-rgt-neg-in
*-commutative
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
01646
13042
24442
35342
46142
58142
610942
Stop Event
saturated
Calls
Call 1
Inputs
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
Outputs
(+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(+.f64 (*.f64 (neg.f64 x) (/.f64 #s(literal 1 binary64) (tan.f64 B))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))
(-.f64 (/.f64 #s(literal 1 binary64) (sin.f64 B)) (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B))))
(+.f64 (*.f64 x (/.f64 #s(literal -1 binary64) (tan.f64 B))) (/.f64 #s(literal 1 binary64) (sin.f64 B)))

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 13 to 10 computations (23.1% saved)

preprocess34.0ms (0.3%)

Remove

(negabs B)

Compiler

Compiled 106 to 80 computations (24.5% saved)

end0.0ms (0%)

Profiling

Loading profile data...