Herbie run

Date:Saturday, December 9th, 2023
Commit:665878db on main
Hostname:nightly with Racket 8.6
Seed:2023343
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: 6.0min)

sample1.2min (20.7%)

Results
39.5s269499×body256valid
15.1s14497×body2048valid
8.1s19500×body1024valid
5.3s31024×body256infinite
2.7s11040×body512valid
1.8s202×body8192exit
452.0ms2739×body256invalid
450.0ms809×body4096valid
150.0ms957×body256unsamplable
97.0ms163×body1024infinite
74.0ms209×body512infinite
10.0ms11×body2048infinite
Bogosity

eval58.5s (16.3%)

Compiler

Compiled 2650382 to 1671494 computations (36.9% saved)

localize53.6s (14.9%)

Compiler

Compiled 31004 to 18333 computations (40.9% saved)

soundness49.0s (13.6%)

Rules
171184×fma-def
84666×associate-*r*
77160×times-frac
76704×distribute-lft-in
73478×associate-*l*
Stop Event
1×unsound
4×saturated
251×node limit
Compiler

Compiled 23954 to 14282 computations (40.4% saved)

simplify29.6s (8.2%)

Algorithm
165×egg-herbie
Rules
99160×fma-def
56988×associate-*r*
52988×distribute-lft-in
52554×log-prod
51362×associate-*l*
Stop Event
14×done
1×unsound
42×saturated
28×fuel
122×node limit
Counts
52199 → 48400
Compiler

Compiled 10151 to 6439 computations (36.6% saved)

prune21.7s (6%)

Counts
79552 → 2152
Compiler

Compiled 147697 to 99713 computations (32.5% saved)

regimes19.5s (5.4%)

Counts
4363 → 543
Calls

94 calls:

2.2s
d
2.1s
b
2.0s
c
1.5s
a
1.1s
x
Compiler

Compiled 82946 to 49861 computations (39.9% saved)

rewrite18.4s (5.1%)

Algorithm
123×batch-egg-rewrite
Rules
63556×log1p-expm1-u
54743×expm1-log1p-u
47886×prod-diff
41238×log-prod
40406×expm1-udef
Stop Event
123×node limit
Counts
925 → 34236

preprocess15.6s (4.4%)

Algorithm
42×egg-herbie
Rules
53066×fma-def
20932×sub-neg
19756×fma-neg
19090×div-sub
18074×unsub-neg
Stop Event
11×saturated
31×node limit
Compiler

Compiled 33636 to 20504 computations (39% saved)

bsearch8.3s (2.3%)

Algorithm
248×binary-search
29×left-value
Stop Event
227×narrow-enough
21×predicate-same
Results
4.3s21932×body256valid
1.4s3477×body256infinite
821.0ms1717×body1024valid
618.0ms684×body2048valid
218.0ms794×body512valid
182.0ms1748×body256invalid
19.0ms142×body256unsamplable
16.0ms8×body4096valid
10.0ms29×body512infinite
6.0ms10×body1024infinite
4.0ms5×body2048infinite
Compiler

Compiled 87808 to 59265 computations (32.5% saved)

analyze7.0s (1.9%)

Algorithm
43×search
2×random
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%54.5%45.5%0%0%0%0
23.5%12.8%41.7%45.5%0%0%0%1
37.4%20.4%34.1%45.5%0%0%0%2
49.2%26.2%27.1%45.5%0%1.2%0%3
58%30.7%22.3%45.5%0%1.5%0%4
71.4%37.7%15.1%45.6%0%1.7%0%5
73%38.4%14.2%45.6%0%1.7%0%6
78%40.7%11.5%45.6%0%2.2%0%7
81.6%42.6%9.6%45.7%0%2.2%0%8
84.5%43.8%8%45.7%0%2.5%0%9
86.6%44.6%6.9%45.7%0%2.7%0%10
88.7%45.6%5.8%45.7%0%2.8%0.1%11
89.7%45.9%5.3%45.7%0%2.9%0.1%12
Compiler

Compiled 1441 to 1017 computations (29.4% saved)

series3.3s (0.9%)

Counts
925 → 17963
Calls

5040 calls:

TimeVariablePointExpression
105.0ms
t
@0
(pow.f64 (pow.f64 (pow.f64 (cbrt.f64 (fma.f64 t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) 2) 3/4) 2)
75.0ms
t
@0
(pow.f64 (*.f64 (sqrt.f64 (pow.f64 (fma.f64 t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 3/4)) (sqrt.f64 (pow.f64 (fma.f64 t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/4))) 2)
74.0ms
i
@0
(/.f64 (-.f64 (*.f64 (*.f64 n 100) (*.f64 n 100)) (*.f64 (*.f64 100 (*.f64 (*.f64 n i) (-.f64 1/2 (/.f64 1/2 n)))) (*.f64 100 (*.f64 (*.f64 n i) (-.f64 1/2 (/.f64 1/2 n)))))) (-.f64 (*.f64 n 100) (*.f64 100 (*.f64 (*.f64 n i) (-.f64 1/2 (/.f64 1/2 n))))))
69.0ms
x
@-inf
(-.f64 (/.f64 x (tan.f64 x)) (/.f64 (sin.f64 x) (tan.f64 x)))
65.0ms
t
@-inf
(pow.f64 (pow.f64 (fma.f64 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/4) 2)

end10.0ms (0%)

Profiling

Loading profile data...