Herbie run

Date:Thursday, June 6th, 2024
Commit:b2854467 on platforms
Hostname:nightly with Racket 8.11.1
Seed:2024158
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: 17.7min)

sample5.6min (32%)

Results
2.0min25813×5exit
1.1min129539×1valid
43.0s271146×0valid
23.2s8148×3valid
18.4s19092×2valid
13.2s49609×0unsamplable
8.7s1383×4valid
4.5s19112×0invalid
3.3s11260×1invalid
1.1s1779×2invalid
107.0ms871×0precondition
95.0ms5valid
40.0ms56×1unsamplable
19.0ms25×3invalid
3.0ms2unsamplable
3.0ms5unsamplable
1.0ms3unsamplable
Precisions
Click to see histograms. Total time spent on operations: 4.3min
ival-pow: 1.9min (43.8% of total)
ival-mult: 25.6s (9.9% of total)
ival-sin: 22.5s (8.7% of total)
ival-cos: 21.9s (8.4% of total)
ival-div: 16.6s (6.4% of total)
backward-pass: 12.3s (4.7% of total)
ival-add: 8.7s (3.3% of total)
ival-sub: 8.2s (3.2% of total)
ival-exp: 6.1s (2.4% of total)
ival-log: 5.3s (2% of total)
ival-sqrt: 5.0s (1.9% of total)
ival-neg: 3.4s (1.3% of total)
ival-<: 2.8s (1.1% of total)
...c/correct-round.rkt:119:19: 2.1s (0.8% of total)
const: 1.4s (0.5% of total)
ival-atan2: 826.0ms (0.3% of total)
ival-pi: 668.0ms (0.3% of total)
ival-tan: 585.0ms (0.2% of total)
ival-and: 418.0ms (0.2% of total)
ival-atan: 365.0ms (0.1% of total)
ival-acos: 362.0ms (0.1% of total)
ival-cbrt: 313.0ms (0.1% of total)
ival-<=: 231.0ms (0.1% of total)
ival-fabs: 156.0ms (0.1% of total)
ival-asin: 149.0ms (0.1% of total)
ival-==: 2.0ms (0% of total)
ival-or: 0.0ms (0% of total)
Bogosity

soundness2.3min (13%)

Rules
1373934×*-lowering-*.f32
1373934×*-lowering-*.f64
659654×+-lowering-+.f32
659654×+-lowering-+.f64
569054×/-lowering-/.f32
Stop Event
14×saturated
324×iter limit
44×fuel
308×node limit
done
Compiler

Compiled 60536 to 31729 computations (47.6% saved)

simplify2.1min (11.7%)

Algorithm
448×egg-herbie
Rules
1424942×*-lowering-*.f32
1424942×*-lowering-*.f64
765258×+-lowering-+.f32
765258×+-lowering-+.f64
420156×fma-lowering-fma.f64
Stop Event
399×iter limit
108×saturated
339×node limit
unsound
Counts
91013 → 91013

localize2.0min (11.1%)

Results
36.0s4567×5exit
31.1s12745×1valid
17.0s27542×0valid
8.0s2423×2valid
2.8s2573×0invalid
2.1s413×3valid
1.6s398×1invalid
53.0ms16×2invalid
18.0ms4valid
4.0ms0unsamplable
Compiler

