Metrics for Herbie run

Date:	Friday, October 6th, 2023
Commit:	add13636 on main
Hostname:	nightly with Racket 8.6
Seed:	2023279
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

sample9.9min (33.6%)

Results

2.7min	16006×	body	8192	exit
1.7min	65046×	body	1024	valid
1.4min	8166×	body	4096	valid
1.3min	269028×	body	256	valid
47.7s	13264×	body	2048	valid
39.3s	1596×	body	8192	valid
26.1s	32612×	body	512	valid
11.5s	4233×	body	1024	infinite
8.7s	26893×	body	256	infinite
6.7s	26477×	body	256	unsamplable
6.4s	627×	body	4096	infinite
5.7s	817×	body	2048	infinite
5.1s	21235×	body	256	invalid
3.7s	2136×	body	512	infinite
3.3s	5392×	body	2048	invalid
2.4s	3788×	body	1024	invalid
1.1s	2249×	body	512	invalid
447.0ms	18×	body	8192	infinite
152.0ms	874×	body	256	precondition
6.0ms	6×	body	512	unsamplable
3.0ms	2×	body	1024	unsamplable
3.0ms	7×	body	4096	invalid

Bogosity

localize8.1min (27.7%)

Results

Compiler

Compiled 75852 to 35446 computations (53.3% saved)

eval2.2min (7.5%)

Results

Compiler

Compiled 5021567 to 2724632 computations (45.7% saved)

soundness2.0min (6.8%)

Rules

344154×	`fma-def`
208364×	`associate-r`
192708×	`log-prod`
157782×	`*-commutative`
151458×	`associate-l`

Stop Event

10×	unsound
9×	saturated
443×	node limit

Results

Compiler

Compiled 47232 to 25878 computations (45.2% saved)

preprocess1.6min (5.3%)

Algorithm

51×	egg-herbie

Rules

66624×	`fma-def`
26490×	`fma-neg`
25742×	`div-sub`
23584×	`sub-neg`
22428×	`distribute-lft-neg-in`

Stop Event

10×	saturated
41×	node limit

Results

Compiler

Compiled 39902 to 20359 computations (49% saved)

regimes1.5min (5.2%)

Counts

14938 → 857

Calls

132 calls:

7.0s	phi2
6.9s	phi1
5.9s	lambda2
5.6s	b
5.2s	lambda1

Results

Compiler

Compiled 307517 to 131456 computations (57.3% saved)

simplify1.1min (3.6%)

Algorithm

217×	egg-herbie

Rules

155624×	`fma-def`
96130×	`associate-r`
83692×	`log-prod`
80222×	`associate-l`
76912×	`*-commutative`

Stop Event

2×	unsound
47×	saturated
7×	done
40×	fuel
168×	node limit

Counts

72549 → 57184

Compiler

Compiled 13964 to 8870 computations (36.5% saved)

prune1.0min (3.5%)

Counts: 112584 → 6138
Compiler: Compiled 664570 to 446185 computations (32.9% saved)

analyze51.2s (2.9%)

Algorithm

53×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	79.4%	20.6%	0%	0%	0%	0
19.6%	15.5%	63.8%	20.6%	0%	0%	0%	1
27.1%	21.4%	57.6%	21%	0%	0%	0%	2
36.8%	28.5%	48.9%	21.2%	0%	1.4%	0%	3
42.3%	32.2%	43.9%	21.2%	0%	2.8%	0%	4
47.2%	35.4%	39.6%	21.2%	0%	3.8%	0%	5
50.2%	37.2%	36.9%	21.2%	0%	4.6%	0%	6
53.6%	39.3%	34%	21.2%	0%	5.4%	0.1%	7
55.3%	40.3%	32.5%	21.3%	0%	5.8%	0.1%	8
58.3%	42%	30.1%	21.3%	0%	6.4%	0.2%	9
59.6%	42.8%	29%	21.3%	0%	6.7%	0.2%	10
61.9%	44.2%	27.2%	21.3%	0%	7.1%	0.3%	11
63.3%	45%	26%	21.3%	0%	7.4%	0.3%	12

Compiler

Compiled 1919 to 1338 computations (30.3% saved)

bsearch29.3s (1.7%)

Algorithm

373×	binary-search
36×	left-value

Stop Event

365×	narrow-enough
8×	predicate-same

Results

11.4s	7202×	body	1024	valid
9.1s	30632×	body	256	valid
2.4s	3213×	body	512	valid
2.2s	1646×	body	2048	valid
1.5s	1098×	body	4096	valid
575.0ms	2929×	body	256	invalid
233.0ms	787×	body	256	infinite
225.0ms	499×	body	512	infinite
177.0ms	23×	body	2048	infinite
156.0ms	150×	body	1024	infinite
149.0ms	12×	body	4096	infinite
48.0ms	2×	body	8192	valid
43.0ms	66×	body	1024	invalid
29.0ms	67×	body	512	invalid
19.0ms	28×	body	2048	invalid
6.0ms	62×	body	256	unsamplable

Compiler

Compiled 102058 to 74157 computations (27.3% saved)

rewrite27.2s (1.5%)

Algorithm

170×	batch-egg-rewrite

Rules

123524×	`pow1`
116878×	`add-exp-log`
116804×	`log1p-expm1-u`
116772×	`expm1-log1p-u`
108594×	`add-log-exp`

Stop Event

4×	unsound
166×	node limit

Counts

1552 → 37957

series13.7s (0.8%)

Counts

1552 → 34592

Calls

9195 calls:

Time	Variable		Point	Expression
402.0ms	lambda2	@	-inf	(log.f64 (hypot.f64 (sin.f64 (.f64 (-.f64 phi1 phi2) 1/2)) (.f64 (sqrt.f64 (.f64 (cos.f64 phi1) (cos.f64 phi2))) (sin.f64 (.f64 (-.f64 lambda1 lambda2) 1/2)))))
120.0ms	phi1	@	inf	(log.f64 (hypot.f64 (sin.f64 (.f64 (-.f64 phi1 phi2) 1/2)) (.f64 (sqrt.f64 (.f64 (cos.f64 phi1) (cos.f64 phi2))) (sin.f64 (.f64 (-.f64 lambda1 lambda2) 1/2)))))
119.0ms	phi1	@	inf	(fma.f64 (.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2)) (.f64 (sin.f64 phi1) (sin.f64 phi2)))
100.0ms	lambda1	@	0	(sqrt.f64 (+.f64 (.f64 (cos.f64 phi1) (pow.f64 (sin.f64 (.f64 1/2 (-.f64 lambda1 lambda2))) 2)) (pow.f64 (sin.f64 (*.f64 1/2 phi1)) 2)))
94.0ms	b	@	-inf	(log.f64 (+.f64 (exp.f64 a) (exp.f64 b)))

Herbie run

sample9.9min (33.6%)

localize8.1min (27.7%)

eval2.2min (7.5%)

soundness2.0min (6.8%)

preprocess1.6min (5.3%)

regimes1.5min (5.2%)

simplify1.1min (3.6%)

prune1.0min (3.5%)

analyze51.2s (2.9%)

bsearch29.3s (1.7%)

rewrite27.2s (1.5%)

series13.7s (0.8%)

end30.0ms (0%)

Profiling