Herbie run

Date:Friday, May 17th, 2024
Commit:468a8500 on if-cost
Hostname:nightly with Racket 8.11.1
Seed:2024138
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: 6.4min)

sample1.5min (22.5%)

Results
32.2s281786×0valid
15.4s51717×1valid
13.3s23521×5exit
6.0s13249×2valid
385.0ms4236×0invalid
111.0ms926×0unsamplable
Precisions
Click to see histograms. Total time spent on operations: 50.2s
ival-mult: 11.8s (23.5% of total)
ival-add: 5.9s (11.7% of total)
ival-pow: 5.5s (10.9% of total)
ival-sub: 4.0s (8% of total)
backward-pass: 3.9s (7.7% of total)
ival-div: 3.7s (7.4% of total)
...c/correct-round.rkt:119:19: 3.1s (6.2% of total)
ival-<=: 2.7s (5.4% of total)
compiled-spec: 2.2s (4.3% of total)
ival-sin: 2.1s (4.1% of total)
ival-log: 1.0s (2% of total)
ival-exp: 846.0ms (1.7% of total)
const: 814.0ms (1.6% of total)
ival-cos: 621.0ms (1.2% of total)
ival-neg: 475.0ms (0.9% of total)
ival-sqrt: 458.0ms (0.9% of total)
ival-and: 432.0ms (0.9% of total)
ival-==: 305.0ms (0.6% of total)
ival-tan: 131.0ms (0.3% of total)
ival-<: 121.0ms (0.2% of total)
ival-atan: 81.0ms (0.2% of total)
ival-pi: 38.0ms (0.1% of total)
ival-if: 8.0ms (0% of total)
ival-fabs: 4.0ms (0% of total)
Bogosity

soundness1.2min (18%)

Rules
635468×*-lowering-*.f32
635468×*-lowering-*.f64
341528×+-lowering-+.f32
341528×+-lowering-+.f64
301300×/-lowering-/.f64
Stop Event
13×saturated
182×iter limit
173×node limit
26×fuel
16×done
Compiler

Compiled 25339 to 12955 computations (48.9% saved)

simplify1.0min (16.1%)

Algorithm
334×egg-herbie
Rules
762780×*-lowering-*.f32
762780×*-lowering-*.f64
432800×+-lowering-+.f32
432800×+-lowering-+.f64
306124×fma-lowering-fma.f64
Stop Event
282×iter limit
117×saturated
227×node limit
Counts
37428 → 37428

rewrite54.7s (14.1%)

Algorithm
146×batch-egg-rewrite
Rules
484876×*-lowering-*.f32
484876×*-lowering-*.f64
380910×/-lowering-/.f64
380910×/-lowering-/.f32
204806×+-lowering-+.f32
Stop Event
11×saturated
145×iter limit
140×node limit
Counts
1867 → 74181

localize28.4s (7.4%)

Results
10.8s31512×0valid
3.0s3096×1valid
2.5s1346×2valid
2.5s855×5exit
561.0ms137×3valid
147.0ms386×0invalid
28.0ms17×1unsamplable
13.0ms25×0unsamplable
8.0ms4valid
Compiler

