0.002 * [progress]: [Phase 1 of 3] Setting up. 0.003 * * * [progress]: [1/2] Preparing points 0.006 * * * * [points]: Sampling 256 additional inputs, on iter 0 have 0 / 256 0.008 * * * * [points]: Computing exacts on every 16 of 256 points to ramp up precision 0.070 * * * * [points]: Setting MPFR precision to 64 0.072 * * * * [points]: Setting MPFR precision to 320 0.074 * * * * [points]: Computing exacts on every 8 of 256 points to ramp up precision 0.077 * * * * [points]: Setting MPFR precision to 64 0.079 * * * * [points]: Setting MPFR precision to 320 0.081 * * * * [points]: Computing exacts on every 4 of 256 points to ramp up precision 0.084 * * * * [points]: Setting MPFR precision to 64 0.087 * * * * [points]: Setting MPFR precision to 320 0.091 * * * * [points]: Computing exacts on every 2 of 256 points to ramp up precision 0.093 * * * * [points]: Setting MPFR precision to 64 0.099 * * * * [points]: Setting MPFR precision to 320 0.105 * * * * [points]: Computing exacts for 256 points 0.108 * * * * [points]: Setting MPFR precision to 64 0.125 * * * * [points]: Setting MPFR precision to 320 0.173 * * * * [points]: Filtering points with unrepresentable outputs 0.175 * * * * [points]: Sampled 256 points with exact outputs 0.175 * * * [progress]: [2/2] Setting up program. 0.196 * [progress]: [Phase 2 of 3] Improving. 0.196 * * * * [progress]: [ 1 / 1 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 0.198 * [simplify]: Simplifying: (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 0.199 * * [simplify]: iteration 1: (16 enodes) 0.209 * * [simplify]: iteration 2: (45 enodes) 0.217 * * [simplify]: iteration 3: (91 enodes) 0.235 * * [simplify]: iteration 4: (310 enodes) 0.364 * * [simplify]: iteration 5: (1361 enodes) 2.501 * * [simplify]: Extracting #0: cost 1 inf + 0 2.501 * * [simplify]: Extracting #1: cost 109 inf + 0 2.503 * * [simplify]: Extracting #2: cost 706 inf + 1 2.517 * * [simplify]: Extracting #3: cost 1290 inf + 2251 2.525 * * [simplify]: Extracting #4: cost 1800 inf + 50605 2.535 * * [simplify]: Extracting #5: cost 2124 inf + 108239 2.566 * * [simplify]: Extracting #6: cost 2247 inf + 615589 2.796 * * [simplify]: Extracting #7: cost 604 inf + 4149249 3.185 * * [simplify]: Extracting #8: cost 6 inf + 5636236 3.571 * * [simplify]: Extracting #9: cost 0 inf + 5653221 4.025 * [simplify]: Simplified to: (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 c a) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)) 4.060 * * [progress]: iteration 1 / 4 4.060 * * * [progress]: picking best candidate 4.092 * * * * [pick]: Picked #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 4.092 * * * [progress]: localizing error 4.758 * * * [progress]: generating rewritten candidates 4.758 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 4.763 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 4.763 * * * * [progress]: [ 3 / 4 ] rewriting at (2) 4.769 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1 2) 4.778 * * * [progress]: generating series expansions 4.778 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 4.778 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 4.778 * * * * [progress]: [ 3 / 4 ] generating series at (2) 4.779 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1 2) 4.779 * * * [progress]: simplifying candidates 4.779 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 4.779 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))> 4.779 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 4))))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 4.779 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)))> 4.780 * [simplify]: Simplifying: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (real->posit16 4) a) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 2) a)) 4.780 * * [simplify]: iteration 1: (24 enodes) 4.790 * * [simplify]: iteration 2: (65 enodes) 4.811 * * [simplify]: iteration 3: (180 enodes) 4.890 * * [simplify]: iteration 4: (623 enodes) 5.203 * * [simplify]: Extracting #0: cost 7 inf + 0 5.203 * * [simplify]: Extracting #1: cost 215 inf + 0 5.209 * * [simplify]: Extracting #2: cost 514 inf + 1206 5.218 * * [simplify]: Extracting #3: cost 617 inf + 194688 5.256 * * [simplify]: Extracting #4: cost 501 inf + 851856 5.411 * * [simplify]: Extracting #5: cost 185 inf + 1681136 5.609 * * [simplify]: Extracting #6: cost 2 inf + 2083473 5.763 * * [simplify]: Extracting #7: cost 0 inf + 2087081 5.939 * [simplify]: Simplified to: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (+.p16 (*.p16 (+.p16 (neg.p16 b) (neg.p16 b)) (+.p16 (neg.p16 b) b)) (*.p16 (*.p16 a c) (real->posit16 4))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (real->posit16 2)) (*.p16 (real->posit16 2) (*.p16 a (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b))) (*.p16 a (real->posit16 4)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)) 5.940 * * * [progress]: adding candidates to table 6.707 * * [progress]: iteration 2 / 4 6.707 * * * [progress]: picking best candidate 6.852 * * * * [pick]: Picked #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 6.852 * * * [progress]: localizing error 7.230 * * * [progress]: generating rewritten candidates 7.230 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 7.233 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 7.234 * * * * [progress]: [ 3 / 4 ] rewriting at (2 1 1 2 1 2) 7.241 * * * * [progress]: [ 4 / 4 ] rewriting at (2) 7.249 * * * [progress]: generating series expansions 7.249 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 7.249 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 7.249 * * * * [progress]: [ 3 / 4 ] generating series at (2 1 1 2 1 2) 7.249 * * * * [progress]: [ 4 / 4 ] generating series at (2) 7.249 * * * [progress]: simplifying candidates 7.249 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 4))))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (*.p16 a (real->posit16 2))))> 7.250 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 7.250 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> 7.250 * [simplify]: Simplifying: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (*.p16 (real->posit16 4) a) (*.p16 a (real->posit16 2)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))) (real->posit16 2)) 7.251 * * [simplify]: iteration 1: (22 enodes) 7.260 * * [simplify]: iteration 2: (53 enodes) 7.279 * * [simplify]: iteration 3: (140 enodes) 7.355 * * [simplify]: iteration 4: (544 enodes) 7.703 * * [simplify]: Extracting #0: cost 6 inf + 0 7.703 * * [simplify]: Extracting #1: cost 120 inf + 0 7.705 * * [simplify]: Extracting #2: cost 381 inf + 724 7.717 * * [simplify]: Extracting #3: cost 513 inf + 137920 7.769 * * [simplify]: Extracting #4: cost 367 inf + 890858 7.848 * * [simplify]: Extracting #5: cost 188 inf + 1426435 7.963 * * [simplify]: Extracting #6: cost 9 inf + 1776574 8.083 * * [simplify]: Extracting #7: cost 0 inf + 1799609 8.195 * [simplify]: Simplified to: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) (+.p16 (*.p16 (*.p16 a c) (real->posit16 4)) (*.p16 (+.p16 (neg.p16 b) (neg.p16 b)) (+.p16 (neg.p16 b) b))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4)))) b) (*.p16 a (real->posit16 4)) (*.p16 (real->posit16 2) a) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (real->posit16 2)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (real->posit16 2)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (real->posit16 2)) (/.p16 (-.p16 (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 a c) (real->posit16 4))))) b) (real->posit16 2)) 8.196 * * * [progress]: adding candidates to table 8.603 * * [progress]: iteration 3 / 4 8.603 * * * [progress]: picking best candidate 8.772 * * * * [pick]: Picked #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 8.772 * * * [progress]: localizing error 9.029 * * * [progress]: generating rewritten candidates 9.029 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1) 9.033 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 2) 9.033 * * * * [progress]: [ 3 / 4 ] rewriting at (2) 9.049 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 2 1) 9.057 * * * [progress]: generating series expansions 9.057 * * * * [progress]: [ 1 / 4 ] generating series at (2 1) 9.057 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 2) 9.057 * * * * [progress]: [ 3 / 4 ] generating series at (2) 9.057 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 2 1) 9.057 * * * [progress]: simplifying candidates 9.057 * * * * [progress]: [ 1 / 10 ] simplifiying candidate #posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 9.057 * * * * [progress]: [ 2 / 10 ] simplifiying candidate #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 9.058 * * * * [progress]: [ 3 / 10 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 9.058 * * * * [progress]: [ 4 / 10 ] simplifiying candidate #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))))))> 9.058 * * * * [progress]: [ 5 / 10 ] simplifiying candidate #posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 9.058 * * * * [progress]: [ 6 / 10 ] simplifiying candidate #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> 9.058 * * * * [progress]: [ 7 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 9.058 * * * * [progress]: [ 8 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 9.059 * * * * [progress]: [ 9 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 9.059 * * * * [progress]: [ 10 / 10 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> 9.059 * [simplify]: Simplifying: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (real->posit16 2)) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c)) (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)) (*.p16 (real->posit16 4) a) (*.p16 (real->posit16 4) a) (*.p16 (real->posit16 4) a) (*.p16 (real->posit16 4) a) 9.059 * * [simplify]: iteration 1: (27 enodes) 9.070 * * [simplify]: iteration 2: (79 enodes) 9.097 * * [simplify]: iteration 3: (228 enodes) 9.201 * * [simplify]: iteration 4: (879 enodes) 10.015 * * [simplify]: Extracting #0: cost 9 inf + 0 10.016 * * [simplify]: Extracting #1: cost 217 inf + 0 10.018 * * [simplify]: Extracting #2: cost 832 inf + 2648 10.024 * * [simplify]: Extracting #3: cost 1352 inf + 31536 10.081 * * [simplify]: Extracting #4: cost 1380 inf + 777244 10.255 * * [simplify]: Extracting #5: cost 343 inf + 3072300 10.538 * * [simplify]: Extracting #6: cost 1 inf + 3942130 10.810 * * [simplify]: Extracting #7: cost 0 inf + 3945614 11.101 * [simplify]: Simplified to: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (/.p16 (-.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (real->posit16 2)) (*.p16 (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 (real->posit16 2) a)) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))) (*.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))) (+.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 b b))) (+.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 b b)) (*.p16 a (real->posit16 4)) (*.p16 a (real->posit16 4)) (*.p16 a (real->posit16 4)) (*.p16 a (real->posit16 4)) 11.102 * * * [progress]: adding candidates to table 11.531 * * [progress]: iteration 4 / 4 11.531 * * * [progress]: picking best candidate 11.678 * * * * [pick]: Picked #posit16 4) a) c)))) (real->posit16 2)) a))> 11.679 * * * [progress]: localizing error 11.890 * * * [progress]: generating rewritten candidates 11.890 * * * * [progress]: [ 1 / 4 ] rewriting at (2 1 1) 11.891 * * * * [progress]: [ 2 / 4 ] rewriting at (2 1 1 2) 11.892 * * * * [progress]: [ 3 / 4 ] rewriting at (2) 11.895 * * * * [progress]: [ 4 / 4 ] rewriting at (2 1 1 2 1) 11.905 * * * [progress]: generating series expansions 11.905 * * * * [progress]: [ 1 / 4 ] generating series at (2 1 1) 11.905 * * * * [progress]: [ 2 / 4 ] generating series at (2 1 1 2) 11.905 * * * * [progress]: [ 3 / 4 ] generating series at (2) 11.906 * * * * [progress]: [ 4 / 4 ] generating series at (2 1 1 2 1) 11.906 * * * [progress]: simplifying candidates 11.906 * * * * [progress]: [ 1 / 9 ] simplifiying candidate #posit16 4) a) c))))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 2 / 9 ] simplifiying candidate #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 3 / 9 ] simplifiying candidate #posit16 4) a) c)))) (*.p16 a (real->posit16 2))))> 11.906 * * * * [progress]: [ 4 / 9 ] simplifiying candidate #posit16 4) a) c))))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 5 / 9 ] simplifiying candidate #posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 6 / 9 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 7 / 9 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 8 / 9 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 11.906 * * * * [progress]: [ 9 / 9 ] simplifiying candidate #posit16 4) a) c)))) (real->posit16 2)) a))> 11.906 * [simplify]: Simplifying: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (-.p16 (*.p16 (neg.p16 b) (neg.p16 b)) (*.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)))) (*.p16 a (real->posit16 2)) (neg.p16 (*.p16 (*.p16 (real->posit16 4) a) c)) (-.p16 (*.p16 (*.p16 b b) (*.p16 b b)) (*.p16 (*.p16 (*.p16 (real->posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c)) (*.p16 (real->posit16 4) a) (*.p16 (real->posit16 4) a) (*.p16 (real->posit16 4) a) (*.p16 (real->posit16 4) a) 11.906 * * [simplify]: iteration 1: (24 enodes) 11.913 * * [simplify]: iteration 2: (66 enodes) 11.924 * * [simplify]: iteration 3: (179 enodes) 11.971 * * [simplify]: iteration 4: (757 enodes) 12.698 * * [simplify]: Extracting #0: cost 8 inf + 0 12.698 * * [simplify]: Extracting #1: cost 131 inf + 0 12.702 * * [simplify]: Extracting #2: cost 632 inf + 964 12.731 * * [simplify]: Extracting #3: cost 958 inf + 200910 12.797 * * [simplify]: Extracting #4: cost 816 inf + 1443808 13.099 * * [simplify]: Extracting #5: cost 53 inf + 3223896 13.387 * * [simplify]: Extracting #6: cost 0 inf + 3347926 13.734 * * [simplify]: Extracting #7: cost 0 inf + 3347767 14.056 * [simplify]: Simplified to: (neg.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))))) (+.p16 (*.p16 (+.p16 (neg.p16 b) b) (+.p16 (neg.p16 b) (neg.p16 b))) (*.p16 c (*.p16 a (real->posit16 4)))) (-.p16 (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4))))) b) (*.p16 a (real->posit16 2)) (neg.p16 (*.p16 c (*.p16 a (real->posit16 4)))) (*.p16 (-.p16 (*.p16 b b) (*.p16 c (*.p16 a (real->posit16 4)))) (+.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 b b))) (+.p16 (*.p16 c (*.p16 a (real->posit16 4))) (*.p16 b b)) (*.p16 a (real->posit16 4)) (*.p16 a (real->posit16 4)) (*.p16 a (real->posit16 4)) (*.p16 a (real->posit16 4)) 14.057 * * * [progress]: adding candidates to table 14.642 * [progress]: [Phase 3 of 3] Extracting. 14.642 * * [regime]: Finding splitpoints for: (#posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>) 14.648 * * * [regime-changes]: Trying 3 branch expressions: (c a b) 14.649 * * * * [regimes]: Trying to branch on c from (#posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>) 14.916 * * * * [regimes]: Trying to branch on a from (#posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>) 15.119 * * * * [regimes]: Trying to branch on b from (#posit16 4) a) c) (*.p16 (*.p16 (real->posit16 4) a) c))) (+.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (real->posit16 2)) a))> #posit16 4) a) c)))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (real->posit16 2)) a))> #posit16 4) a) c))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (*.p16 (real->posit16 4) a) c))))) (*.p16 (real->posit16 2) a)))> #posit16 4) (*.p16 a c))))) (real->posit16 2)) a))> #posit16 4) (*.p16 a c)))) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c)))))) (*.p16 (*.p16 (real->posit16 2) a) (+.p16 (neg.p16 b) (sqrt.p16 (-.p16 (*.p16 b b) (*.p16 (real->posit16 4) (*.p16 a c))))))))>) 15.407 * * * [regime]: Found split indices: #