sqrt( (z - za)^2 + ( sqrt((x)^2 + (y)^2) - ra)^2 );

Time bar (total: 2.2s)

analyze1.0ms (0%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%3.6%96.4%0%0%0%0
100%3.6%0%96.4%0%0%0%1
Compiler

Compiled 63 to 48 computations (23.8% saved)

sample1.9s (84.8%)

Results
1.9s8251×body256valid
2.0msbody512valid
1.0msbody1024valid
Bogosity

preprocess79.0ms (3.5%)

Algorithm
egg-herbie
Rules
1942×unsub-neg
1042×associate-+l+
740×*-commutative
514×neg-sub0
502×neg-mul-1
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
0119924
1272408
2867400
32741400
46461400
Stop Event
node limit
Calls
Call 1
Inputs
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 (neg.f64 z) za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z (neg.f64 za)) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 (neg.f64 x) 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 (neg.f64 y) 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) (neg.f64 ra)) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 za z) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 x za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 z 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 y za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 z 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 ra za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) z) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z x) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 za 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z y) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 za 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z ra) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) za) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 y 2) (pow.f64 x 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 ra 2) (pow.f64 y 2))) x) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 ra 2))) y) 2)))
Outputs
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 (neg.f64 z) za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2) (pow.f64 (-.f64 (neg.f64 z) za) 2)))
(hypot.f64 (-.f64 (hypot.f64 x y) ra) (-.f64 (neg.f64 z) za))
(hypot.f64 (-.f64 (hypot.f64 x y) ra) (+.f64 z za))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z (neg.f64 za)) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2) (pow.f64 (-.f64 (neg.f64 z) za) 2)))
(hypot.f64 (-.f64 (hypot.f64 x y) ra) (-.f64 (neg.f64 z) za))
(hypot.f64 (-.f64 (hypot.f64 x y) ra) (+.f64 z za))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 (neg.f64 x) 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 (neg.f64 y) 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) (neg.f64 ra)) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) (neg.f64 ra)) 2)))
(hypot.f64 (-.f64 z za) (+.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 za z) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 x za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 z 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 x za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 y y) (*.f64 z z))) ra) 2)))
(hypot.f64 (-.f64 x za) (-.f64 (hypot.f64 z y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 y za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 z 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 y za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 z z))) ra) 2)))
(hypot.f64 (-.f64 y za) (-.f64 (hypot.f64 z x) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 ra za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) z) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 ra za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) z) 2)))
(hypot.f64 (-.f64 ra za) (-.f64 (hypot.f64 x y) z))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z x) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 za 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z x) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 y y) (*.f64 za za))) ra) 2)))
(hypot.f64 (-.f64 z x) (-.f64 (hypot.f64 za y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z y) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 za 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z y) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 za za))) ra) 2)))
(hypot.f64 (-.f64 z y) (-.f64 (hypot.f64 za x) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z ra) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) za) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z ra) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) za) 2)))
(hypot.f64 (-.f64 z ra) (-.f64 (hypot.f64 x y) za))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 y 2) (pow.f64 x 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 ra 2) (pow.f64 y 2))) x) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 y y) (*.f64 ra ra))) x) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 y ra) x))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 ra 2))) y) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 ra ra))) y) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x ra) y))
Symmetry

(abs x)

(abs y)

(sort z za)

(sort x y)

Compiler

Compiled 29 to 24 computations (17.2% saved)

simplify40.0ms (1.8%)

Algorithm
egg-herbie
Rules
1388×unsub-neg
1372×associate-+l-
1220×fma-def
840×fma-neg
828×associate-+r-
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
01957
13925
29625
323025
475025
5343225
Stop Event
node limit
Counts
1 → 3
Calls
Call 1
Inputs
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
Outputs
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 y y))) ra) 2)))
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))

eval1.0ms (0.1%)

Compiler

Compiled 52 to 33 computations (36.5% saved)

prune2.0ms (0.1%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New213
Fresh101
Picked000
Done000
Total314
Accurracy
100.0%
Counts
4 → 1
Alt Table
Click to see full alt table
StatusAccuracyProgram
100.0%
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
100.0%
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
Compiler

Compiled 28 to 18 computations (35.7% saved)

localize43.0ms (1.9%)

Compiler

Compiled 31 to 10 computations (67.7% saved)

eval0.0ms (0%)

Compiler

Compiled 5 to 5 computations (0% saved)

prune2.0ms (0.1%)

Pruning

1 alts after pruning (0 fresh and 1 done)

PrunedKeptTotal
New000
Fresh000
Picked011
Done000
Total011
Accurracy
100.0%
Counts
1 → 1
Alt Table
Click to see full alt table
StatusAccuracyProgram
100.0%
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
Compiler

Compiled 47 to 31 computations (34% saved)

regimes41.0ms (1.8%)

Accuracy

Total -1.7b remaining (-∞%)

Threshold costs -1.7b (-∞%)

Counts
2 → 1
Calls
Call 1
Inputs
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
Outputs
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
Calls

15 calls:

3.0ms
(+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2))
3.0ms
(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
3.0ms
(pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)
3.0ms
(-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra)
3.0ms
ra
Results
AccuracySegmentsBranch
100.0%1z
100.0%1za
100.0%1x
100.0%1y
100.0%1ra
100.0%1(sqrt.f64 (+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)))
100.0%1(+.f64 (pow.f64 (-.f64 z za) 2) (pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2))
100.0%1(pow.f64 (-.f64 z za) 2)
100.0%1(-.f64 z za)
100.0%1(pow.f64 (-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra) 2)
100.0%1(-.f64 (sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2))) ra)
100.0%1(sqrt.f64 (+.f64 (pow.f64 x 2) (pow.f64 y 2)))
100.0%1(+.f64 (pow.f64 x 2) (pow.f64 y 2))
100.0%1(pow.f64 x 2)
100.0%1(pow.f64 y 2)
Compiler

Compiled 201 to 159 computations (20.9% saved)

simplify5.0ms (0.2%)

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

Useful iterations: 0 (0.0ms)

IterNodesCost
01125
11625
22425
32825
43025
Stop Event
done
saturated
Calls
Call 1
Inputs
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
Outputs
(hypot.f64 (-.f64 z za) (-.f64 (hypot.f64 x y) ra))
Compiler

Compiled 14 to 9 computations (35.7% saved)

soundness87.0ms (3.9%)

Rules
1388×unsub-neg
1372×associate-+l-
1220×fma-def
840×fma-neg
828×associate-+r-
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
01957
13925
29625
323025
475025
5343225
Stop Event
node limit
Compiler

Compiled 126 to 71 computations (43.7% saved)

end0.0ms (0%)

preprocess39.0ms (1.7%)

Remove

(sort x y)

(sort z za)

(abs y)

(abs x)

Compiler

Compiled 188 to 128 computations (31.9% saved)

Profiling

Loading profile data...