Compiled 101830 to 8038 computations (92.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 51.8s
ival-mult: 10.9s (21% of total)
backward-pass: 7.7s (14.8% of total)
ival-cos: 6.2s (12% of total)
ival-sin: 6.0s (11.5% of total)
ival-div: 5.5s (10.6% of total)
ival-pow: 4.0s (7.8% of total)
ival-add: 3.2s (6.1% of total)
ival-sub: 1.6s (3.1% of total)
...c/correct-round.rkt:119:19: 1.6s (3.1% of total)
compiled-spec: 1.3s (2.4% of total)
ival-sqrt: 953.0ms (1.8% of total)
ival-log: 822.0ms (1.6% of total)
ival-atan2: 336.0ms (0.6% of total)
ival-cbrt: 254.0ms (0.5% of total)
ival-exp: 243.0ms (0.5% of total)
ival-atan: 229.0ms (0.4% of total)
const: 219.0ms (0.4% of total)
ival-tan: 204.0ms (0.4% of total)
ival-acos: 198.0ms (0.4% of total)
ival-neg: 179.0ms (0.3% of total)
ival-fabs: 138.0ms (0.3% of total)
ival-pi: 110.0ms (0.2% of total)
ival-asin: 31.0ms (0.1% 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.1%)

Algorithm
198×batch-egg-rewrite
Rules
741354×*-lowering-*.f32
741354×*-lowering-*.f64
519868×/-lowering-/.f32
519868×/-lowering-/.f64
266514×+-lowering-+.f32
Stop Event
saturated
199×iter limit
197×node limit
Counts
3525 → 124875

regimes59.6s (5.6%)

Counts
32581 → 1121
Calls

155 calls:

3.6s
b
3.3s
phi2
3.2s
a
3.1s
lambda1
3.1s
phi1
Compiler

Compiled 13609 to 9003 computations (33.8% saved)

eval49.2s (4.6%)

Compiler

Compiled 12000067 to 689660 computations (94.3% saved)

prune48.0s (4.5%)

Counts
269846 → 8152
Compiler

Compiled 658981 to 294359 computations (55.3% saved)

bsearch28.4s (2.7%)

Algorithm
60×left-value
442×binary-search
Stop Event
25×predicate-same
417×narrow-enough
Results
9.5s13131×1valid
5.7s33159×0valid
3.6s3486×2valid
3.6s1977×3valid
570.0ms103×4valid
320.0ms2268×0invalid
57.0ms121×1invalid
31.0ms63×2invalid
8.0ms3invalid
3.0ms37×0unsamplable
Compiler

Compiled 144973 to 97450 computations (32.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 18.8s
ival-cos: 3.4s (18.3% of total)
ival-sin: 3.3s (17.8% of total)
ival-mult: 3.0s (16% of total)
ival-pow: 2.5s (13.2% of total)
ival-div: 1.6s (8.4% of total)
backward-pass: 1.2s (6.5% of total)
ival-sub: 1.0s (5.4% of total)
ival-add: 802.0ms (4.3% of total)
ival-sqrt: 608.0ms (3.2% of total)
ival-atan2: 220.0ms (1.2% of total)
ival-exp: 209.0ms (1.1% of total)
ival-neg: 208.0ms (1.1% of total)
ival-atan: 192.0ms (1% of total)
const: 110.0ms (0.6% of total)
ival-log: 110.0ms (0.6% of total)
ival-pi: 109.0ms (0.6% of total)
ival-acos: 88.0ms (0.5% of total)
ival-tan: 45.0ms (0.2% of total)
ival-fabs: 14.0ms (0.1% of total)
ival-asin: 11.0ms (0.1% of total)

analyze24.5s (2.3%)

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: 15.1s
ival-mult: 4.3s (28.6% of total)
ival-pow: 2.0s (13.3% of total)
ival-sin: 1.6s (10.9% of total)
ival-cos: 1.6s (10.6% of total)
ival-div: 1.2s (7.7% of total)
ival-sub: 1.0s (6.8% of total)
ival-add: 765.0ms (5.1% of total)
...c/correct-round.rkt:119:19: 564.0ms (3.7% of total)
ival-sqrt: 516.0ms (3.4% of total)
ival-<: 386.0ms (2.6% of total)
ival-neg: 283.0ms (1.9% of total)
ival-atan2: 173.0ms (1.1% of total)
const: 92.0ms (0.6% of total)
ival-exp: 90.0ms (0.6% of total)
ival-tan: 84.0ms (0.6% of total)
ival-pi: 70.0ms (0.5% of total)
ival-and: 54.0ms (0.4% of total)
ival-log: 53.0ms (0.4% of total)
ival-atan: 50.0ms (0.3% of total)
ival-acos: 43.0ms (0.3% of total)
backward-pass: 38.0ms (0.3% of total)
ival-asin: 35.0ms (0.2% of total)
ival-fabs: 31.0ms (0.2% of total)
ival-cbrt: 18.0ms (0.1% of total)
ival-<=: 3.0ms (0% of total)
ival-==: 1.0ms (0% of total)
ival-or: 0.0ms (0% of total)

explain21.4s (2%)

Results
6.7s8400×1valid
3.6s15654×0valid
3.0s1870×2valid
2.2s600×3valid
745.0ms100×4valid
Compiler

Compiled 20263 to 2450 computations (87.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.9s
ival-sin: 2.0s (22.4% of total)
ival-mult: 1.4s (15.3% of total)
ival-cos: 1.3s (14.8% of total)
backward-pass: 921.0ms (10.3% of total)
ival-pow: 686.0ms (7.7% of total)
ival-div: 675.0ms (7.5% of total)
ival-sub: 371.0ms (4.1% of total)
ival-add: 349.0ms (3.9% of total)
ival-sqrt: 271.0ms (3% of total)
ival-log: 260.0ms (2.9% of total)
ival-exp: 182.0ms (2% of total)
ival-neg: 148.0ms (1.7% of total)
ival-tan: 103.0ms (1.2% of total)
ival-atan2: 64.0ms (0.7% of total)
const: 56.0ms (0.6% of total)
ival-pi: 41.0ms (0.5% of total)
ival-asin: 33.0ms (0.4% of total)
ival-atan: 31.0ms (0.3% of total)
ival-cbrt: 25.0ms (0.3% of total)
ival-acos: 21.0ms (0.2% of total)
ival-fabs: 12.0ms (0.1% of total)

series20.2s (1.9%)

Counts
3525 → 91013
Calls

18654 calls:

TimeVariablePointExpression
315.0ms
x
@-inf
(log (+ x x))
260.0ms
v
@inf
(* (/ (- 1 m) v) m)
146.0ms
s
@inf
(pow (* (/ 1 (+ 1 (exp (- 0 t)))) (+ 1 (exp (- 0 s)))) (- 0 c_p))
140.0ms
t
@inf
(/ (* (pow (/ 1 (+ 1 (exp (neg s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (neg t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (neg t))))) c_n)))
117.0ms
angle
@-inf
(* (* 1/4 (* y-scale (sqrt 8))) (sqrt (- (* (* b b) (+ 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90))))) (- (/ (+ (* -1 (* (+ (* (* a a) (- 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90))))) (* (* b b) (+ 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90)))))) (* (/ 1 (* y-scale y-scale)) (+ (* (* a a) (+ 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90))))) (* (* b b) (- 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90))))))))) (* 2 (/ (* (+ 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90)))) (* (- 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90)))) (* (+ a b) (* (+ a b) (* (- b a) (- b a)))))) (* y-scale y-scale)))) (* (/ 1 (* y-scale y-scale)) (+ (* (* a a) (+ 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90))))) (* (* b b) (- 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90)))))))) (* (* a a) (- 1/2 (* 1/2 (cos (* (* angle (PI)) 1/90)))))))))

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 69456 to 24586 computations (64.6% saved)

end0.0ms (0%)

Profiling

Loading profile data...