fabs fraction 2

Time bar (total: 8.5s)

analyze1.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
100%99.9%0%0.1%0%0%0%1
Compiler

Compiled 9 to 7 computations (22.2% saved)

sample8.4s (98.4%)

Results
908.0ms8256×0valid
687.0ms8244×0valid-sollya
7.0ms12×0exit-sollya
Sollya Eval
PtRival-outSollya-intervalSollya-pointstatusSollya statusRival itersollya-timecheck
(4.330359131633256e-75 4.01509309169762e-50)2.00754654584881e-50(+nan.0 +nan.0)+nan.0validexit05.0#f
(-1.7829026233590696e-129 -5.958615164386604e+234)2.979307582193302e+234(2.979307582193302e+234 2.979307582193302e+234)+nan.0validexit00.181175#f
(6.619950579594659e+57 -4.484415297937575e-164)3.309975289797329e+57(3.309975289797329e+57 3.309975289797329e+57)+nan.0validexit00.19981#f
(-3.5192780946456506e+80 3.206240488879828e-100)1.7596390473228253e+80(1.7596390473228253e+80 1.7596390473228253e+80)+nan.0validexit00.11003#f
(-3.968204157088655e-35 -8186724.424100681)4093362.2120503406(4093362.2120503406 4093362.2120503406)+nan.0validexit00.19274#f
(2.0018848130172753e+94 4.0223797952126534e+136)2.0111898976063267e+136(2.0111898976063267e+136 2.0111898976063267e+136)+nan.0validexit00.113919#f
(-9.646754018633252e+23 1.2072388724265706e+211)6.036194362132853e+210(6.036194362132853e+210 6.036194362132853e+210)+nan.0validexit00.10148900000000001#f
(8.28028386672832e+185 2.089671751101601e-98)4.14014193336416e+185(4.14014193336416e+185 4.14014193336416e+185)+nan.0validexit00.16926#f
(5.679221937611446e-235 1.0954517693502176e-38)5.477258846751088e-39(5.477258846751088e-39 5.477258846751088e-39)+nan.0validexit00.152595#f
(-9.590033632363496e-67 -2.4986363936890578e-71)4.7948918843620636e-67(4.7948918843620636e-67 4.7948918843620636e-67)+nan.0validexit00.187802#f
(-1.4911878173393215e+254 -1.1193069378787425e-101)7.455939086696607e+253(7.455939086696607e+253 7.455939086696607e+253)+nan.0validexit00.21957100000000002#f
(1.1455346769192834e-224 -5.373492856834809e-206)2.6867464284174043e-206(2.6867464284174043e-206 2.6867464284174043e-206)+nan.0validexit00.114436#f
Sollya timings
Total time spent in Sollya 694.0ms
Bogosity

preprocess75.0ms (0.9%)

Algorithm
egg-herbie
Rules
68×fma-neg
24×sub-neg
22×fma-define
14×*-commutative
13×distribute-lft-neg-in
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
025177
152161
298161
3189161
4266161
5318161
6346161
7358161
8359161
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 a (neg.f64 b))) #s(literal 2 binary64))
(neg.f64 (/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal 2 binary64)))
(neg.f64 (/.f64 (fabs.f64 (-.f64 a (neg.f64 b))) #s(literal 2 binary64)))
(/.f64 (fabs.f64 (-.f64 b a)) #s(literal 2 binary64))
Outputs
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 b a)) #s(literal 2 binary64))
(*.f64 (fabs.f64 (-.f64 b a)) #s(literal 1/2 binary64))
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 b a)) #s(literal 2 binary64))
(*.f64 (fabs.f64 (-.f64 b a)) #s(literal 1/2 binary64))
(/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (+.f64 a b)) #s(literal 2 binary64))
(*.f64 (fabs.f64 (+.f64 a b)) #s(literal 1/2 binary64))
(/.f64 (fabs.f64 (-.f64 a (neg.f64 b))) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (+.f64 a b)) #s(literal 2 binary64))
(*.f64 (fabs.f64 (+.f64 a b)) #s(literal 1/2 binary64))
(neg.f64 (/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal 2 binary64)))
(/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal -2 binary64))
(/.f64 (fabs.f64 (+.f64 a b)) #s(literal -2 binary64))
(*.f64 (fabs.f64 (+.f64 a b)) #s(literal -1/2 binary64))
(neg.f64 (/.f64 (fabs.f64 (-.f64 a (neg.f64 b))) #s(literal 2 binary64)))
(/.f64 (fabs.f64 (-.f64 (neg.f64 a) b)) #s(literal -2 binary64))
(/.f64 (fabs.f64 (+.f64 a b)) #s(literal -2 binary64))
(*.f64 (fabs.f64 (+.f64 a b)) #s(literal -1/2 binary64))
(/.f64 (fabs.f64 (-.f64 b a)) #s(literal 2 binary64))
(*.f64 (fabs.f64 (-.f64 b a)) #s(literal 1/2 binary64))
Symmetry

(sort a b)

Compiler

Compiled 8 to 6 computations (25% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune14.0ms (0.2%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
100.0%
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
Compiler

Compiled 16 to 12 computations (25% saved)

simplify3.0ms (0%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01223
11623
22323
32823
43123
53223
Stop Event
saturated
Calls
Call 1
Inputs
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
Outputs
(/.f64 (fabs.f64 (-.f64 a b)) #s(literal 2 binary64))
(/.f64 (fabs.f64 (-.f64 b a)) #s(literal 2 binary64))

soundness1.0ms (0%)

Stop Event
fuel
Compiler

Compiled 8 to 6 computations (25% saved)

preprocess40.0ms (0.5%)

Remove

(sort a b)

Compiler

Compiled 64 to 48 computations (25% saved)

end0.0ms (0%)

Profiling

Loading profile data...