Details

Time bar (total: 2.1s)

analyze107.0ms (5%)

Algorithm
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 10 to 7 computations (30% saved)

sample1.2s (54.1%)

Results
1.1s8256×body256valid
Bogosity

preprocess188.0ms (8.8%)

Algorithm
egg-herbie
Rules
2830×fma-def_binary64
1127×fma-neg_binary64
286×associate--r-_binary64
276×distribute-rgt-out--_binary64
273×+-commutative_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01020
12020
24020
37420
415720
532620
664914
7134014
8284514
9341614
10349814
11351214
12351214
13487214
14546414
15566814
16572514
17578114
18578114
19580014
20580414
022
122
Stop Event
unsound
node limit
Calls
Call 1
Inputs
0
1
Outputs
0
1
0
Call 2
Inputs
(+.f64 x (/.f64 (-.f64 y x) 2))
(+.f64 y (/.f64 (-.f64 x y) 2))
Outputs
(+.f64 x (/.f64 (-.f64 y x) 2))
(*.f64 1/2 (+.f64 y x))
(*.f64 1/2 (+.f64 x y))
(+.f64 y (/.f64 (-.f64 x y) 2))
(+.f64 x (/.f64 (-.f64 y x) 2))
(*.f64 1/2 (+.f64 y x))
(*.f64 1/2 (+.f64 x y))
Symmetry

(sort x y)

Compiler

Compiled 11 to 8 computations (27.3% saved)

simplify179.0ms (8.4%)

Algorithm
egg-herbie
Rules
1251×fma-neg_binary64
737×distribute-rgt-in_binary64
446×distribute-lft-in_binary64
362×associate--r-_binary64
300×fma-def_binary64
Iterations

Useful iterations: 8 (0.0ms)

IterNodesCost
0710
11310
22410
34210
48810
516410
63688
76088
89167
921467
1034147
1138567
1238747
1338887
1438887
1552617
1656777
1758337
1859047
1959977
2066117
Stop Event
node limit
Counts
1 → 2
Calls
Call 1
Inputs
(+.f64 x (/.f64 (-.f64 y x) 2))
Outputs
(+.f64 x (/.f64 (-.f64 y x) 2))
(fma.f64 x 1/2 (/.f64 y 2))
(fma.f64 x 1/2 (*.f64 1/2 y))
(*.f64 1/2 (+.f64 x y))

eval1.0ms (0%)

Compiler

Compiled 14 to 9 computations (35.7% saved)

prune1.0ms (0.1%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New112
Fresh101
Picked000
Done000
Total213
Error
0b
Counts
3 → 1
Alt Table
Click to see full alt table
StatusErrorProgram
0b
(*.f64 1/2 (+.f64 x y))
Compiler

Compiled 7 to 5 computations (28.6% saved)

localize6.0ms (0.3%)

Compiler

Compiled 13 to 6 computations (53.8% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune1.0ms (0%)

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 1/2 (+.f64 x y))
Compiler

Compiled 7 to 5 computations (28.6% saved)

regimes10.0ms (0.5%)

Accuracy

Total -0.0b remaining (-∞%)

Threshold costs -0.0b (-∞%)

Counts
2 → 1
Calls
Call 1
Inputs
(*.f64 1/2 (+.f64 x y))
(+.f64 x (/.f64 (-.f64 y x) 2))
Outputs
(*.f64 1/2 (+.f64 x y))
Calls

3 calls:

3.0ms
(+.f64 x (/.f64 (-.f64 y x) 2))
3.0ms
y
3.0ms
x
Results
ErrorSegmentsBranch
0b1x
0b1y
0b1(+.f64 x (/.f64 (-.f64 y x) 2))
Compiler

Compiled 29 to 19 computations (34.5% saved)

simplify5.0ms (0.2%)

Algorithm
egg-herbie
Rules
+-commutative_binary64
*-commutative_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
067
187
Stop Event
done
saturated
Calls
Call 1
Inputs
(*.f64 1/2 (+.f64 x y))
Outputs
(*.f64 1/2 (+.f64 x y))
Compiler

Compiled 7 to 5 computations (28.6% saved)

soundness469.0ms (21.9%)

Algorithm
egg-herbie
Rules
1251×fma-neg_binary64
737×distribute-rgt-in_binary64
446×distribute-lft-in_binary64
362×associate--r-_binary64
300×fma-def_binary64
Iterations

Useful iterations: 8 (0.0ms)

IterNodesCost
0710
11310
22410
34210
48810
516410
63688
76088
89167
921467
1034147
1138567
1238747
1338887
1438887
1552617
1656777
1758337
1859047
1959977
2066117
Stop Event
node limit
Compiler

Compiled 270 to 219 computations (18.9% saved)

end15.0ms (0.7%)

Remove

(sort x y)

Compiler

Compiled 21 to 15 computations (28.6% saved)

Profiling

Loading profile data...