
Time bar (total: 13.0s)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 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 |
Compiled 15 to 11 computations (26.7% saved)
| 2.4s | 8256× | 0 | valid |
| 973.0ms | 8238× | 0 | valid-sollya |
| 4.0ms | 18× | 0 | exit-sollya |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (-5.247351337928393e-290 -2.4282606907318444e+163) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.254272 | #f |
| (7.501778245136372e+214 -3.107117089638758e-106) | 1.1281349798048932 | (1.1281349798048932 1.1281349798048932) | +nan.0 | valid | exit | 0 | 0.17360699999999998 | #f |
| (-3.521518188487381e+20 -2.2098228273887469e-60) | -1.0030056699864394 | (-1.0030056699864394 -1.0030056699864394) | +nan.0 | valid | exit | 0 | 0.20039600000000002 | #f |
| (-1002587724383.6624 -4.930210451709451e+286) | 8.2921836556468e+286 | (8.2921836556468e+286 8.2921836556468e+286) | +nan.0 | valid | exit | 0 | 0.275688 | #f |
| (-2.2152067370948476e+164 -1.4868582453165114e+105) | 9.427974326381034e+105 | (9.427974326381034e+105 9.427974326381034e+105) | +nan.0 | valid | exit | 0 | 0.156613 | #f |
| (8.722047183464892e+24 4.275878156476777e-65) | 3.756076498343931 | (3.756076498343931 3.756076498343931) | +nan.0 | valid | exit | 0 | 0.259098 | #f |
| (2.0672561542386146e-230 -2.4467043096593595e+76) | 1.1835515906641469e+306 | (1.1835515906641469e+306 1.1835515906641469e+306) | +nan.0 | valid | exit | 0 | 0.244666 | #f |
| (-3.7081025911121944e-239 -2.535596889254729e+242) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.20851499999999998 | #f |
| (-4.097740638743653e+162 3.268614630469811e-85) | 1.8528049178608503 | (1.8528049178608503 1.8528049178608503) | +nan.0 | valid | exit | 0 | 0.31560099999999996 | #f |
| (7.569022702680529e+214 1.4843596984245922e+114) | 4.99609888658209e+112 | (4.99609888658209e+112 4.99609888658209e+112) | +nan.0 | valid | exit | 0 | 0.285645 | #f |
| (1.578540127604132e+149 -2.4021492592481474e+246) | -9.273479359543595e+245 | (-9.273479359543595e+245 -9.273479359543595e+245) | +nan.0 | valid | exit | 0 | 0.26303699999999997 | #f |
| (-3.506672333349939e-17 -1.0589067446408431e+198) | -3.0196911601069524e+214 | (-3.0196911601069524e+214 -3.0196911601069524e+214) | +nan.0 | valid | exit | 0 | 0.207069 | #f |
| (2.5396095355533392e-269 -1.5457761799895743e+64) | +inf.0 | (+inf.0 +inf.0) | +nan.0 | valid | exit | 0 | 0.151595 | #f |
| (-4.610770508060124e+100 -6.898064649090368e-230) | -1.0652416170626036 | (-1.0652416170626036 -1.0652416170626036) | +nan.0 | valid | exit | 0 | 0.27160900000000004 | #f |
| (1.9020173078268283e+288 -3.044178204704498e-237) | -1.010422926266425 | (-1.010422926266425 -1.010422926266425) | +nan.0 | valid | exit | 0 | 0.337818 | #f |
| (-2.3070607517175373e+22 2.9078402182741228e-213) | -1.080613649373176 | (-1.080613649373176 -1.080613649373176) | +nan.0 | valid | exit | 0 | 0.195785 | #f |
| (8.179890250132308e-304 8.792569003013448e+84) | -inf.0 | (-inf.0 -inf.0) | +nan.0 | valid | exit | 0 | 0.133866 | #f |
| (-1.2031592236910127e+82 -2.5569677981992688e+138) | -1.0370379029107992e+138 | (-1.0370379029107992e+138 -1.0370379029107992e+138) | +nan.0 | valid | exit | 0 | 0.236286 | #f |
| 1× | egg-herbie |
| 233× | fma-define |
| 186× | fma-neg |
| 54× | distribute-lft-neg-in |
| 41× | sub-neg |
| 37× | cancel-sign-sub-inv |
Useful iterations: 1 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 37 | 342 |
| 1 | 94 | 252 |
| 2 | 257 | 252 |
| 3 | 520 | 252 |
| 4 | 812 | 252 |
| 5 | 1028 | 252 |
| 6 | 1154 | 252 |
| 7 | 1284 | 252 |
| 8 | 1294 | 252 |
| 1× | saturated |
| 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))) |
(negabs B)
Compiled 14 to 10 computations (28.6% saved)
Compiled 2 to 2 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 99.7% | (+.f64 (neg.f64 (*.f64 x (/.f64 #s(literal 1 binary64) (tan.f64 B)))) (/.f64 #s(literal 1 binary64) (sin.f64 B))) |
Compiled 28 to 20 computations (28.6% saved)
| 1× | egg-herbie |
| 14× | neg-mul-1 |
| 12× | unsub-neg |
| 6× | distribute-lft-neg-in |
| 6× | distribute-rgt-neg-in |
| 6× | *-commutative |
Useful iterations: 1 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 16 | 46 |
| 1 | 30 | 42 |
| 2 | 44 | 42 |
| 3 | 53 | 42 |
| 4 | 61 | 42 |
| 5 | 81 | 42 |
| 6 | 109 | 42 |
| 1× | saturated |
| 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))) |
| 1× | fuel |
Compiled 13 to 10 computations (23.1% saved)
(negabs B)
Compiled 106 to 80 computations (24.5% saved)
Loading profile data...