Herbie run

Date:Friday, April 26th, 2024
Commit:00df8817 on fix-proofs
Hostname:nightly with Racket 8.11.1
Seed:2024117
Parameters:256 points for 4 iterations
Flags:
reduce: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: 5.9min)

sample2.7min (46.3%)

Results
28.2s140049×0precondition
28.5s116203×1valid
6.2s57017×0valid
42.0s55301×2valid
29.8s7311×5exit
569.0ms4243×0unsamplable
416.0ms4154×0invalid
3.8s2647×3valid
Precisions
Click to see histograms. Total time spent on operations: 2.0min
ival-pow: 29.0s (24.7% of total)
ival-tan: 12.3s (10.5% of total)
ival-exp: 12.1s (10.3% of total)
ival-mult: 9.7s (8.2% of total)
ival-sub: 8.5s (7.3% of total)
ival-log: 5.6s (4.7% of total)
backward-pass: 5.2s (4.4% of total)
ival-div: 5.0s (4.3% of total)
ival-add: 4.9s (4.2% of total)
ival-cos: 4.5s (3.9% of total)
ival-<=: 4.4s (3.7% of total)
ival-sin: 4.1s (3.5% of total)
ival-fabs: 3.9s (3.3% of total)
ival-<: 2.3s (2% of total)
ival-sqrt: 1.4s (1.2% of total)
ival-fmin: 991.0ms (0.8% of total)
ival-and: 825.0ms (0.7% of total)
const: 798.0ms (0.7% of total)
ival->: 730.0ms (0.6% of total)
ival-neg: 506.0ms (0.4% of total)
ival-atan: 382.0ms (0.3% of total)
ival-cbrt: 339.0ms (0.3% of total)
Bogosity

localize36.6s (10.4%)

Algorithm
111×egg-herbie
Rules
48952×fma-define
41392×fma-neg
21853×distribute-lft-in
18665×distribute-rgt-in
17598×unsub-neg
Stop Event
48×saturated
63×node limit
Results
4.3s14171×0valid
6.3s7696×1valid
6.4s4499×2valid
595.0ms1278×0invalid
1.3s412×3valid
909.0ms360×5exit
Compiler

Compiled 17933 to 2619 computations (85.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.6s
ival-mult: 2.4s (17.4% of total)
ival-pow: 2.0s (14.7% of total)
backward-pass: 1.4s (10.4% of total)
ival-div: 1.4s (10.1% of total)
ival-add: 982.0ms (7.2% of total)
ival-sin: 917.0ms (6.8% of total)
ival-tan: 696.0ms (5.1% of total)
ival-sub: 668.0ms (4.9% of total)
ival-log: 644.0ms (4.7% of total)
ival-exp: 529.0ms (3.9% of total)
ival-fma: 383.0ms (2.8% of total)
ival-cos: 295.0ms (2.2% of total)
ival-sqrt: 284.0ms (2.1% of total)
ival-cbrt: 201.0ms (1.5% of total)
ival-log1p: 195.0ms (1.4% of total)
ival-neg: 166.0ms (1.2% of total)
ival-cosh: 155.0ms (1.1% of total)
const: 133.0ms (1% of total)
ival-expm1: 79.0ms (0.6% of total)
ival-hypot: 47.0ms (0.3% of total)
ival-atan: 31.0ms (0.2% of total)
ival-atan2: 21.0ms (0.2% of total)
ival-e: 4.0ms (0% of total)

simplify35.6s (10.1%)

Algorithm
138×egg-herbie
Rules
36495×fma-neg
33013×fma-define
32104×times-frac
30254×*-commutative
29080×distribute-lft-in
Stop Event
28×saturated
110×node limit
Counts
57292 → 59461

soundness28.8s (8.2%)

Rules
35926×log1p-expm1-u
30705×fma-neg
29363×fma-define
28052×expm1-log1p-u
21730×associate-*r*
Stop Event
7×saturated
115×node limit
23×fuel
5×done
Compiler

Compiled 22206 to 6726 computations (69.7% saved)

rewrite24.9s (7.1%)

Algorithm
110×batch-egg-rewrite
Rules
70307×log1p-expm1-u
52328×expm1-log1p-u
22287×pow1
21912×add-exp-log
21748×add-log-exp
Stop Event
110×node limit
Counts
1257 → 38557

prune17.7s (5%)

Counts
83788 → 2062
Compiler

Compiled 66237 to 38279 computations (42.2% saved)

eval16.5s (4.7%)

Compiler

Compiled 1974206 to 315653 computations (84% saved)

series7.1s (2%)

Counts
1257 → 18735
Calls

5070 calls:

TimeVariablePointExpression
140.0ms
a
@-inf
(/ (pow (- (pow b_2 2) (* a c)) 1/4) a)
139.0ms
b_2
@-inf
(- (sqrt (- (pow b_2 2) (- (* a c) (* 2 (+ (* a (neg c)) (* a c)))))) b_2)
122.0ms
eps
@inf
(+ (* -1/2 (sin x)) (* -1/6 (* eps (cos x))))
113.0ms
x
@inf
(- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1))))
112.0ms
N
@inf
(+ 2 (/ (+ -1/2 (/ 1/3 N)) N))

