Falkner and Boettcher, Appendix B, 1

Time bar (total: 7.6s)

analyze314.0ms (4.1%)

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 32 to 20 computations (37.5% saved)

sample7.1s (93.8%)

Results
769.0ms3831×3valid-sollya
1.2s3831×3valid-rival-baseline
1.1s3831×3valid-rival
270.0ms2212×1valid-rival-baseline
330.0ms2212×1valid-rival
239.0ms2212×1valid-sollya
441.0ms2015×2valid-rival
458.0ms2015×2valid-rival-baseline
305.0ms2015×2valid-sollya
13.0ms198×0valid-sollya
15.0ms198×0valid-rival-baseline
14.0ms198×0valid-rival
Bogosity

preprocess138.0ms (1.8%)

Algorithm
egg-herbie
Rules
586×fma-neg
504×sub-neg
432×fma-define
359×unsub-neg
342×distribute-lft-neg-in
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
022200
169200
2188184
3652184
42521184
55095184
66375184
77330184
Stop Event
node limit
Calls
Call 1
Inputs
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))) (-.f64 (*.f64 (neg.f64 v) (neg.f64 v)) #s(literal 1 binary64))))
(neg.f64 (acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))) (-.f64 (*.f64 (neg.f64 v) (neg.f64 v)) #s(literal 1 binary64)))))
Outputs
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -5 binary64) (*.f64 v v))) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (fma.f64 (*.f64 v v) #s(literal -5 binary64) #s(literal 1 binary64)) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -5 binary64) (*.f64 v v))) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (fma.f64 (*.f64 v v) #s(literal -5 binary64) #s(literal 1 binary64)) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))) (-.f64 (*.f64 (neg.f64 v) (neg.f64 v)) #s(literal 1 binary64))))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -5 binary64) (*.f64 v v))) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (fma.f64 v v #s(literal -1 binary64))))
(acos.f64 (/.f64 (fma.f64 (*.f64 v v) #s(literal -5 binary64) #s(literal 1 binary64)) (fma.f64 v v #s(literal -1 binary64))))
(neg.f64 (acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 (neg.f64 v) (neg.f64 v)))) (-.f64 (*.f64 (neg.f64 v) (neg.f64 v)) #s(literal 1 binary64)))))
(neg.f64 (acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 #s(literal -5 binary64) (*.f64 v v))) (fma.f64 v v #s(literal -1 binary64)))))
(neg.f64 (acos.f64 (/.f64 (+.f64 #s(literal 1 binary64) (*.f64 (*.f64 v v) #s(literal -5 binary64))) (fma.f64 v v #s(literal -1 binary64)))))
(neg.f64 (acos.f64 (/.f64 (fma.f64 (*.f64 v v) #s(literal -5 binary64) #s(literal 1 binary64)) (fma.f64 v v #s(literal -1 binary64)))))
Symmetry

(abs v)

Compiler

Compiled 15 to 9 computations (40% saved)

eval0.0ms (0%)

Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
99.2%
(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 30 to 18 computations (40% saved)

simplify4.0ms (0%)

Algorithm
egg-herbie
Rules
12×neg-mul-1
10×unsub-neg
*-commutative
+-commutative
distribute-lft-neg-in
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01453
12753
24153
35553
47453
510153
610953
711153
Stop Event
saturated
Calls
Call 1
Inputs
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
Outputs
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (-.f64 (*.f64 v v) #s(literal 1 binary64))))
(acos.f64 (/.f64 (-.f64 #s(literal 1 binary64) (*.f64 #s(literal 5 binary64) (*.f64 v v))) (+.f64 (*.f64 v v) #s(literal -1 binary64))))

soundness0.0ms (0%)

Stop Event
fuel
Compiler

Compiled 15 to 10 computations (33.3% saved)

preprocess18.0ms (0.2%)

Remove

(abs v)

Compiler

Compiled 120 to 78 computations (35% saved)

end0.0ms (0%)

Profiling

Loading profile data...