expq3 (problem 3.4.2)
Time bar (total: 1.2min)
| 1× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 25.4% | 74.6% | 0% | 0% | 0% | 0 |
| 0% | 0% | 25.4% | 74.6% | 0% | 0% | 0% | 1 |
| 0% | 0% | 25.4% | 74.6% | 0% | 0% | 0% | 2 |
| 0% | 0% | 25.4% | 74.6% | 0% | 0% | 0% | 3 |
| 0% | 0% | 22.2% | 77.8% | 0% | 0% | 0% | 4 |
| 0% | 0% | 20.6% | 79.4% | 0% | 0% | 0% | 5 |
| 0% | 0% | 18.3% | 81.7% | 0% | 0% | 0% | 6 |
| 0% | 0% | 10.7% | 89.3% | 0% | 0% | 0% | 7 |
| 0% | 0% | 9.3% | 90.7% | 0% | 0% | 0% | 8 |
| 0% | 0% | 8.2% | 91.8% | 0% | 0% | 0% | 9 |
| 0% | 0% | 5.7% | 94.3% | 0% | 0% | 0% | 10 |
| 0% | 0% | 5% | 95% | 0% | 0% | 0% | 11 |
| 0% | 0% | 4.4% | 95.6% | 0% | 0% | 0% | 12 |
Compiled 54 to 30 computations (44.4% saved)
| 34.5s | 63761× | 0 | precondition |
| 14.6s | 5987× | 2 | valid |
| 915.0ms | 5921× | 2 | valid-sollya |
| 3.0s | 2267× | 1 | valid |
| 328.0ms | 2248× | 1 | valid-sollya |
| 73.0ms | 66× | 2 | exit-sollya |
| 18.0ms | 19× | 1 | exit-sollya |
| 0.0ms | 2× | 0 | valid-sollya |
| 1.0ms | 2× | 0 | valid |
| Pt | Rival-out | Sollya-interval | Sollya-point | status | Sollya status | Rival iter | sollya-time | check |
|---|---|---|---|---|---|---|---|---|
| (-1.0170871948352523e-261 1.4077573103781589e-19 5.001312239177227e-286) | -9.831998722213585e+260 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.22275499999999998 | #f |
| (-1.8127523882556617e-240 6.540885159320958e-162 1.7852868689977277e-254) | -5.516473217626041e+239 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.286647 | #f |
| (-3.9657349366813827e-171 5.422264149897295e-97 1.753943881474446e-181) | -2.5216007019289667e+170 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.2309 | #f |
| (-2.280981758842342e-12 -4.390830984912274e-286 2.1716771324639092e-305) | -2.2774732241714362e+285 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.252457 | #f |
| (3.075656851508081e-178 1.2654478371864853e-190 3.404697003674842e-198) | 7.902340741470203e+189 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (2.4285824458055034e-160 -1.55247692347387e-183 1.2665584601126978e-200) | -6.441319576991646e+182 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.116906 | #f |
| (3.5732473401819347e-104 3.172320562155304e-137 1.7504600253653277e-150) | 3.1522665519041706e+136 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 1 | 5.0 | #f |
| (-1.0068212159362666e-159 3.981629055876903e-32 1.0081493875318746e-161) | -9.93224997816595e+158 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.132183 | #f |
| (-1.6442156787731058e-228 -2.0801010417282372e-13 6.526545657697839e-230) | -6.081927163875412e+227 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-5.546079274512395e-203 8.049145191531527e-24 2.774917880332939e-211) | -1.8030755611366896e+202 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.205524 | #f |
| (-7.836022292580892e-109 -6.298697449260406e-162 1.0917987435105524e-164) | -1.587629836256733e+161 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.307354 | #f |
| (-1.8314424727245859e-84 -2.556602773064763e-111 1.812939775210737e-137) | -3.911440645123122e+110 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.280727 | #f |
| (-1.659015461610235e-50 8.293435722232811e-203 6.785218563453857e-212) | 1.2057728949646622e+202 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.267503 | #f |
| (-5.224770349458432e-94 9.186051372080999e-192 7.949485447994147e-204) | 1.0886070189410022e+191 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.237327 | #f |
| (4.1255607080252486e-207 5.891987774816138e-283 5.026296486020389e-308) | 1.6972200863590648e+282 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.201713 | #f |
| (-4.254292615261507e-185 -3.9002839759308847e-113 7.587557676466961e-200) | -2.3505670400119643e+184 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.252411 | #f |
| (-1.2700399227811975e-49 -9.757175462650245e-17 1.3065459573464466e-61) | -7.873768234073693e+48 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.225709 | #f |
| (-7.11574814906752e-215 -1.1213177604711693e-124 1.7809961873240149e-230) | -1.405333605196587e+214 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.157677 | #f |
| (-2.9213660466310134e-152 3.387246737521202e-86 5.905886349322832e-168) | -3.4230561457822894e+151 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.237624 | #f |
| (-1.1997900364018688e-131 2.0619126675639475e-30 8.175125263326348e-138) | -8.334791669040421e+130 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.262645 | #f |
| (-3.948005433411142e-106 6.3901814458097146e-102 6.246955546394795e-118) | -2.532768088841701e+105 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.238351 | #f |
| (-2.2900990123251814e-43 -9.378215754147631e-286 1.366340979165058e-300) | -1.0663009107651823e+285 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.263314 | #f |
| (-6.785072149963112e-252 -2.7589480344674178e-283 9.5433115928547e-285) | -3.6245698994944575e+282 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.282633 | #f |
| (6.248125150244242e-157 3.76210093798082e-157 8.36395170791215e-161) | 4.25856933943317e+156 | (0.0 +inf.0) | +nan.0 | valid | exit | 1 | 0.240406 | #f |
| (3.258321119919687e-277 1.5078079597326985e-50 2.5399826856091374e-292) | 3.0690652124080653e+276 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.240893 | #f |
| (-3.264727640810566e-188 -6.82440019911103e-150 1.3830358346922715e-195) | -3.063042648641037e+187 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.186865 | #f |
| (-4.2199788201491926e-182 -2.2259285433485302e-198 1.0885584667124535e-205) | -4.492507196550301e+197 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.24605999999999997 | #f |
| (9.563214156017603e-49 -4.875211190405999e-202 9.16066008428665e-203) | -2.0511931913183884e+201 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.22658699999999998 | #f |
| (1.752220910251801e-239 -3.428673268245634e-81 1.529744665427693e-242) | 5.707042954168925e+238 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.23883500000000002 | #f |
| (-1.6052946065305265e-121 -2.6770803198720625e-239 1.3553905623539589e-241) | -3.735412765082035e+238 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.25717999999999996 | #f |
| (-1.4708351249798998e-71 -8.774381019722367e-29 7.632976459158486e-91) | -6.798858573721279e+70 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.228182 | #f |
| (4.2242976728469034e-139 -4.8449401791958656e-126 1.3544493736940522e-145) | 2.3672574175530993e+138 | (0.0 +inf.0) | +nan.0 | valid | exit | 1 | 0.246014 | #f |
| (4.710052219621738e-238 -5.8069848526227675e-123 1.3681059463920297e-250) | 2.123118711580462e+237 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.28940699999999997 | #f |
| (1.1448765947069724e-205 4.57982785870537e-257 1.5388663784868913e-266) | 2.183488180891325e+256 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-4.064398615481802e-8 -7.790600282603457e-142 2.710621193823205e-143) | -1.2835981358625431e+141 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 1 | 5.0 | #f |
| (-9.616569720618006e-276 1.0747686154524334e-141 9.3555369674796e-285) | -1.0398718348144367e+275 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.227899 | #f |
| (3.0540477136989214e-27 -8.653628149575485e-62 1.7804977307701575e-80) | -1.1555846665875703e+61 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.11393800000000001 | #f |
| (6.977490942311235e-102 3.916997737331219e-106 1.032577287286503e-122) | 2.553119007689068e+105 | (0.0 +inf.0) | +nan.0 | valid | exit | 1 | 0.197902 | #f |
| (3.2577022712401895e-24 -4.3349375469210464e-8 6.982079354836145e-29) | 3.0696482266910945e+23 | (0.0 +inf.0) | +nan.0 | valid | exit | 1 | 0.25005 | #f |
| (3.4803090306069734e-166 2.0817410818916943e-110 4.119747999306549e-174) | 2.873308063179659e+165 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.200436 | #f |
| (7.990056979617496e-86 -1.531105859602941e-46 6.70434746251467e-92) | 1.2515555302684119e+85 | (0.0 +inf.0) | +nan.0 | valid | exit | 1 | 0.12136000000000001 | #f |
| (-1.0549968718547382e-41 2.0427081823270823e-269 1.6924489373298896e-291) | 4.895461861129796e+268 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.255867 | #f |
| (-4.721193385205408e-161 -1.1805771243372367e-226 9.842963577080456e-253) | -8.470433480247123e+225 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.24623899999999999 | #f |
| (1.1420745347097866e-286 1.39829328324168e-55 1.1800197394322004e-293) | 8.755995949547292e+285 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.13375499999999999 | #f |
| (-4.092724190844141e-273 546.8319662129466 2.1377610002979188e-280) | -2.443360347215936e+272 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.237714 | #f |
| (4.535020801026936e-178 -3.404394932829659e-203 2.571118425969136e-228) | -2.9373795336042923e+202 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.268747 | #f |
| (-1.3449006933476999e-254 -7.724620754749148e-240 2.425968842756104e-274) | -7.435493229695805e+253 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.283286 | #f |
| (2.9725943037473637e-22 -7.951395753048932e-299 6.973874853653626e-304) | -1.2576408357193816e+298 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.234574 | #f |
| (4.1209265811168563e-184 9.056466768612304e-89 7.013241931092754e-208) | 2.426638719025611e+183 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-2.0733837052777188e-148 -4.7270806380240795e-163 2.5692729545314516e-180) | -2.1154705759747784e+162 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-2.3192030132497963e-113 1.0223487280173462e-75 1.9497751005806597e-125) | -4.311826063897461e+112 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.11614400000000001 | #f |
| (-1.0603624099545658e-187 3.9919410309384816e-49 1.4226913989989446e-212) | -9.430737930844302e+186 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-2.9230857966999704e-89 4.350701098734516e-258 8.083675323419783e-279) | 2.2984801237917009e+257 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.303403 | #f |
| (9.817762026678747e-262 2.0969889969726883e-116 4.186904336990114e-282) | 1.018562068710368e+261 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.21380100000000002 | #f |
| (2.2248246279913187e-89 -4.9302207465826914e-33 1.2089621792644892e-95) | 4.494736292553761e+88 | (0.0 +inf.0) | +nan.0 | valid | exit | 1 | 0.247228 | #f |
| (1.478536769005693e-242 -2.357877680634265e-195 1.25064819648241e-255) | 6.763443567740922e+241 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (7.267899918115482e-269 -7.717797548359473e-113 2.4717401393533495e-269) | 1.3759132779298005e+268 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.335013 | #f |
| (-3.853221587827628e-293 -2.1442947999607456e-121 3.8002535843443556e-299) | -2.5952309702587875e+292 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.263231 | #f |
| (-8.482673741897685e-30 -3.048208611358513e-265 7.397168688660557e-272) | -3.280615362983061e+264 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.25537 | #f |
| (-2.115315255967814e-25 -8.002021601990392e-177 5.466891730196281e-192) | -1.2496842044906051e+176 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.247294 | #f |
| (1.3091762057104415e-102 1.362473503889786e-235 1.428326470415949e-253) | 7.33959227203359e+234 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (1.0739195303937427e-143 -2.6495162941913825e-56 5.181946506706388e-158) | 9.311684643944963e+142 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 1 | 5.0 | #f |
| (-2.3208860109864903e-168 2.8646573128104417e-22 2.520438881138039e-179) | -4.3086993297656653e+167 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.226605 | #f |
| (3.894459744761517e-259 -2.020530497427161e-162 4.723746284097909e-265) | 2.567750254307062e+258 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.22886900000000002 | #f |
| (9.143792435309764e-6 -7.747600150745782 3.586779748626614e-18) | 109363.68327093117 | (33.01771630867434 +inf.0) | +nan.0 | valid | exit | 1 | 0.174654 | #f |
| (-3.0963205714832774e-192 -1.1544874867338613e-190 2.1934084053946598e-199) | -3.316258273361645e+191 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-3.772864903408525e-179 -2.2601269452140455e-106 1.4911370790327588e-193) | -2.6505057180726736e+178 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.250847 | #f |
| (2.081479832338027e-29 3.037313983708708e-259 2.8228410623925974e-282) | 3.292382695248884e+258 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.243713 | #f |
| (-4.028595078089547e-246 8.222483407600185e-133 6.270458516124758e-256) | -2.4822549315981966e+245 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.245869 | #f |
| (4.948214784428335e-99 -9.570971603427757e-237 4.792838795516291e-253) | -1.0448260024529369e+236 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.226514 | #f |
| (2.2996001812288383e-66 1.1275565911666365e-201 7.802908474642633e-205) | 8.868734463831576e+200 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.247649 | #f |
| (-3.8251365006500206e-277 -3.8640961028698336e-221 3.478077593234707e-297) | -2.6142857904026853e+276 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.261156 | #f |
| (-2.0699616686910316e-156 -1.3477183115409725e-19 5.529920264046617e-162) | -4.831007332770387e+155 | (-inf.0 0.0) | +nan.0 | valid | exit | 1 | 0.181511 | #f |
| (-1.7602240560923304e-270 5.9615632836950556e-117 5.397404682009878e-291) | -5.681094952309561e+269 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.242787 | #f |
| (-3.405467078883309e-130 9.993718411396205e-174 1.1501079269963054e-175) | 1.0006285536919502e+173 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.246864 | #f |
| (-3.1246975002444986e-7 1.8089307305334988e-259 1.6592996682755803e-265) | 5.528127656414323e+258 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-5.798620399415591e-126 -9.623172034314625e-180 1.0178322622706825e-198) | -1.0391583943778278e+179 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.261958 | #f |
| (3.3918524964034166e-224 5.3032144128949404e-235 4.302205931087276e-248) | 1.8856488200516696e+234 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.110206 | #f |
| (2.7917540889233005e-191 2.6006848808267367e-10 1.2660671499619424e-214) | 3.581977381058198e+190 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.231635 | #f |
| (-3.1259414626116896e-212 5.316562770960042e-266 1.3957758145954915e-275) | 1.8809144988603684e+265 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.24819799999999997 | #f |
| (4.481990220815379e-26 -2.5358871910487092e-254 2.1836884698355684e-277) | -3.94339307966792e+253 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-9.47205242475318e-263 3.7510669488306103e-265 8.191653772245357e-275) | 2.6553507893069207e+264 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.16345500000000002 | #f |
| (-3.083981731444687e-30 -4.8447728808464086e-237 1.7909574680567053e-252) | -2.0640802460595312e+236 | (-inf.0 0.0) | +nan.0 | valid | exit | 2 | 0.222805 | #f |
| (1.5843856940900114e-65 6.295709258457583e-174 2.0086528838498793e-192) | 1.588383387712213e+173 | (+nan.0 +nan.0) | +nan.0 | valid | exit | 2 | 5.0 | #f |
| (-4.3172933556541595e-231 1.4503182744567806e-290 3.6657262217847756e-292) | 6.895038265821699e+289 | (0.0 +inf.0) | +nan.0 | valid | exit | 2 | 0.319869 | #f |
| 1× | egg-herbie |
| 662× | times-frac |
| 578× | div-sub |
| 499× | fma-define |
| 425× | distribute-lft-in |
| 424× | distribute-rgt-in |
Useful iterations: 1 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 95 | 937 |
| 1 | 292 | 921 |
| 2 | 754 | 921 |
| 3 | 2307 | 921 |
| 4 | 7707 | 921 |
| 1× | node limit |
| Inputs |
|---|
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64)))) |
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))) |
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64))))) |
(neg.f64 (/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64))))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 b a) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 a (-.f64 (exp.f64 (*.f64 (+.f64 eps b) a)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 eps a)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b a)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 b (-.f64 (exp.f64 (*.f64 (+.f64 a eps) b)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a b)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 eps b)) #s(literal 1 binary64)))) |
| Outputs |
|---|
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps b))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (expm1.f64 (*.f64 eps a)))) |
(*.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps b))))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps b))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (expm1.f64 (*.f64 eps a)))) |
(*.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps b))))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps (neg.f64 a)))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 b (neg.f64 a)))) (expm1.f64 (*.f64 eps b)))) |
(*.f64 eps (/.f64 (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (expm1.f64 (*.f64 eps b))) (expm1.f64 (*.f64 a (neg.f64 eps))))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 a (neg.f64 eps)))))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 eps (neg.f64 a)))))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64)))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b)))))) |
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps (neg.f64 b)))) (/.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (expm1.f64 (*.f64 eps a)))) |
(*.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b)))))) |
(/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64)))) |
(*.f64 (/.f64 (neg.f64 eps) (expm1.f64 (*.f64 eps (neg.f64 a)))) (/.f64 (expm1.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) (expm1.f64 (*.f64 eps (neg.f64 b))))) |
(*.f64 (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b)))) (/.f64 (neg.f64 eps) (*.f64 (expm1.f64 (*.f64 a (neg.f64 eps))) (expm1.f64 (*.f64 eps (neg.f64 b)))))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b)))) (*.f64 (expm1.f64 (*.f64 eps (neg.f64 b))) (neg.f64 (expm1.f64 (*.f64 a (neg.f64 eps))))))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 (neg.f64 b) a))) (*.f64 (expm1.f64 (*.f64 eps (neg.f64 a))) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 b))))))) |
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 (neg.f64 a) b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 (neg.f64 a) eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))) |
(/.f64 (*.f64 eps (expm1.f64 (*.f64 eps (+.f64 b (neg.f64 a))))) (neg.f64 (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 eps (neg.f64 a)))))) |
(*.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps b)) (neg.f64 (expm1.f64 (*.f64 a (neg.f64 eps))))))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 b a))) (*.f64 (expm1.f64 (*.f64 eps b)) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 a))))))) |
(neg.f64 (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a (neg.f64 b)) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 (neg.f64 b) eps)) #s(literal 1 binary64))))) |
(/.f64 (*.f64 eps (expm1.f64 (*.f64 eps (-.f64 a b)))) (neg.f64 (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b)))))) |
(*.f64 eps (/.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (*.f64 (expm1.f64 (*.f64 eps a)) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 b))))))) |
(*.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (neg.f64 (expm1.f64 (*.f64 eps (neg.f64 b))))))) |
(*.f64 (expm1.f64 (*.f64 eps (-.f64 a b))) (/.f64 (neg.f64 eps) (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps (neg.f64 b)))))) |
(neg.f64 (/.f64 (*.f64 (neg.f64 eps) (-.f64 (exp.f64 (*.f64 (+.f64 a b) (neg.f64 eps))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a (neg.f64 eps))) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b (neg.f64 eps))) #s(literal 1 binary64))))) |
(/.f64 (*.f64 (neg.f64 eps) (expm1.f64 (*.f64 (+.f64 a b) (neg.f64 eps)))) (neg.f64 (*.f64 (expm1.f64 (*.f64 eps (neg.f64 a))) (expm1.f64 (*.f64 eps (neg.f64 b)))))) |
(/.f64 (*.f64 eps (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b))))) (*.f64 (expm1.f64 (*.f64 a (neg.f64 eps))) (expm1.f64 (*.f64 eps (neg.f64 b))))) |
(*.f64 (expm1.f64 (*.f64 eps (neg.f64 (+.f64 a b)))) (/.f64 (/.f64 eps (expm1.f64 (*.f64 a (neg.f64 eps)))) (expm1.f64 (*.f64 eps (neg.f64 b))))) |
(*.f64 eps (/.f64 (/.f64 (expm1.f64 (*.f64 eps (-.f64 (neg.f64 b) a))) (expm1.f64 (*.f64 eps (neg.f64 b)))) (expm1.f64 (*.f64 eps (neg.f64 a))))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 b a) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)))) |
(*.f64 (/.f64 eps (expm1.f64 (*.f64 eps b))) (/.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (expm1.f64 (*.f64 eps a)))) |
(*.f64 (expm1.f64 (*.f64 eps (+.f64 a b))) (/.f64 eps (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 eps b))))) |
(/.f64 (*.f64 a (-.f64 (exp.f64 (*.f64 (+.f64 eps b) a)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 eps a)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b a)) #s(literal 1 binary64)))) |
(*.f64 a (/.f64 (expm1.f64 (*.f64 a (+.f64 eps b))) (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 a b))))) |
(*.f64 (expm1.f64 (*.f64 a (+.f64 eps b))) (/.f64 a (*.f64 (expm1.f64 (*.f64 eps a)) (expm1.f64 (*.f64 a b))))) |
(/.f64 (*.f64 b (-.f64 (exp.f64 (*.f64 (+.f64 a eps) b)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a b)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 eps b)) #s(literal 1 binary64)))) |
(*.f64 (/.f64 b (expm1.f64 (*.f64 a b))) (/.f64 (expm1.f64 (*.f64 b (+.f64 eps a))) (expm1.f64 (*.f64 eps b)))) |
(*.f64 b (/.f64 (expm1.f64 (*.f64 b (+.f64 eps a))) (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 a b))))) |
(*.f64 (expm1.f64 (*.f64 b (+.f64 eps a))) (/.f64 b (*.f64 (expm1.f64 (*.f64 eps b)) (expm1.f64 (*.f64 a b))))) |
(sort a b)
Compiled 27 to 17 computations (37% saved)
Compiled 3 to 3 computations (0% saved)
| Status | Accuracy | Program |
|---|---|---|
| 0.0% | (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
Compiled 54 to 34 computations (37% saved)
| 1× | egg-herbie |
| 6× | *-commutative |
| 5× | +-commutative |
| 4× | unsub-neg |
| 4× | sub-neg |
| 3× | 1-exp |
Useful iterations: 0 (0.0ms)
| Iter | Nodes | Cost |
|---|---|---|
| 0 | 24 | 97 |
| 1 | 39 | 97 |
| 2 | 45 | 97 |
| 3 | 48 | 97 |
| 4 | 51 | 97 |
| 5 | 56 | 97 |
| 1× | saturated |
| Inputs |
|---|
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
| Outputs |
|---|
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 eps (+.f64 a b))) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 eps a)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 eps b)) #s(literal 1 binary64)))) |
(/.f64 (*.f64 eps (+.f64 (exp.f64 (*.f64 eps (+.f64 a b))) #s(literal -1 binary64))) (*.f64 (+.f64 (exp.f64 (*.f64 eps a)) #s(literal -1 binary64)) (+.f64 (exp.f64 (*.f64 eps b)) #s(literal -1 binary64)))) |
| 1× | fuel |
Compiled 27 to 17 computations (37% saved)
(sort a b)
Compiled 236 to 150 computations (36.4% saved)
Loading profile data...