Metrics for Herbie run

Date:	Thursday, February 6th, 2025
Commit:	f63971dc on main
Seed:	2025037
Parameters:	256 points for 4 iterations
Flags:	`reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs` default
Memory:	93 394.5 MB

sample45.4s (53.4%)

Memory

872.6MiB live, 50 044.1MiB allocated; 13.7s collecting garbage

Samples

13.9s	16 527×	5	exit
8.4s	39 893×	1	valid
8.3s	108 742×	0	valid
5.8s	16 485×	2	valid
532.0ms	3 949×	0	invalid
130.0ms	1 482×	0	exit

Precisions

Click to see histograms. Total time spent on operations: 29.0s

ival-exp: 4.3s (14.8% of total)

ival-pow: 3.6s (12.3% of total)

adjust: 3.6s (12.3% of total)

ival-log: 3.2s (11.1% of total)

ival-cos: 2.2s (7.6% of total)

ival-mult: 1.6s (5.6% of total)

ival-tan: 1.5s (5.2% of total)

ival-sinh: 1.2s (4.3% of total)

ival-sqrt: 1.1s (3.9% of total)

ival-div: 968.0ms (3.3% of total)

ival-fmod: 855.0ms (3% of total)

ival-add: 854.0ms (2.9% of total)

ival-sub: 808.0ms (2.8% of total)

ival-sin: 722.0ms (2.5% of total)

ival-pow2: 716.0ms (2.5% of total)

ival-acos: 539.0ms (1.9% of total)

const: 432.0ms (1.5% of total)

ival-neg: 310.0ms (1.1% of total)

ival-hypot: 175.0ms (0.6% of total)

ival-assert: 74.0ms (0.3% of total)

ival-atan: 62.0ms (0.2% of total)

ival-<=: 53.0ms (0.2% of total)

exact: 41.0ms (0.1% of total)

ival-and: 40.0ms (0.1% of total)

ival-or: 20.0ms (0.1% of total)

ival->: 2.0ms (0% of total)

ival-==: 2.0ms (0% of total)

ival-<: 2.0ms (0% of total)

Bogosity

rewrite10.5s (12.4%)

Memory

-277.5MiB live, 10 251.7MiB allocated; 1.8s collecting garbage

Stop Event

186×	iter limit
49×	node limit
17×	unsound
4×	saturated

Counts

8 244 → 17 196

regimes4.9s (5.7%)

Memory

71.9MiB live, 6 840.6MiB allocated; 1.6s collecting garbage

Counts

3 336 → 209

Calls

53 calls:

610.0ms	x
542.0ms	(+.f64 y z)
494.0ms	a
348.0ms	b
220.0ms	r

Compiler

Compiled 1 729 to 1 999 computations (-15.6% saved)

preprocess4.1s (4.8%)

Memory

217.4MiB live, 3 798.0MiB allocated; 586ms collecting garbage

Stop Event

38×	iter limit
29×	node limit
13×	saturated

Compiler

Compiled 11 505 to 3 298 computations (71.3% saved)

analyze3.5s (4.1%)

Memory

15.7MiB live, 3 265.4MiB allocated; 2.2s collecting garbage

Algorithm

20×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	73.7%	26.3%	0%	0%	0%	0
28.8%	21.3%	52.5%	26.3%	0%	0%	0%	1
44.1%	32.5%	41.2%	26.3%	0%	0%	0%	2
52.6%	38.7%	35%	26.3%	0%	0%	0%	3
61.9%	45.6%	28.1%	26.3%	0%	0%	0%	4
65.2%	47.5%	25.3%	26.3%	0%	0.9%	0%	5
66.8%	48.4%	24%	26.3%	0%	1.2%	0%	6
71.1%	51.1%	20.8%	26.3%	0%	1.9%	0%	7
72.1%	51.6%	20%	26.3%	0%	2.1%	0%	8
74.4%	53%	18.2%	26.3%	0%	2.5%	0%	9
75.8%	53.9%	17.2%	26.3%	0%	2.6%	0%	10
76.6%	54.3%	16.6%	26.3%	0%	2.8%	0%	11
77.3%	54.8%	16.1%	26.3%	0%	2.9%	0%	12

Compiler

Compiled 279 to 216 computations (22.6% saved)

series3.2s (3.8%)

Memory

-368.5MiB live, 4 004.4MiB allocated; 675ms collecting garbage

Counts

1 493 → 6 751

Calls

384 calls:

