Details

Time bar (total: 1.2s)

analyze52.0ms (4.4%)

Algorithm
1×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
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
0%0%99.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
56.3%56.2%43.7%0.1%0%0%0%7
65.6%65.6%34.3%0.1%0%0%0%8
76.6%76.5%23.4%0.1%0%0%0%9
82%82%18%0.1%0%0%0%10
87.9%87.8%12.1%0.1%0%0%0%11
90.8%90.7%9.2%0.1%0%0%0%12
Compiler

Compiled 9 to 7 computations (22.2% saved)

sample992.0ms (85.2%)

Results
980.0ms8256×body256valid
Bogosity

preprocess53.0ms (4.5%)

Algorithm
2×egg-herbie
Rules
36×fma-neg_binary64
16×sub-neg_binary64
16×fma-def_binary64
14×cancel-sign-sub-inv_binary64
12×associate--r+_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01018
11418
22218
33418
46418
512918
616318
720718
822218
922518
1022718
022
122
Stop Event
1×unsound
1×saturated
Calls
Call 1
Inputs
0
1
Outputs
0
1
0
Call 2
Inputs
(/.f64 (fabs.f64 (-.f64 a b)) 2)
(/.f64 (fabs.f64 (-.f64 b a)) 2)
Outputs
(/.f64 (fabs.f64 (-.f64 a b)) 2)
(*.f64 1/2 (fabs.f64 (-.f64 a b)))
(*.f64 (fabs.f64 (-.f64 a b)) 1/2)
(/.f64 (fabs.f64 (-.f64 b a)) 2)
(/.f64 (fabs.f64 (-.f64 a b)) 2)
(*.f64 1/2 (fabs.f64 (-.f64 a b)))
(*.f64 (fabs.f64 (-.f64 a b)) 1/2)
Symmetry

(sort a b)

Compiler

Compiled 10 to 8 computations (20% saved)

simplify11.0ms (0.9%)

Algorithm
1×egg-herbie
Rules
39×fma-neg_binary64
17×fma-def_binary64
16×cancel-sign-sub-inv_binary64
16×sub-neg_binary64
9×fabs-sub_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
079
1119
2189
3279
4489
51049
61579
71989
82289
92369
102389
Stop Event
1×saturated
Counts
1 → 2
Calls
Call 1
Inputs
(/.f64 (fabs.f64 (-.f64 a b)) 2)
Outputs
(/.f64 (fabs.f64 (-.f64 a b)) 2)
(*.f64 1/2 (fabs.f64 (-.f64 a b)))
(*.f64 (fabs.f64 (-.f64 a b)) 1/2)

eval1.0ms (0.1%)

Compiler

Compiled 14 to 8 computations (42.9% saved)

prune1.0ms (0.1%)

Pruning

2 alts after pruning (2 fresh and 0 done)

PrunedKeptTotal
New112
Fresh011
Picked000
Done000
Total123
Error
0b
Counts
3 → 1
Alt Table
Click to see full alt table
StatusErrorProgram
▶0b
(/.f64 (fabs.f64 (-.f64 a b)) 2)
Compiler

Compiled 8 to 6 computations (25% saved)

localize11.0ms (0.9%)

Compiler

Compiled 18 to 7 computations (61.1% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune1.0ms (0.1%)

Pruning

1 alts after pruning (0 fresh and 1 done)

PrunedKeptTotal
New000
Fresh000
Picked011
Done000
Total011
Error
0b
Counts
1 → 1
Alt Table
Click to see full alt table
StatusErrorProgram
✓0b
(/.f64 (fabs.f64 (-.f64 a b)) 2)
Compiler

Compiled 16 to 12 computations (25% saved)

simplify2.0ms (0.2%)

Algorithm
1×egg-herbie
Rules
4×+-commutative_binary64
4×sub-neg_binary64
2×*-commutative_binary64
2×neg-sub0_binary64
2×neg-mul-1_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
079
1119
2189
3239
4269
5279
Stop Event
1×done
1×saturated
Calls
Call 1
Inputs
(/.f64 (fabs.f64 (-.f64 a b)) 2)
Outputs
(/.f64 (fabs.f64 (-.f64 a b)) 2)
Compiler

Compiled 8 to 6 computations (25% saved)

soundness0.0ms (0%)

end40.0ms (3.5%)

Remove

(sort a b)

Compiler

Compiled 24 to 18 computations (25% saved)

Profiling

Loading profile data...