Details

Time bar (total: 1.3s)

analyze182.0ms (14.4%)

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
0%0%99.9%0.1%0%0%0%5
0%0%99.9%0.1%0%0%0%6
12.5%12.5%87.4%0.1%0%0%0%7
18.8%18.7%81.1%0.1%0%0%0%8
28.1%28.1%71.8%0.1%0%0%0%9
39.7%37.4%56.9%0.1%5.5%0%0%10
46.5%43.7%50.3%0.1%5.9%0%0%11
55.2%51.9%42.1%0.1%5.9%0%0%12
Compiler

Compiled 11 to 8 computations (27.3% saved)

sample981.0ms (77.8%)

Results
918.0ms8256×body256valid
51.0ms612×body256infinite
Bogosity

preprocess51.0ms (4%)

Algorithm
egg-herbie
Rules
563×fma-def_binary64
276×fma-neg_binary64
103×cancel-sign-sub-inv_binary64
94×associate-*r*_binary64
85×associate-*l*_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01640
14840
212232
328532
442932
569032
6128132
7157432
8176932
9180232
10180532
11180532
033
133
Stop Event
unsound
saturated
Calls
Call 1
Inputs
0
1
2
Outputs
0
1
2
1
Call 2
Inputs
(-.f64 x (*.f64 (*.f64 y 4) z))
(-.f64 y (*.f64 (*.f64 x 4) z))
(-.f64 z (*.f64 (*.f64 y 4) x))
(-.f64 x (*.f64 (*.f64 z 4) y))
Outputs
(-.f64 x (*.f64 (*.f64 y 4) z))
(-.f64 x (*.f64 y (*.f64 4 z)))
(+.f64 x (*.f64 y (*.f64 z -4)))
(fma.f64 z (*.f64 y -4) x)
(fma.f64 y (*.f64 z -4) x)
(-.f64 y (*.f64 (*.f64 x 4) z))
(-.f64 y (*.f64 x (*.f64 4 z)))
(+.f64 y (*.f64 x (*.f64 z -4)))
(fma.f64 x (*.f64 z -4) y)
(fma.f64 z (*.f64 x -4) y)
(-.f64 z (*.f64 (*.f64 y 4) x))
(-.f64 z (*.f64 x (*.f64 y 4)))
(+.f64 z (*.f64 x (*.f64 y -4)))
(fma.f64 x (*.f64 y -4) z)
(-.f64 x (*.f64 (*.f64 z 4) y))
(-.f64 x (*.f64 y (*.f64 4 z)))
(+.f64 x (*.f64 y (*.f64 z -4)))
(fma.f64 z (*.f64 y -4) x)
(fma.f64 y (*.f64 z -4) x)
Symmetry

(sort y z)

Compiler

Compiled 13 to 10 computations (23.1% saved)

simplify20.0ms (1.6%)

Algorithm
egg-herbie
Rules
282×fma-def_binary64
110×fma-neg_binary64
57×cancel-sign-sub-inv_binary64
36×distribute-rgt-neg-in_binary64
27×sub-neg_binary64
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
0810
11710
2478
31048
41578
52188
63128
73868
85138
97268
108228
118348
Stop Event
saturated
Counts
1 → 5
Calls
Call 1
Inputs
(-.f64 x (*.f64 (*.f64 y 4) z))
Outputs
(-.f64 x (*.f64 (*.f64 y 4) z))
(-.f64 x (*.f64 y (*.f64 4 z)))
(+.f64 x (*.f64 z (*.f64 y -4)))
(fma.f64 z (*.f64 y -4) x)
(fma.f64 y (*.f64 z -4) x)

eval1.0ms (0.1%)

Compiler

Compiled 36 to 21 computations (41.7% saved)

prune1.0ms (0.1%)

Pruning

2 alts after pruning (2 fresh and 0 done)

PrunedKeptTotal
New415
Fresh011
Picked000
Done000
Total426
Error
0b
Counts
6 → 1
Alt Table
Click to see full alt table
StatusErrorProgram
0b
(-.f64 x (*.f64 (*.f64 y 4) z))
Compiler

Compiled 10 to 7 computations (30% saved)

localize8.0ms (0.6%)

Compiler

Compiled 22 to 13 computations (40.9% saved)

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune2.0ms (0.2%)

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 x (*.f64 (*.f64 y 4) z))
Compiler

Compiled 20 to 14 computations (30% saved)

simplify3.0ms (0.2%)

Algorithm
egg-herbie
Rules
*-commutative_binary64
+-commutative_binary64
sub-neg_binary64
distribute-rgt-neg-in_binary64
neg-sub0_binary64
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0810
11510
23410
34210
44810
55010
Stop Event
done
saturated
Calls
Call 1
Inputs
(-.f64 x (*.f64 (*.f64 y 4) z))
Outputs
(-.f64 x (*.f64 (*.f64 y 4) z))
(+.f64 x (*.f64 z (*.f64 y -4)))
Compiler

Compiled 10 to 7 computations (30% saved)

soundness0.0ms (0%)

end13.0ms (1%)

Remove

(sort y z)

Compiler

Compiled 30 to 21 computations (30% saved)

Profiling

Loading profile data...