2tan (problem 3.3.2)

Time bar (total: 35.7s)

analyze114.0ms (0.3%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%50.6%49.4%0%0%0%0
0%0%50.6%49.4%0%0%0%1
0%0%50.6%49.4%0%0%0%2
0%0%25.3%74.7%0%0%0%3
0%0%25.3%74.7%0%0%0%4
0%0%19%81%0%0%0%5
0%0%15.8%84.2%0%0%0%6
0%0%11.1%88.9%0%0%0%7
0%0%8.7%91.3%0%0%0%8
0%0%5.9%94.1%0%0%0%9
0%0%4.5%95.5%0%0%0%10
0%0%3.1%96.9%0%0%0%11
0%0%2.7%97.3%0%0%0%12
Compiler

Compiled 28 to 18 computations (35.7% saved)

sample35.3s (99%)

Results
8.7s26375×0precondition
2.7s4459×1valid
427.0ms4446×1valid-sollya
1.3s3797×0valid
351.0ms3783×0valid-sollya
2.0ms14×0exit-sollya
2.0ms13×1exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(-1.5701823440194018e-10 7.960233915622422e-17)7.960233915622422e-17(7.960233915619999e-17 7.960233915623785e-17)+nan.0validexit00.203612#f
(-2.0093185668504338e-190 1.25943123426609e-196)1.25943123426609e-196(1.2594312342658999e-196 1.2594312342662649e-196)+nan.0validexit00.175372#f
(-1.6791575498314274e-47 3.297563532813859e-52)3.297563532813859e-52(3.297563532813838e-52 3.2975635328138736e-52)+nan.0validexit00.22510100000000002#f
(1.4648966292188172e-66 1.1535869689973482e-79)1.1535869689973482e-79(1.1535856722513484e-79 1.1535895329195405e-79)+nan.0validexit10.206006#f
(-1.369373017494062e-54 1.815931531632711e-69)1.815931531632711e-69(1.8156636553047558e-69 1.8160881402615758e-69)+nan.0validexit10.104771#f
(-2.5302872575505972e-259 3.1162815867706165e-262)3.1162815867706165e-262(3.1162815867706165e-262 3.1162815867706165e-262)+nan.0validexit00.191482#f
(-3.1567942956000432e-177 1.0421412688277548e-190)1.0421412688277548e-190(1.0421389918501565e-190 1.0421454131666087e-190)+nan.0validexit10.159928#f
(8.973665589228394e-202 7.956556824605607e-209)7.956556824605607e-209(7.95655682459096e-209 7.956556824617517e-209)+nan.0validexit00.11498#f
(-6.774243047886213e-21 3.990760136060282e-24)3.990760136060282e-24(3.990760136060282e-24 3.990760136060283e-24)+nan.0validexit00.10195599999999999#f
(-1.6062074842979864e-192 6.062592633594946e-208)6.062592633594946e-208(6.061630459132117e-208 6.06448209648156e-208)+nan.0validexit10.111055#f
(1.4475554775338946e-229 1.3620516899220196e-238)1.3620516899220196e-238(1.362051689810522e-238 1.3620516900786887e-238)+nan.0validexit10.239084#f
(-9.809703639717377e-61 2.9673719752165684e-73)2.9673719752165684e-73(2.967370648013742e-73 2.967372672115747e-73)+nan.0validexit10.178313#f
(-6.416268940031169e-149 1.520790746210474e-149)1.520790746210474e-149(1.520790746210474e-149 1.520790746210474e-149)+nan.0validexit00.187551#f
(-3.230933490941084e-283 5.887441071626347e-294)5.887441071626347e-294(5.8874410412490155e-294 5.887441111243787e-294)+nan.0validexit10.128413#f
(-2.0077303888495448e-199 8.029686773562698e-202)8.029686773562698e-202(8.029686773562698e-202 8.029686773562698e-202)+nan.0validexit00.233406#f
(-6.174609384143866e-170 2.6245118344866006e-173)2.6245118344866006e-173(2.6245118344866002e-173 2.624511834486601e-173)+nan.0validexit00.162306#f
(-1.284810687156146e-8 1.3807114624322109e-22)1.380711462432211e-22(1.3806969204959824e-22 1.3807211543029908e-22)+nan.0validexit10.16819599999999998#f
(6.210664460847271e-53 1.6316100370333053e-68)1.6316100370333053e-68(1.630927802096691e-68 1.632286153958515e-68)+nan.0validexit10.10318300000000001#f
(3.482415271116968e-202 2.8135267132839534e-216)2.8135267132839534e-216(2.8135041526616375e-216 2.8135705475175913e-216)+nan.0validexit10.10995100000000001#f
(-2.1619763540660082e-88 2.7561544830462803e-104)2.7561544830462803e-104(2.7537077877300712e-104 2.757795429176479e-104)+nan.0validexit10.105077#f
(-2.131675076919213e-259 2.184818351766361e-271)2.184818351766361e-271(2.1848181502297558e-271 2.1848185733221876e-271)+nan.0validexit10.22170800000000002#f
(1.4423586240062966e-274 1.406535196470196e-275)1.406535196470196e-275(1.406535196470196e-275 1.406535196470196e-275)+nan.0validexit00.16563799999999998#f
(5.588900546150869e-146 1.2032876559137615e-146)1.2032876559137615e-146(1.2032876559137615e-146 1.2032876559137615e-146)+nan.0validexit00.158312#f
(-9.395742793366995e-262 3.877885092512442e-263)3.877885092512442e-263(3.877885092512442e-263 3.877885092512442e-263)+nan.0validexit00.174286#f
(-1.5929698914600499e-232 5.9224311727688934e-235)5.9224311727688934e-235(5.9224311727688934e-235 5.9224311727688934e-235)+nan.0validexit00.18301#f
(2.7550304578355924e-14 6.979791214241591e-26)6.979791214241591e-26(6.979790907068167e-26 6.979791369291354e-26)+nan.0validexit10.117051#f
(1.7634490422865783e-71 1.7104194809748024e-74)1.7104194809748024e-74(1.7104194809748022e-74 1.7104194809748024e-74)+nan.0validexit00.103534#f
Sollya timings
Total time spent in Sollya 783.0ms
Bogosity

preprocess146.0ms (0.4%)

Algorithm
egg-herbie
Rules
154×fma-neg
59×fma-define
49×sub-neg
39×cancel-sign-sub-inv
35×associate--r+
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
027226
149210
2101210
3201210
4378210
5481210
6638210
7720210
8762210
9768210
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x)))
(-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x))
(neg.f64 (-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x))))
(neg.f64 (-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x)))
(-.f64 (tan.f64 (+.f64 eps x)) (tan.f64 eps))
Outputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
(-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x)))
(-.f64 (tan.f64 (+.f64 eps (neg.f64 x))) (neg.f64 (tan.f64 x)))
(+.f64 (tan.f64 x) (tan.f64 (-.f64 eps x)))
(-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x))
(-.f64 (tan.f64 (-.f64 x eps)) (tan.f64 x))
(neg.f64 (-.f64 (tan.f64 (+.f64 (neg.f64 x) eps)) (tan.f64 (neg.f64 x))))
(-.f64 (tan.f64 (-.f64 x eps)) (tan.f64 x))
(neg.f64 (-.f64 (tan.f64 (+.f64 x (neg.f64 eps))) (tan.f64 x)))
(-.f64 (tan.f64 (+.f64 eps (neg.f64 x))) (neg.f64 (tan.f64 x)))
(+.f64 (tan.f64 x) (tan.f64 (-.f64 eps x)))
(-.f64 (tan.f64 (+.f64 eps x)) (tan.f64 eps))
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 eps))
Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
61.0%
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
Compiler

Compiled 18 to 12 computations (33.3% saved)

simplify4.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01230
11530
22030
32230
42330
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
Outputs
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 9 to 6 computations (33.3% saved)

preprocess95.0ms (0.3%)

Compiler

Compiled 60 to 40 computations (33.3% saved)

end0.0ms (0%)

Profiling

Loading profile data...