Falkner and Boettcher, Appendix B, 1

Time bar (total: 6.7s)

analyze420.0ms (6.3%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%100%0%0%0%0%0
0%0%100%0%0%0%0%1
0%0%100%0%0%0%0%2
0%0%100%0%0%0%0%3
0%0%100%0%0%0%0%4
0%0%100%0%0%0%0%5
0%0%100%0%0%0%0%6
0%0%100%0%0%0%0%7
0%0%100%0%0%0%0%8
0%0%100%0%0%0%0%9
0%0%100%0%0%0%0%10
0%0%100%0%0%0%0%11
0%0%100%0%0%0%0%12
Compiler

Compiled 16 to 10 computations (37.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 220.0ms
ival-mult: 88.0ms (40% of total)
ival-acos: 49.0ms (22.3% of total)
ival-sub: 47.0ms (21.3% of total)
ival-div: 30.0ms (13.6% of total)
const: 5.0ms (2.3% of total)
backward-pass: 2.0ms (0.9% of total)

sample4.5s (67.8%)

Results
709.0ms8156×0invalid
1.5s3576×3valid
843.0ms2217×1valid
774.0ms2109×2valid
33.0ms354×0valid
Precisions
Click to see histograms. Total time spent on operations: 2.5s
ival-acos: 636.0ms (25.1% of total)
ival-mult: 571.0ms (22.6% of total)
ival-sub: 459.0ms (18.1% of total)
ival-div: 422.0ms (16.7% of total)
backward-pass: 388.0ms (15.3% of total)
const: 55.0ms (2.2% of total)
Bogosity

preprocess454.0ms (6.8%)

Algorithm
egg-herbie
Rules
8668×accelerator-lowering-fma.f32
8668×accelerator-lowering-fma.f64
2288×*-lowering-*.f32
2288×*-lowering-*.f64
2162×--lowering--.f32
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01743
15843
217143
362043
4245843
5447743
6533043
7628143
8728443
9789443
0914
12914
27414
320014
457514
5123214
6248814
7385814
8567614
9733014
10788514
0809912
Stop Event
iter limit
node limit
node limit
Calls
Call 1
Inputs
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))
Outputs
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (+.f64 (*.f64 v v) #s(literal -1 binary64))))
Call 2
Inputs
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))
(acos (/ (- 1 (* 5 (* (neg v) (neg v)))) (- (* (neg v) (neg v)) 1)))
(neg (acos (/ (- 1 (* 5 (* (neg v) (neg v)))) (- (* (neg v) (neg v)) 1))))
Outputs
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))
(acos (/ (+ 1 (* v (* v -5))) (+ (* v v) -1)))
(acos (/ (- 1 (* 5 (* (neg v) (neg v)))) (- (* (neg v) (neg v)) 1)))
(acos (/ (+ 1 (* v (* v -5))) (+ (* v v) -1)))
(neg (acos (/ (- 1 (* 5 (* (neg v) (neg v)))) (- (* (neg v) (neg v)) 1))))
(neg (acos (/ (+ 1 (* v (* v -5))) (+ (* v v) -1))))
Symmetry

(abs v)

explain321.0ms (4.8%)

FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
14241(1.1174602031076003e-199)0-(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
00-0-(-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v)))
00-0-(-.f64 (*.f64 v v) #s(literal 1 binary64))
00-0-v
00-0-(/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64)))
00-0-(*.f64 v v)
00-0-#s(literal 5 binary64)
00-0-#s(literal 1 binary64)
01(7.187202868780392e-163)0-(*.f64 #s(literal 5 binary64) (*.f64 v v))
Results
186.0ms228×3valid
31.0ms142×1valid
41.0ms122×2valid
2.0ms20×0valid
Compiler

Compiled 119 to 29 computations (75.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 183.0ms
ival-mult: 86.0ms (47% of total)
backward-pass: 30.0ms (16.4% of total)
ival-acos: 29.0ms (15.8% of total)
ival-sub: 18.0ms (9.8% of total)
ival-div: 17.0ms (9.3% of total)
const: 3.0ms (1.6% of total)

eval0.0ms (0%)

Compiler

Compiled 15 to 10 computations (33.3% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
98.8%
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
Compiler

Compiled 15 to 9 computations (40% saved)

localize492.0ms (7.4%)

Algorithm
egg-herbie
Localize:

Found 8 expressions of interest:

NewMetricScoreProgram
cost-diff0
#s(literal 1 binary64)
cost-diff0
(-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v)))
cost-diff0
(/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64)))
cost-diff0
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
accuracy100.0%
(*.f64 v v)
accuracy100.0%
(/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64)))
accuracy99.7%
(*.f64 #s(literal 5 binary64) (*.f64 v v))
accuracy98.8%
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
Rules
8668×accelerator-lowering-fma.f32
8668×accelerator-lowering-fma.f64
2288×*-lowering-*.f32
2288×*-lowering-*.f64
2162×--lowering--.f32
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0950
12950
27450
320050
457550
5123250
6248850
7385850
8567650
9733050
10788550
0809944
Stop Event
iter limit
node limit
Calls
Call 1
Inputs
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))
(/ (- 1 (* 5 (* v v))) (- (* v v) 1))
(- 1 (* 5 (* v v)))
1
(* 5 (* v v))
5
(* v v)
v
(- (* v v) 1)
Outputs
(acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (+.f64 (*.f64 v v) #s(literal -1 binary64))))
(/ (- 1 (* 5 (* v v))) (- (* v v) 1))
(/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (+.f64 (*.f64 v v) #s(literal -1 binary64)))
(- 1 (* 5 (* v v)))
(+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64)))
1
#s(literal 1 binary64)
(* 5 (* v v))
(*.f64 #s(literal 5 binary64) (*.f64 v v))
5
#s(literal 5 binary64)
(* v v)
(*.f64 v v)
v
(- (* v v) 1)
(+.f64 (*.f64 v v) #s(literal -1 binary64))
Results
70.0ms114×3valid
15.0ms71×1valid
23.0ms61×2valid
1.0ms10×0valid
Compiler

Compiled 52 to 10 computations (80.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 59.0ms
backward-pass: 14.0ms (23.7% of total)
ival-acos: 14.0ms (23.7% of total)
ival-mult: 12.0ms (20.3% of total)
ival-div: 10.0ms (16.9% of total)
ival-sub: 9.0ms (15.2% of total)
const: 1.0ms (1.7% of total)

series8.0ms (0.1%)

Counts
6 → 60
Calls
Call 1
Inputs
#<alt (acos (/ (- 1 (* 5 (* v v))) (- (* v v) 1)))>
#<alt (* 5 (* v v))>
#<alt (/ (- 1 (* 5 (* v v))) (- (* v v) 1))>
#<alt (* v v)>
#<alt (- 1 (* 5 (* v v)))>
#<alt 1>
Outputs
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (acos (/ (- 1 (* 5 (pow v 2))) (- (pow v 2) 1)))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt (* 5 (pow v 2))>
#<alt -1>
#<alt (- (* 4 (pow v 2)) 1)>
#<alt (- (* (pow v 2) (+ 4 (* 4 (pow v 2)))) 1)>
#<alt (- (* (pow v 2) (+ 4 (* (pow v 2) (+ 4 (* 4 (pow v 2)))))) 1)>
#<alt -5>
#<alt (* -1 (+ 5 (* 4 (/ 1 (pow v 2)))))>
#<alt (- (* -1 (/ (+ 4 (* 4 (/ 1 (pow v 2)))) (pow v 2))) 5)>
#<alt (- (* -1 (/ (+ 4 (* 4 (/ 1 (pow v 2)))) (pow v 4))) (+ 5 (* 4 (/ 1 (pow v 2)))))>
#<alt -5>
#<alt (* -1 (+ 5 (* 4 (/ 1 (pow v 2)))))>
#<alt (- (* -1 (/ (+ 4 (* 4 (/ 1 (pow v 2)))) (pow v 2))) 5)>
#<alt (- (* -1 (/ (+ 4 (* 4 (/ 1 (pow v 2)))) (pow v 4))) (+ 5 (* 4 (/ 1 (pow v 2)))))>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt (pow v 2)>
#<alt 1>
#<alt (+ 1 (* -5 (pow v 2)))>
#<alt (+ 1 (* -5 (pow v 2)))>
#<alt (+ 1 (* -5 (pow v 2)))>
#<alt (* -5 (pow v 2))>
#<alt (* (pow v 2) (- (/ 1 (pow v 2)) 5))>
#<alt (* (pow v 2) (- (/ 1 (pow v 2)) 5))>
#<alt (* (pow v 2) (- (/ 1 (pow v 2)) 5))>
#<alt (* -5 (pow v 2))>
#<alt (* (pow v 2) (- (/ 1 (pow v 2)) 5))>
#<alt (* (pow v 2) (- (/ 1 (pow v 2)) 5))>
#<alt (* (pow v 2) (- (/ 1 (pow v 2)) 5))>
Calls

15 calls:

TimeVariablePointExpression
0.0ms
v
@0
(* 5 (* v v))
0.0ms
v
@inf
(* 5 (* v v))
0.0ms
v
@inf
(/ (- 1 (* 5 (* v v))) (- (* v v) 1))
0.0ms
v
@-inf
(/ (- 1 (* 5 (* v v))) (- (* v v) 1))
0.0ms
v
@inf
(* v v)

rewrite457.0ms (6.8%)

Algorithm
batch-egg-rewrite
Rules
4946×accelerator-lowering-fma.f32
4946×accelerator-lowering-fma.f64
4582×*-lowering-*.f32
4582×*-lowering-*.f64
3506×/-lowering-/.f32
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0943
16443
252443
3681643
0816438
Stop Event
iter limit
node limit

end0.0ms (0%)

Profiling

Loading profile data...