Time	Variable		Point	Expression
80.0ms	x	@	-inf	((/ (- x lo) (- hi lo)) (+ (* (neg lo) (+ (* (/ x (* hi hi)) -1) (exp (* (log hi) -1)))) (/ x hi)) (neg lo) lo (+ (* (/ x (* hi hi)) -1) (exp (* (log hi) -1))) (/ x (* hi hi)) x (* hi hi) hi -1 (exp (* (log hi) -1)) (* (log hi) -1) (neg (log hi)) (log hi) (/ x hi) (/ (- x lo) (- hi lo)) (+ (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (/ hi lo)) (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) 1 (/ hi lo) (/ (- x lo) (- hi lo)) (/ (- (+ (* lo (/ (- x lo) hi)) x) lo) hi) (+ (* (/ (- (/ x hi) 1) hi) lo) (/ x hi)) (* -1 (* lo (+ (* -1 (/ x (* hi lo))) (* -1 (/ (- (/ x hi) 1) hi))))) (* lo (+ (* -1 (/ x (* hi lo))) (* -1 (/ (- (/ x hi) 1) hi)))) (+ (* -1 (/ x (* hi lo))) (* -1 (/ (- (/ x hi) 1) hi))) (/ x (* hi lo)) (* hi lo) (* -1 (/ (- (/ x hi) 1) hi)) (/ (- (/ x hi) 1) hi) (- (/ x hi) 1) (/ (- x lo) (- hi lo)) (- (+ (+ (* (pow (/ hi lo) 2) (neg (/ (- x hi) lo))) (/ (neg x) lo)) 1) (+ (* (* (neg (/ (- x hi) lo)) (/ hi lo)) -1) (/ (neg hi) lo))) (+ (+ (* (pow (/ hi lo) 2) (neg (/ (- x hi) lo))) (/ (neg x) lo)) 1) (+ (* (pow (/ hi lo) 2) (neg (/ (- x hi) lo))) (/ (neg x) lo)) (pow (/ hi lo) 2) 2 (neg (/ (- x hi) lo)) (/ (- x hi) lo) (- x hi) (/ (neg x) lo) (neg x) (+ (* (* (neg (/ (- x hi) lo)) (/ hi lo)) -1) (/ (neg hi) lo)) (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg hi) lo) (neg hi) (/ (- x lo) (- hi lo)) (+ (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (/ hi lo)) (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) (/ (- x hi) (neg lo)) (* x (- (/ hi (* lo x)) (pow lo -1))) (- (/ hi (* lo x)) (pow lo -1)) (/ hi (* lo x)) (* lo x) (pow lo -1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) (/ (- x hi) (neg lo)))
75.0ms	hi	@	-inf	((/ (- x lo) (- hi lo)) (+ (* (neg lo) (+ (* (/ x (* hi hi)) -1) (exp (* (log hi) -1)))) (/ x hi)) (neg lo) lo (+ (* (/ x (* hi hi)) -1) (exp (* (log hi) -1))) (/ x (* hi hi)) x (* hi hi) hi -1 (exp (* (log hi) -1)) (* (log hi) -1) (neg (log hi)) (log hi) (/ x hi) (/ (- x lo) (- hi lo)) (+ (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (/ hi lo)) (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) 1 (/ hi lo) (/ (- x lo) (- hi lo)) (/ (- (+ (* lo (/ (- x lo) hi)) x) lo) hi) (+ (* (/ (- (/ x hi) 1) hi) lo) (/ x hi)) (* -1 (* lo (+ (* -1 (/ x (* hi lo))) (* -1 (/ (- (/ x hi) 1) hi))))) (* lo (+ (* -1 (/ x (* hi lo))) (* -1 (/ (- (/ x hi) 1) hi)))) (+ (* -1 (/ x (* hi lo))) (* -1 (/ (- (/ x hi) 1) hi))) (/ x (* hi lo)) (* hi lo) (* -1 (/ (- (/ x hi) 1) hi)) (/ (- (/ x hi) 1) hi) (- (/ x hi) 1) (/ (- x lo) (- hi lo)) (- (+ (+ (* (pow (/ hi lo) 2) (neg (/ (- x hi) lo))) (/ (neg x) lo)) 1) (+ (* (* (neg (/ (- x hi) lo)) (/ hi lo)) -1) (/ (neg hi) lo))) (+ (+ (* (pow (/ hi lo) 2) (neg (/ (- x hi) lo))) (/ (neg x) lo)) 1) (+ (* (pow (/ hi lo) 2) (neg (/ (- x hi) lo))) (/ (neg x) lo)) (pow (/ hi lo) 2) 2 (neg (/ (- x hi) lo)) (/ (- x hi) lo) (- x hi) (/ (neg x) lo) (neg x) (+ (* (* (neg (/ (- x hi) lo)) (/ hi lo)) -1) (/ (neg hi) lo)) (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg hi) lo) (neg hi) (/ (- x lo) (- hi lo)) (+ (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (/ hi lo)) (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) (/ (- x hi) (neg lo)) (* x (- (/ hi (* lo x)) (pow lo -1))) (- (/ hi (* lo x)) (pow lo -1)) (/ hi (* lo x)) (* lo x) (pow lo -1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) (/ (- x hi) (neg lo)))
75.0ms	x	@	0	((/ (- x lo) (- hi lo)) (+ (* (neg lo) (+ (* (/ x (* hi hi)) -1) (pow hi -1))) (/ x hi)) (neg lo) lo (+ (* (/ x (* hi hi)) -1) (pow hi -1)) (/ x (* hi hi)) x (* hi hi) hi -1 (pow hi -1) (/ x hi) (/ (- x lo) (- hi lo)) 1 (/ (- x lo) (- hi lo)) (- x lo) (- hi lo) (/ (- x lo) (- hi lo)) (/ (- (+ (* lo (/ (- x lo) hi)) x) lo) hi) (- (+ (* lo (/ (- x lo) hi)) x) lo) (+ (* lo (/ (- x lo) hi)) x) (/ (- x lo) hi) (/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) (neg (/ (- x hi) lo)) (/ (- x hi) lo) (- x hi) (/ hi lo) (/ (neg x) lo) (neg x))
70.0ms	x	@	0	((/ (cos (* 2 x)) (pow (* (* s c) x) 2)) (cos (* 2 x)) (* 2 x) 2 x (pow (* (* s c) x) 2) (* (* s c) x) (* s c) s c (/ (cos (* 2 x)) (* (* (* c c) (* x x)) (* s s))) (* (* (* c c) (* x x)) (* s s)) (* (* c c) (* x x)) (* c c) (* x x) (* s s) (/ (cos (* 2 x)) (* (pow c 2) (* (* x (pow s 2)) x))) (/ (pow c -2) (pow (* s x) 2)) (pow c -2) -2 (pow (* s x) 2) (* s x) (/ (cos (* 2 x)) (* (pow (* s x) 2) (* c c))) (* (pow (* s x) 2) (* c c)) (/ (cos (* 2 x)) (* (pow c 2) (exp (* (log (* s x)) 2)))) (* (pow c 2) (exp (* (log (* s x)) 2))) (pow c 2) (exp (* (log (* s x)) 2)) (* (log (* s x)) 2) (log (* s x)))
66.0ms	x	@	inf	((log (/ (sinh x) x)) (/ (sinh x) x) (sinh x) x)

eval3.1s (3.7%)

Memory: 218.0MiB live, 4 210.7MiB allocated; 745ms collecting garbage
Compiler: Compiled 676 102 to 83 291 computations (87.7% saved)

derivations3.1s (3.7%)

Memory

-35.6MiB live, 2 069.6MiB allocated; 339ms collecting garbage

Stop Event

13×	fuel
7×	done

Compiler

Compiled 4 820 to 1 001 computations (79.2% saved)

explain3.1s (3.6%)

Memory

85.2MiB live, 3 693.5MiB allocated; 565ms collecting garbage

Explanations

Click to see full explanations table

Operator	Subexpression	Explanation	Count
`sqrt.f64`	`#f`	oflow-rescue	611	0
`cos.f64`	`#f`	sensitivity	553	0
`-.f64`	`#f`	cancellation	350	1
`sqrt.f64`	`#f`	uflow-rescue	316	0
`/.f64`	`#f`	n/o	262	0
`acos.f64`	`(acos.f64 (-.f64 #s(literal 1 binary64) x))`	sensitivity	253	1
`log.f64`	`(log.f64 (/.f64 (sinh.f64 x) x))`	sensitivity	249	0
`tan.f64`	`(tan.f64 (+.f64 y z))`	sensitivity	183	0
`pow.f64`	`(pow.f64 l (exp.f64 w))`	sensitivity	113	12
`*.f64`	`#f`	*no**	34	0
`*.f64`	`#f`	*nu**	29	0
`*.f64`	`#f`	*uo**	28	0
`*.f64`	`(.f64 (pow.f64 c #s(literal 2 binary64)) (.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))`	*ou**	15	0
↳	`(pow.f64 c #s(literal 2 binary64))`	overflow	65
↳	`(.f64 (.f64 x (pow.f64 s #s(literal 2 binary64))) x)`	underflow	56
↳	`(*.f64 x (pow.f64 s #s(literal 2 binary64)))`	underflow	55
↳	`(pow.f64 s #s(literal 2 binary64))`	underflow	59
`-.f64`	`(-.f64 (.f64 a a) (.f64 b b))`	nan-rescue	14	0
↳	`(*.f64 a a)`	overflow	120
↳	`(*.f64 b b)`	overflow	14
`log.f64`	`(log.f64 (/.f64 (sinh.f64 x) x))`	oflow-rescue	5	0
↳	`(sinh.f64 x)`	overflow	5
↳	`(/.f64 (sinh.f64 x) x)`	overflow	5
`exp.f64`	`(exp.f64 (neg.f64 x))`	sensitivity	1	0

Confusion

	Predicted +	Predicted -
+	2240	259
-	703	1918

Precision

0.7611281005776419

Recall

0.896358543417367

Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	2240	2	257
-	703	12	1906

Precision?

0.75820087926953

Recall?

0.8971588635454182

Freqs

test

number	freq
0	2177
1	2871
2	71
3	1

Total Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	18	0	0
-	0	0	2

Precision?

1.0

Recall?

1.0

Samples

549.0ms	2 558×	1	valid
509.0ms	98×	5	exit
478.0ms	6 600×	0	valid
344.0ms	984×	2	valid

Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions

Click to see histograms. Total time spent on operations: 1.5s

ival-cos: 507.0ms (34.8% of total)

adjust: 127.0ms (8.7% of total)

ival-tan: 112.0ms (7.7% of total)

ival-add: 90.0ms (6.2% of total)

ival-mult: 77.0ms (5.3% of total)

ival-log: 74.0ms (5.1% of total)

ival-sinh: 69.0ms (4.7% of total)

ival-sqrt: 68.0ms (4.7% of total)

ival-exp: 51.0ms (3.5% of total)

ival-sin: 42.0ms (2.9% of total)

ival-sub: 41.0ms (2.8% of total)

ival-fmod: 38.0ms (2.6% of total)

ival-pow2: 37.0ms (2.5% of total)

ival-div: 30.0ms (2.1% of total)

ival-acos: 27.0ms (1.9% of total)

ival-neg: 25.0ms (1.7% of total)

ival-hypot: 14.0ms (1% of total)

ival-pow: 10.0ms (0.7% of total)

ival-true: 9.0ms (0.6% of total)

ival-assert: 5.0ms (0.3% of total)

ival-atan: 3.0ms (0.2% of total)

exact: 2.0ms (0.1% of total)

prune2.1s (2.5%)

Memory: 382.1MiB live, 3 402.3MiB allocated; 444ms collecting garbage
Counts: 21 006 → 1 487
Compiler: Compiled 84 699 to 42 346 computations (50% saved)

simplify1.1s (1.3%)

Memory

-153.5MiB live, 847.3MiB allocated; 279ms collecting garbage

Stop Event

16×	node limit
4×	saturated

bsearch846.0ms (1%)

Memory

56.4MiB live, 965.2MiB allocated; 135ms collecting garbage

Algorithm

66×	binary-search
12×	left-value

Stop Event

43×	narrow-enough
14×	predicate-failed
9×	predicate-same

Samples

247.0ms	1 138×	1	valid
172.0ms	1 414×	0	invalid
94.0ms	1 246×	0	valid
57.0ms	144×	2	valid

Compiler

Compiled 18 231 to 13 982 computations (23.3% saved)

Precisions

Click to see histograms. Total time spent on operations: 443.0ms

ival-exp: 113.0ms (25.5% of total)

ival-cos: 107.0ms (24.1% of total)

ival-fmod: 56.0ms (12.6% of total)

adjust: 34.0ms (7.7% of total)

ival-mult: 33.0ms (7.4% of total)

ival-tan: 18.0ms (4.1% of total)

ival-sqrt: 18.0ms (4.1% of total)

ival-sin: 16.0ms (3.6% of total)

ival-add: 11.0ms (2.5% of total)

ival-neg: 10.0ms (2.3% of total)

ival-div: 8.0ms (1.8% of total)

ival-pow: 8.0ms (1.8% of total)

ival-true: 3.0ms (0.7% of total)

ival-assert: 2.0ms (0.5% of total)

ival-sub: 2.0ms (0.5% of total)

ival-pow2: 2.0ms (0.5% of total)

ival-acos: 2.0ms (0.5% of total)

exact: 0.0ms (0% of total)

start1.0ms (0%)

Memory: 1.6MiB live, 1.6MiB allocated; 0ms collecting garbage

end0.0ms (0%)

Memory: 0.2MiB live, 0.2MiB allocated; 0ms collecting garbage

sample45.4s (53.4%)

rewrite10.5s (12.4%)

regimes4.9s (5.7%)

preprocess4.1s (4.8%)

analyze3.5s (4.1%)

series3.2s (3.8%)

eval3.1s (3.7%)

derivations3.1s (3.7%)

explain3.1s (3.6%)

prune2.1s (2.5%)

simplify1.1s (1.3%)

bsearch846.0ms (1%)

start1.0ms (0%)

end0.0ms (0%)

Profiling