2frac (problem 3.3.1)
Time bar (total: 31.2s)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 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 |
| 75% | 75% | 25% | 0% | 0% | 0% | 0% | 4 |
| 87.5% | 87.5% | 12.5% | 0% | 0% | 0% | 0% | 5 |
| 93.8% | 93.7% | 6.2% | 0% | 0% | 0% | 0% | 6 |
| 96.9% | 96.8% | 3.1% | 0% | 0% | 0% | 0% | 7 |
| 98.4% | 98.4% | 1.6% | 0% | 0% | 0% | 0% | 8 |
| 99.2% | 99.2% | 0.8% | 0% | 0% | 0% | 0% | 9 |
| 99.6% | 99.6% | 0.4% | 0% | 0% | 0% | 0% | 10 |
| 99.8% | 99.8% | 0.2% | 0% | 0% | 0% | 0% | 11 |
| 99.9% | 99.9% | 0.1% | 0% | 0% | 0% | 0% | 12 |
Compiled 11 to 7 computations (36.4% saved)
| 1.7s | 4287× | 0 | valid |
| 379.0ms | 4277× | 0 | valid-sollya |
| 2.8s | 3969× | 1 | valid |
| 592.0ms | 3958× | 1 | valid-sollya |
| 2.0ms | 11× | 1 | exit-sollya |
| 11.0ms | 10× | 0 | exit-sollya |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (4.200315905712422e+184) | -0.0 | (-4.7842535765268324e-204 1.5947511921756108e-204) | +nan.0 | valid | exit | 1 | 0.211308 | #f |
| (-8.4877024095340435e+183) | -0.0 | (-1.2758009537404886e-203 1.2758009537404886e-203) | +nan.0 | valid | exit | 1 | 0.205882 | #f |
| (2.657382385795694e+143) | -1.416093391305133e-287 | (-5.556896873712694e-163 2.778448436856347e-163) | +nan.0 | valid | exit | 1 | 0.237679 | #f |
| (-5.515645488506009e+121) | -3.2870575720218615e-244 | (-2.624170354518394e-141 1.312085177259197e-141) | +nan.0 | valid | exit | 1 | 0.198679 | #f |
| (7.153253336392515e-266) | -1.3979653074950562e+265 | (-1.3979653074950562e+265 -1.3979653074950562e+265) | +nan.0 | valid | exit | 0 | 0.095587 | #f |
| (-2.852292008036363e-286) | 3.50595239611684e+285 | (3.50595239611684e+285 3.50595239611684e+285) | +nan.0 | valid | exit | 0 | 0.231951 | #f |
| (5.0108714966698045e+284) | -0.0 | (-3.645561009778199e-304 1.8227805048890994e-304) | +nan.0 | valid | exit | 1 | 0.113409 | #f |
| (1.0487395482610313e-184) | -9.535255933259607e+183 | (-9.535255933259607e+183 -9.535255933259607e+183) | +nan.0 | valid | exit | 0 | 0.186281 | #f |
| (1.7005595345015637e+260) | -0.0 | (-8.814425663402488e-280 4.407212831701244e-280) | +nan.0 | valid | exit | 1 | 0.190946 | #f |
| (-9.624576721071661e-94) | 1.0390067313928105e+93 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (1.2250772915956972e+173) | -0.0 | (-8.767237396033612e-193 8.767237396033612e-193) | +nan.0 | valid | exit | 1 | 0.17227900000000002 | #f |
| (-1.1853599300021768e+230) | -0.0 | (-1.676041797431891e-249 5.586805991439637e-250) | +nan.0 | valid | exit | 1 | 0.158789 | #f |
| (2.995789998930575e-190) | -3.3380176860092864e+189 | (-3.3380176860092864e+189 -3.3380176860092864e+189) | +nan.0 | valid | exit | 0 | 0.185988 | #f |
| (-5.363467158705638e-22) | 1.8644655973643164e+21 | (1.8644655973643164e+21 1.8644655973643164e+21) | +nan.0 | valid | exit | 0 | 0.094485 | #f |
| (-1.4506882481943719e-303) | 6.893279801809038e+302 | (6.893279801809038e+302 6.893279801809038e+302) | +nan.0 | valid | exit | 0 | 0.199521 | #f |
| (-6.7968847153476714e+106) | -2.1646126518733808e-214 | (-1.4772765788457177e-126 1.4772765788457177e-126) | +nan.0 | valid | exit | 1 | 0.204869 | #f |
| (-6.3783086246195255e+233) | -0.0 | (-2.727932613007635e-253 1.3639663065038175e-253) | +nan.0 | valid | exit | 1 | 0.203295 | #f |
| (-6.191921694452174e-155) | 1.6150075038836136e+154 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 0 | 5.0 | #f |
| (2.4772001357656255e+278) | -0.0 | (-3.8226477813891845e-298 3.8226477813891845e-298) | +nan.0 | valid | exit | 1 | 0.17646 | #f |
| (-1.6766648096558366e-85) | 5.964221317469332e+84 | (5.964221317469332e+84 5.964221317469332e+84) | +nan.0 | valid | exit | 0 | 0.264774 | #f |
| (2.2753932268411165e-186) | -4.394844760034204e+185 | (-4.394844760034204e+185 -4.394844760034204e+185) | +nan.0 | valid | exit | 0 | 0.192908 | #f |
| 1× | egg-herbie |
| 89× | fma-neg |
| 39× | fma-define |
| 24× | distribute-lft-neg-in |
| 23× | sub-neg |
| 20× | cancel-sign-sub-inv |
Useful iterations: 2 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 17 | 144 |
| 1 | 34 | 128 |
| 2 | 70 | 124 |
| 3 | 138 | 124 |
| 4 | 236 | 124 |
| 5 | 334 | 124 |
| 6 | 411 | 124 |
| 7 | 456 | 124 |
| 8 | 473 | 124 |
| 9 | 475 | 124 |
| 1× | saturated |
| Inputs |
|---|
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x))) |
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x)))) |
| Outputs |
|---|
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal 1 binary64) x)) |
(+.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal -1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal 1 binary64) x)) |
(+.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal -1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x))) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) (neg.f64 x))) (/.f64 #s(literal 1 binary64) (neg.f64 x))) |
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (-.f64 #s(literal 1 binary64) x))) |
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 (neg.f64 x) #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) (neg.f64 x)))) |
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) (neg.f64 x))) (/.f64 #s(literal 1 binary64) (neg.f64 x)))) |
(+.f64 (neg.f64 (/.f64 #s(literal 1 binary64) (-.f64 #s(literal 1 binary64) x))) (/.f64 #s(literal -1 binary64) x)) |
(+.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal -1 binary64) (-.f64 #s(literal 1 binary64) x))) |
(+.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal -1 binary64)))) |
Compiled 10 to 6 computations (40% saved)
Compiled 1 to 1 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 79.0% | (-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
Compiled 20 to 12 computations (40% saved)
| 1× | egg-herbie |
| 8× | neg-mul-1 |
| 7× | unsub-neg |
| 5× | +-commutative |
| 4× | sub-neg |
| 3× | *-rgt-identity |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 10 | 31 |
| 1 | 19 | 31 |
| 2 | 27 | 31 |
| 3 | 33 | 31 |
| 4 | 40 | 31 |
| 5 | 52 | 31 |
| 6 | 68 | 31 |
| 1× | saturated |
| Inputs |
|---|
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
| Outputs |
|---|
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 x #s(literal 1 binary64))) (/.f64 #s(literal 1 binary64) x)) |
(-.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal 1 binary64) x)) |
(+.f64 (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 1 binary64) x)) (/.f64 #s(literal -1 binary64) x)) |
| 1× | fuel |
Compiled 10 to 7 computations (30% saved)
Compiled 40 to 26 computations (35% saved)
Loading profile data...