Herbie run

Date:Friday, May 31st, 2024
Commit:5a183db8 on platforms
Hostname:nightly with Racket 8.11.1
Seed:2024152
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:avg-errorreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default

Time bar (total: 16.8min)

sample5.5min (32.6%)

Results
2.0min25937×5exit
1.1min129449×1valid
42.8s271205×0valid
22.8s8142×3valid
17.3s19160×2valid
12.6s49963×0unsamplable
8.2s1355×4valid
3.9s18596×0invalid
2.5s11013×1invalid
1.1s1767×2invalid
104.0ms875×0precondition
44.0ms64×1unsamplable
13.0ms22×3invalid
3.0ms5unsamplable
2.0ms5valid
2.0ms4unsamplable
Precisions
Click to see histograms. Total time spent on operations: 4.3min
ival-pow: 1.9min (44.8% of total)
ival-mult: 26.5s (10.3% of total)
ival-sin: 23.6s (9.1% of total)
ival-cos: 20.5s (7.9% of total)
ival-div: 15.4s (5.9% of total)
backward-pass: 9.8s (3.8% of total)
ival-add: 9.0s (3.5% of total)
ival-sub: 8.5s (3.3% of total)
ival-exp: 5.9s (2.3% of total)
ival-sqrt: 5.0s (1.9% of total)
ival-log: 4.8s (1.8% of total)
ival-neg: 3.6s (1.4% of total)
ival-<: 2.6s (1% of total)
...c/correct-round.rkt:119:19: 1.8s (0.7% of total)
const: 1.1s (0.4% of total)
ival-pi: 1.0s (0.4% of total)
ival-atan2: 725.0ms (0.3% of total)
ival-tan: 626.0ms (0.2% of total)
ival-atan: 450.0ms (0.2% of total)
ival-and: 416.0ms (0.2% of total)
ival-cbrt: 403.0ms (0.2% of total)
ival-acos: 387.0ms (0.1% of total)
ival-<=: 278.0ms (0.1% of total)
ival-fabs: 148.0ms (0.1% of total)
ival-asin: 133.0ms (0.1% of total)
ival-==: 2.0ms (0% of total)
ival-or: 0.0ms (0% of total)
Bogosity

simplify2.1min (12.6%)

Algorithm
453×egg-herbie
Rules
1461552×*-lowering-*.f32
1461552×*-lowering-*.f64
783652×+-lowering-+.f32
783652×+-lowering-+.f64
421302×fma-lowering-fma.f64
Stop Event
403×iter limit
106×saturated
347×node limit
Counts
92152 → 92152

soundness2.1min (12.5%)

Rules
1302594×*-lowering-*.f32
1302594×*-lowering-*.f64
641528×+-lowering-+.f32
641528×+-lowering-+.f64
526984×/-lowering-/.f32
Stop Event
11×saturated
307×iter limit
43×fuel
293×node limit
done
Compiler

Compiled 53375 to 28052 computations (47.4% saved)

localize1.6min (9.4%)

Results
26.6s4434×5exit
22.2s13031×1valid
11.4s27575×0valid
7.3s2557×2valid
2.6s2903×0invalid
1.6s374×3valid
1.3s474×1invalid
140.0ms100×0unsamplable
68.0ms4valid
2.0ms2invalid
Compiler