explain7.0s (2%)

Results
2.5s7464×1valid
2.3s3354×2valid
429.0ms3332×0valid
345.0ms186×3valid
Compiler

Compiled 2227 to 707 computations (68.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 3.4s
ival-tan: 602.0ms (17.6% of total)
ival-exp: 590.0ms (17.2% of total)
ival-log: 337.0ms (9.8% of total)
ival-sub: 282.0ms (8.2% of total)
backward-pass: 273.0ms (8% of total)
ival-div: 245.0ms (7.1% of total)
ival-sin: 219.0ms (6.4% of total)
ival-cos: 201.0ms (5.9% of total)
ival-mult: 164.0ms (4.8% of total)
ival-sqrt: 143.0ms (4.2% of total)
ival-pow: 139.0ms (4.1% of total)
ival-add: 132.0ms (3.9% of total)
const: 32.0ms (0.9% of total)
ival-neg: 26.0ms (0.8% of total)
ival-atan: 24.0ms (0.7% of total)
ival-cbrt: 19.0ms (0.6% of total)

preprocess4.6s (1.3%)

Algorithm
28×egg-herbie
Rules
8308×fma-neg
6663×fma-define
4279×div-sub
2669×sub-neg
2621×times-frac
Stop Event
23×saturated
5×node limit
Compiler

Compiled 8784 to 3682 computations (58.1% saved)

regimes3.7s (1.1%)

Counts
3804 → 312
Calls

43 calls:

1.4s
x
221.0ms
eps
213.0ms
c
193.0ms
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
169.0ms
b
Compiler

Compiled 1537 to 1030 computations (33% saved)

analyze3.3s (0.9%)

Algorithm
28×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%61.1%38.9%0%0%0%0
10.9%6.7%54.4%38.9%0%0%0%1
20.4%12.4%48.7%38.9%0%0%0%2
38.1%22.2%36.2%41.6%0%0%0%3
47.5%27.7%30.6%41.7%0%0%0%4
55.5%31.9%25.6%42.4%0%0%0%5
57.5%32.7%24.2%43.1%0%0%0%6
61.6%34%21.2%44%0%0.8%0.1%7
64.7%35.3%19.3%44.5%0%0.8%0.1%8
67.2%36%17.6%44.9%0%1.2%0.3%9
69.1%36.5%16.3%45.2%0%1.7%0.3%10
71.7%37.5%14.8%45.4%0%1.9%0.4%11
72.9%37.8%14.1%45.6%0%2.2%0.4%12
Compiler

Compiled 498 to 322 computations (35.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.7s
ival-mult: 220.0ms (13% of total)
ival-pow: 211.0ms (12.5% of total)
ival-sub: 187.0ms (11% of total)
ival-log: 181.0ms (10.7% of total)
ival-div: 176.0ms (10.4% of total)
ival-add: 142.0ms (8.4% of total)
ival-<=: 87.0ms (5.1% of total)
ival-exp: 82.0ms (4.8% of total)
ival-fmin: 77.0ms (4.5% of total)
ival-sin: 60.0ms (3.5% of total)
ival-sqrt: 56.0ms (3.3% of total)
ival-fabs: 48.0ms (2.8% of total)
ival-tan: 39.0ms (2.3% of total)
ival-neg: 36.0ms (2.1% of total)
const: 27.0ms (1.6% of total)
ival-cos: 24.0ms (1.4% of total)
ival->: 13.0ms (0.8% of total)
ival-and: 11.0ms (0.6% of total)
backward-pass: 8.0ms (0.5% of total)
ival-<: 8.0ms (0.5% of total)
ival-atan: 0.0ms (0% of total)
ival-cbrt: 0.0ms (0% of total)

bsearch2.7s (0.8%)

Algorithm
81×binary-search
27×left-value
Stop Event
4×predicate-same
77×narrow-enough
Results
842.0ms8534×0valid
337.0ms1719×0invalid
438.0ms939×1valid
261.0ms543×2valid
3.0ms24×0unsamplable
Compiler

Compiled 13428 to 10088 computations (24.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.1s
ival-sub: 280.0ms (24.5% of total)
ival-mult: 249.0ms (21.8% of total)
ival-pow: 159.0ms (13.9% of total)
ival-div: 143.0ms (12.5% of total)
ival-exp: 72.0ms (6.3% of total)
ival-sqrt: 68.0ms (5.9% of total)
ival-neg: 47.0ms (4.1% of total)
ival-add: 47.0ms (4.1% of total)
backward-pass: 31.0ms (2.7% of total)
ival-cos: 19.0ms (1.7% of total)
const: 17.0ms (1.5% of total)
ival-sin: 7.0ms (0.6% of total)
ival-cbrt: 5.0ms (0.4% of total)

end0.0ms (0%)

Profiling

Loading profile data...