Compiled 35670 to 3613 computations (89.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 10.7s
ival-mult: 3.6s (34% of total)
ival-div: 1.7s (15.4% of total)
ival-add: 1.4s (13.3% of total)
backward-pass: 1.0s (9.4% of total)
...c/correct-round.rkt:119:19: 765.0ms (7.1% of total)
ival-sub: 541.0ms (5% of total)
ival-pow: 452.0ms (4.2% of total)
ival-tan: 283.0ms (2.6% of total)
ival-cos: 261.0ms (2.4% of total)
compiled-spec: 247.0ms (2.3% of total)
const: 109.0ms (1% of total)
ival-exp: 92.0ms (0.9% of total)
ival-sqrt: 80.0ms (0.7% of total)
ival-sin: 44.0ms (0.4% of total)
ival-atan: 43.0ms (0.4% of total)
ival-log: 40.0ms (0.4% of total)
ival-neg: 22.0ms (0.2% of total)
ival-pi: 6.0ms (0.1% of total)

eval22.6s (5.8%)

Compiler

Compiled 5197241 to 313824 computations (94% saved)

prune18.1s (4.7%)

Counts
133582 → 2839
Compiler

Compiled 169391 to 65775 computations (61.2% saved)

bsearch10.1s (2.6%)

Algorithm
333×binary-search
11×left-value
Stop Event
19×predicate-same
314×narrow-enough
Results
4.2s31777×0valid
2.6s8921×1valid
332.0ms486×2valid
258.0ms2123×0invalid
8.0ms68×0unsamplable
Compiler

Compiled 78737 to 52253 computations (33.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 5.2s
ival-pow: 1.4s (27% of total)
ival-mult: 1.3s (24.7% of total)
ival-div: 709.0ms (13.6% of total)
ival-add: 669.0ms (12.8% of total)
ival-sub: 562.0ms (10.7% of total)
backward-pass: 191.0ms (3.7% of total)
ival-neg: 115.0ms (2.2% of total)
ival-exp: 114.0ms (2.2% of total)
const: 85.0ms (1.6% of total)
ival-sqrt: 37.0ms (0.7% of total)
ival-pi: 21.0ms (0.4% of total)
...c/correct-round.rkt:119:19: 17.0ms (0.3% of total)
ival-log: 2.0ms (0% of total)

preprocess9.4s (2.4%)

Algorithm
84×egg-herbie
Rules
65240×fnmadd-define
62928×sum3-define
53926×fmsub-define
53286×fma-define
48410×sum4-define
Stop Event
44×saturated
40×iter limit
42×node limit
Compiler

Compiled 24752 to 8262 computations (66.6% saved)

explain8.2s (2.1%)

Results
2.7s3802×1valid
2.1s16374×0valid
625.0ms1044×2valid
138.0ms260×5exit
29.0ms22×3valid
3.0ms4valid
Compiler

Compiled 7687 to 1404 computations (81.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 3.7s
ival-pow: 1.7s (46.1% of total)
ival-mult: 601.0ms (16.2% of total)
ival-add: 282.0ms (7.6% of total)
ival-div: 260.0ms (7% of total)
backward-pass: 200.0ms (5.4% of total)
ival-sub: 195.0ms (5.2% of total)
ival-sin: 96.0ms (2.6% of total)
ival-cos: 66.0ms (1.8% of total)
ival-exp: 57.0ms (1.5% of total)
...c/correct-round.rkt:119:19: 50.0ms (1.3% of total)
ival-log: 50.0ms (1.3% of total)
const: 46.0ms (1.2% of total)
ival-sqrt: 37.0ms (1% of total)
ival-neg: 27.0ms (0.7% of total)
compiled-spec: 23.0ms (0.6% of total)
ival-tan: 7.0ms (0.2% of total)
ival-atan: 5.0ms (0.1% of total)
ival-pi: 2.0ms (0.1% of total)

regimes7.9s (2.1%)

Counts
8479 → 688
Calls

96 calls:

1.4s
x
526.0ms
(-.f64 #s(literal 1 binary64) (*.f64 x x))
484.0ms
b
338.0ms
a
307.0ms
(*.f64 x x)
Compiler

Compiled 3614 to 2340 computations (35.3% saved)

analyze4.7s (1.2%)

Algorithm
43×search
random
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%54.5%45.5%0%0%0%0
21.4%11.7%42.9%45.5%0%0%0%1
35.2%19.2%35.3%45.5%0%0%0%2
47.6%25.7%28.3%45.5%0%0.6%0%3
57.1%30.5%22.8%45.5%0%1.2%0%4
70.9%37.5%15.4%45.6%0%1.5%0%5
72.8%38.4%14.4%45.6%0%1.7%0%6
77.8%40.7%11.6%45.6%0%2%0%7
81.4%42.5%9.7%45.7%0%2.1%0%8
84.1%43.8%8.3%45.7%0%2.2%0%9
86.2%44.6%7.2%45.7%0%2.5%0%10
88.2%45.6%6.1%45.7%0%2.5%0.1%11
89.1%45.9%5.6%45.7%0%2.6%0.1%12
Compiler

Compiled 1441 to 688 computations (52.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.8s
ival-mult: 693.0ms (24.5% of total)
ival-div: 448.0ms (15.8% of total)
ival-pow: 360.0ms (12.7% of total)
ival-add: 340.0ms (12% of total)
ival-sub: 273.0ms (9.6% of total)
ival-<=: 150.0ms (5.3% of total)
ival-sqrt: 102.0ms (3.6% of total)
ival-exp: 93.0ms (3.3% of total)
ival-if: 70.0ms (2.5% of total)
ival-==: 54.0ms (1.9% of total)
...c/correct-round.rkt:119:19: 52.0ms (1.8% of total)
ival-fabs: 50.0ms (1.8% of total)
const: 45.0ms (1.6% of total)
ival-and: 30.0ms (1.1% of total)
ival-neg: 26.0ms (0.9% of total)
ival-<: 26.0ms (0.9% of total)
backward-pass: 9.0ms (0.3% of total)
ival-pi: 4.0ms (0.1% of total)
ival-cos: 2.0ms (0.1% of total)
ival-log: 1.0ms (0% of total)
ival-atan: 0.0ms (0% of total)
ival-tan: 0.0ms (0% of total)
ival-sin: 0.0ms (0% of total)
compiled-spec: 0.0ms (0% of total)

series3.7s (1%)

Counts
1867 → 37428
Calls

7812 calls:

TimeVariablePointExpression
410.0ms
v
@-inf
(/ (+ (* (+ (* (/ (* (* w w) (* (* r r) (+ 3/8 (* v -1/4)))) (- 1 v)) (/ (* (* w w) (* (* r r) (+ 3/8 (* v -1/4)))) (- 1 v))) -9/4) (* r r)) (* (+ (/ (* (* w w) (* (* r r) (+ 3/8 (* v -1/4)))) (+ v -1)) 3/2) 2)) (* (+ (/ (* (* w w) (* (* r r) (+ 3/8 (* v -1/4)))) (+ v -1)) 3/2) (* r r)))
45.0ms
t
@-inf
(/ 1 (/ (+ 2 (/ (* (* t t) 4) (* (+ t 1) (+ t 1)))) (+ 1 (/ (* (* t t) 4) (* (+ t 1) (+ t 1))))))
36.0ms
a
@inf
(/ (+ (* (/ a (* b b)) (/ (/ a (* b b)) (/ (* b b) a))) (/ -1 (* c (* c c)))) (+ (/ (/ a (* b b)) (/ (* b b) a)) (* (/ 1 c) (+ (/ a (* b b)) (/ 1 c)))))
35.0ms
b
@inf
(/ (/ (+ b (sqrt (* -4 (* c a)))) -2) a)
31.0ms
x1
@-inf
(+ x1 (+ (* (+ (* x1 x1) 1) (+ x1 (+ (* (* x1 x1) -6) (* (/ (+ (* 2 x2) (* x1 (+ (* x1 3) -1))) (+ (* x1 x1) 1)) (+ (* x1 (+ -6 (/ (* 2 (+ (* 2 x2) (* x1 (+ (* x1 3) -1)))) (+ (* x1 x1) 1)))) (* (* x1 x1) 4)))))) (* 3 (+ (/ (* x1 (* x1 (+ (* 2 x2) (* x1 (+ (* x1 3) -1))))) (+ (* x1 x1) 1)) (/ (+ (* x2 -2) (* x1 (+ (* x1 3) -1))) (+ (* x1 x1) 1))))))

end4.0ms (0%)

Profiling

Loading profile data...