Compiled 107204 to 8036 computations (92.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 51.0s
ival-mult: 11.4s (22.5% of total)
ival-sin: 6.6s (13% of total)
ival-cos: 6.3s (12.3% of total)
backward-pass: 5.4s (10.5% of total)
ival-div: 5.3s (10.4% of total)
ival-pow: 3.4s (6.6% of total)
ival-add: 2.6s (5% of total)
ival-sub: 1.9s (3.8% of total)
ival-exp: 1.5s (3% of total)
...c/correct-round.rkt:119:19: 1.5s (2.9% of total)
compiled-spec: 1.4s (2.7% of total)
ival-log: 1.0s (2% of total)
ival-sqrt: 896.0ms (1.8% of total)
ival-atan2: 324.0ms (0.6% of total)
const: 261.0ms (0.5% of total)
ival-tan: 239.0ms (0.5% of total)
ival-atan: 206.0ms (0.4% of total)
ival-acos: 200.0ms (0.4% of total)
ival-cbrt: 199.0ms (0.4% of total)
ival-neg: 145.0ms (0.3% of total)
ival-pi: 107.0ms (0.2% of total)
ival-fabs: 68.0ms (0.1% of total)
ival-asin: 8.0ms (0% of total)
ival-cosh: 3.0ms (0% of total)
ival-tanh: 2.0ms (0% of total)
ival-sinh: 2.0ms (0% of total)

rewrite1.3min (7.8%)

Algorithm
201×batch-egg-rewrite
Rules
739266×*-lowering-*.f32
739266×*-lowering-*.f64
519792×/-lowering-/.f32
519792×/-lowering-/.f64
281456×+-lowering-+.f32
Stop Event
saturated
203×iter limit
200×node limit
Counts
3571 → 125298

eval53.2s (5.3%)

Compiler

Compiled 13102037 to 696199 computations (94.7% saved)

regimes47.9s (4.7%)

Counts
27173 → 1060
Calls

155 calls:

3.4s
phi2
3.2s
b
2.6s
phi1
2.5s
a
2.3s
lambda1
Compiler

Compiled 12385 to 8142 computations (34.3% saved)

prune47.3s (4.7%)

Counts
274773 → 7994
Compiler

Compiled 669030 to 289014 computations (56.8% saved)

bsearch29.7s (2.9%)

Algorithm
449×binary-search
42×left-value
Stop Event
15×predicate-same
434×narrow-enough
Results
8.2s12077×1valid
5.7s36747×0valid
3.2s2644×5exit
3.1s1536×3valid
2.7s2763×2valid
635.0ms3913×0invalid
381.0ms35×4valid
272.0ms653×1invalid
136.0ms261×2invalid
0.0ms0unsamplable
Compiler

Compiled 137490 to 94407 computations (31.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 19.9s
ival-cos: 3.4s (17.2% of total)
ival-pow: 3.3s (16.4% of total)
ival-sin: 3.1s (15.5% of total)
ival-mult: 3.1s (15.5% of total)
ival-div: 1.9s (9.4% of total)
backward-pass: 1.2s (6% of total)
ival-sub: 1.2s (5.9% of total)
ival-add: 873.0ms (4.4% of total)
ival-sqrt: 556.0ms (2.8% of total)
ival-neg: 302.0ms (1.5% of total)
ival-exp: 297.0ms (1.5% of total)
ival-atan2: 194.0ms (1% of total)
ival-acos: 128.0ms (0.6% of total)
const: 126.0ms (0.6% of total)
ival-atan: 110.0ms (0.6% of total)
ival-pi: 105.0ms (0.5% of total)
ival-log: 49.0ms (0.2% of total)
ival-tan: 31.0ms (0.2% of total)
ival-asin: 28.0ms (0.1% of total)
ival-fabs: 12.0ms (0.1% of total)

analyze22.7s (2.2%)

Algorithm
53×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%79.4%20.6%0%0%0%0
14.8%11.8%67.6%20.6%0%0%0%1
22.6%17.7%60.4%21%0%0.9%0%2
32.7%24.7%50.8%21.2%0%3.3%0%3
39.8%29.8%45%21.2%0%4%0%4
45.4%33.8%40.6%21.2%0%4.5%0%5
48.4%35.7%38%21.2%0%5.1%0%6
51.8%37.8%35.2%21.2%0%5.7%0.1%7
53.5%38.9%33.8%21.3%0%6%0.1%8
56.4%40.6%31.4%21.3%0%6.6%0.2%9
57.7%41.4%30.3%21.3%0%6.8%0.2%10
59.8%42.7%28.7%21.3%0%7.1%0.3%11
61.3%43.5%27.5%21.3%0%7.5%0.3%12
Compiler

Compiled 1919 to 947 computations (50.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 14.3s
ival-mult: 4.2s (29.5% of total)
ival-pow: 2.1s (14.8% of total)
ival-cos: 1.8s (12.6% of total)
ival-sin: 1.2s (8.6% of total)
ival-div: 1.2s (8.2% of total)
ival-add: 848.0ms (5.9% of total)
ival-sub: 764.0ms (5.3% of total)
ival-sqrt: 479.0ms (3.3% of total)
...c/correct-round.rkt:119:19: 297.0ms (2.1% of total)
ival-neg: 273.0ms (1.9% of total)
ival-<: 249.0ms (1.7% of total)
ival-atan2: 180.0ms (1.3% of total)
ival-exp: 101.0ms (0.7% of total)
const: 94.0ms (0.7% of total)
ival-pi: 89.0ms (0.6% of total)
ival-atan: 69.0ms (0.5% of total)
ival-log: 58.0ms (0.4% of total)
ival-and: 53.0ms (0.4% of total)
ival-tan: 52.0ms (0.4% of total)
ival-acos: 36.0ms (0.3% of total)
ival-asin: 34.0ms (0.2% of total)
backward-pass: 32.0ms (0.2% of total)
ival-fabs: 32.0ms (0.2% of total)
ival-cbrt: 17.0ms (0.1% of total)
ival-<=: 3.0ms (0% of total)
ival-or: 0.0ms (0% of total)
ival-==: 0.0ms (0% of total)

series20.6s (2%)

Counts
3571 → 92152
Calls

18891 calls:

TimeVariablePointExpression
264.0ms
b
@-inf
(log (+ 2 b))
195.0ms
t
@inf
(exp (+ (- (* c_n (log (+ 1 (/ 1 (+ -1 (/ -1 (exp s))))))) (* c_n (log (+ 1 (/ 1 (- -1 (/ 1 (exp t)))))))) (+ (neg (* (log (+ 1 (/ 1 (exp s)))) c_p)) (* (log (+ 1 (/ 1 (exp t)))) c_p))))
121.0ms
phi1
@-inf
(* (atan2 (sqrt (+ 1/2 (* -1/2 (cos (- lambda1 lambda2))))) (sqrt (- (+ 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (cos phi1) (cos phi2)) (- 1/2 (* 1/2 (cos (* (- lambda1 lambda2) 1)))))))) (* R 2))
109.0ms
s
@inf
(exp (+ (- (* c_n (log (+ 1 (/ 1 (+ -1 (/ -1 (exp s))))))) (* c_n (log (+ 1 (/ 1 (- -1 (/ 1 (exp t)))))))) (+ (neg (* (log (+ 1 (/ 1 (exp s)))) c_p)) (* (log (+ 1 (/ 1 (exp t)))) c_p))))
109.0ms
y-scale
@0
(* x-scale (+ (* 1/8 (/ (* (* y-scale y-scale) (* (sqrt 1/2) (* (sqrt 8) (+ (* -1 (* b b)) (* b b))))) (* a (* x-scale x-scale)))) (* 1/4 (* a (* (sqrt 2) (sqrt 8))))))

explain18.1s (1.8%)

Results
4.7s8138×1valid
3.1s15984×0valid
2.7s1856×2valid
1.7s554×3valid
617.0ms92×4valid
Compiler

Compiled 20263 to 2450 computations (87.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 9.0s
ival-sin: 2.0s (22% of total)
ival-mult: 1.4s (15.5% of total)
ival-cos: 1.4s (15% of total)
ival-pow: 796.0ms (8.8% of total)
ival-div: 693.0ms (7.7% of total)
backward-pass: 614.0ms (6.8% of total)
ival-exp: 463.0ms (5.1% of total)
ival-add: 387.0ms (4.3% of total)
ival-sub: 371.0ms (4.1% of total)
ival-log: 204.0ms (2.3% of total)
ival-sqrt: 200.0ms (2.2% of total)
ival-tan: 148.0ms (1.6% of total)
ival-neg: 108.0ms (1.2% of total)
ival-atan2: 99.0ms (1.1% of total)
const: 58.0ms (0.6% of total)
ival-pi: 41.0ms (0.5% of total)
ival-atan: 29.0ms (0.3% of total)
ival-cbrt: 26.0ms (0.3% of total)
ival-acos: 24.0ms (0.3% of total)
ival-fabs: 13.0ms (0.1% of total)
ival-asin: 8.0ms (0.1% of total)

preprocess14.4s (1.4%)

Algorithm
104×egg-herbie
Rules
96972×fnmadd-define
86210×fma-define
80658×sum3-define
69822×fmsub-define
62900×*-lowering-*.f32
Stop Event
43×saturated
52×iter limit
61×node limit
Compiler

Compiled 63758 to 21140 computations (66.8% saved)

end0.0ms (0%)

Precisions
Click to see histograms. Total time spent on operations: 103.0ms
backward-pass: 103.0ms (100.2% of total)

Profiling

Loading profile data...