Metrics for Herbie run

Date:	Thursday, April 3rd, 2025
Commit:	f7a7cb35 on main
Seed:	2025093
Parameters:	256 points for 4 iterations
Flags:	`reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofs` default
Memory:	1 064 648.4 MB

sample5.0min (35.3%)

Memory

2 022.2MiB live, 355 938.9MiB allocated; 2.0min collecting garbage

Samples

2.7min	2 144 301×	0	valid
16.9s	69 852×	1	valid
12.3s	63 292×	0	invalid
7.0s	6 016×	2	valid
686.0ms	1 222×	5	exit
310.0ms	1 839×	1	invalid
237.0ms	401×	4	exit
198.0ms	694×	3	valid
3.0ms	25×	1	exit
0.0ms	1×	4	valid

Precisions

Click to see histograms. Total time spent on operations: 1.7min

ival-mult!: 31.6s (31.7% of total)

ival-div!: 18.1s (18.1% of total)

ival-sub!: 10.0s (10% of total)

ival-add!: 9.4s (9.4% of total)

ival-log: 7.9s (8% of total)

ival-cos: 6.2s (6.3% of total)

ival-sqrt: 5.3s (5.3% of total)

ival-sin: 3.9s (4% of total)

adjust: 3.7s (3.7% of total)

ival-exp: 2.0s (2% of total)

ival-tan: 291.0ms (0.3% of total)

ival-acos: 277.0ms (0.3% of total)

ival-fabs: 249.0ms (0.2% of total)

ival-cosh: 248.0ms (0.2% of total)

ival-hypot: 185.0ms (0.2% of total)

ival-sinh: 161.0ms (0.2% of total)

ival-tanh: 139.0ms (0.1% of total)

const: 0.0ms (0% of total)

Bogosity

rewrite3.1min (21.7%)

Memory

5 947.7MiB live, 210 803.6MiB allocated; 49.8s collecting garbage

Stop Event

2 230×	iter-limit
854×	node-limit
69×	unsound
12×	saturated

Counts

126 091 → 226 326

derivations1.1min (7.6%)

Memory

-1 373.6MiB live, 62 304.5MiB allocated; 13.1s collecting garbage

Stop Event

149×	fuel
120×	done

Compiler

Compiled 149 197 to 18 753 computations (87.4% saved)

regimes1.1min (7.6%)

Memory

503.6MiB live, 99 751.5MiB allocated; 17.9s collecting garbage

Counts

33 664 → 4 891

Calls

512 calls:

9.6s	y
8.7s	x
7.8s	z
4.0s	t
2.3s	a

Compiler

Compiled 37 880 to 57 160 computations (-50.9% saved)

series50.9s (6%)

Memory

1 804.6MiB live, 74 630.0MiB allocated; 14.8s collecting garbage

Counts

18 942 → 107 149

Calls

8919 calls:

Time	Variable		Point	Expression
2.4s	z	@	-inf	((* (+ (* (sqrt z) y) x) 1/2) (+ (* (sqrt z) y) x) (* (+ (* (/ y x) (sqrt z)) 1) x) (+ (* (/ y x) (sqrt z)) 1) (/ y x) y x (sqrt z) z 1 1/2 (* (/ 1 2) (+ x (* y (sqrt z)))) (* (+ (* (/ (* (sqrt z) y) x) 1/2) 1/2) x) (+ (* (/ (* (sqrt z) y) x) 1/2) 1/2) (* (/ (* (sqrt z) y) x) 1/2) (/ (* (sqrt z) y) x) (* (sqrt z) y) (* (/ 1 2) (+ x (* y (sqrt z)))) (* (* 1/2 (+ (* (/ 1 (sqrt z)) y) (/ x z))) z) (* 1/2 (+ (* (/ 1 (sqrt z)) y) (/ x z))) (+ (* (/ 1 (sqrt z)) y) (/ x z)) (/ (+ (* (sqrt z) y) x) z) (+ (* (sqrt z) y) x) (* (/ 1 2) (+ x (* y (sqrt z)))) (* (* 1/2 (+ (* (sqrt (pow z -1)) y) (/ x z))) z) (* 1/2 (+ (* (sqrt (pow z -1)) y) (/ x z))) (+ (* (sqrt (pow z -1)) y) (/ x z)) (sqrt (pow z -1)) (pow z -1) -1 (/ x z) (* (/ (+ (pow x 3) (pow (* (sqrt z) y) 3)) (+ (* x x) (- (* (* (sqrt z) y) (* (sqrt z) y)) (* x (* (sqrt z) y))))) 1/2) (/ (+ (pow x 3) (pow (* (sqrt z) y) 3)) (+ (* x x) (- (* (* (sqrt z) y) (* (sqrt z) y)) (* x (* (sqrt z) y))))) (+ (pow x 3) (pow (* (sqrt z) y) 3)) (pow x 3) 3 (pow (* (sqrt z) y) 3) (+ (* x x) (- (* (* (sqrt z) y) (* (sqrt z) y)) (* x (* (sqrt z) y)))) (- (* (* (sqrt z) y) (* (sqrt z) y)) (* x (* (sqrt z) y))) (* (* (sqrt z) y) (* (sqrt z) y)) (* x (* (sqrt z) y)))
515.0ms	x	@	-inf	((- (- (+ (+ (* (* a t) -4) (* b c)) (* (* (* 18 (* x y)) t) z)) (* (* x 4) i)) (* (* j 27) k)) (- (+ (+ (* (* a t) -4) (* b c)) (* (* (* 18 (* x y)) t) z)) (* (* x 4) i)) (+ (+ (* (* a t) -4) (* b c)) (* (* (* 18 (* x y)) t) z)) (+ (* (* a t) -4) (* b c)) (* a t) a t -4 (* b c) b c (* (* (* 18 (* x y)) t) z) (* (* 18 (* x y)) t) (* 18 (* x y)) 18 (* x y) x y z (* (* x 4) i) (* x 4) 4 i (* (* j 27) k) (* j 27) j 27 k (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (* (* -27 j) k) (* -27 j) -27 (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (* (+ (* (* 18 t) (* z y)) (* -4 i)) x) (+ (* (* 18 t) (* z y)) (* -4 i)) (* (* (* z t) 18) y) (* (* z t) 18) (* z t) (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (* (+ (* (* (* z y) x) 18) (* -4 a)) t) (+ (* (* (* z y) x) 18) (* -4 a)) (* (* z y) x) (* z y) (* -4 a) (- (- (+ (- (* (* (* (* x 18) y) z) t) (* (* a 4) t)) (* b c)) (* (* x 4) i)) (* (* j 27) k)) (- (* c b) (+ (* 4 (+ (* a t) (* i x))) (* (* k j) 27))) (* c b) (+ (* 4 (+ (* a t) (* i x))) (* (* k j) 27)) (+ (* a t) (* i x)) (* i x) (* (* k j) 27) (* k j))
255.0ms	z	@	0	((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (log (+ y x))) (log z)) t) (+ (+ (* (log t) (- a 1/2)) (log (+ y x))) (log z)) (+ (* (log t) (- a 1/2)) (log (+ y x))) (log t) t (- a 1/2) a 1/2 (log (+ y x)) (+ y x) y x (log z) z (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) (* (log t) a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* x z) (pow t (- a 1/2)))) t) (+ (* (log t) (- a 1/2)) (log (* z x))) (log (* z x)) (* z x) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* (pow t (- a 1/2)) z) y)) t) (log (* (* (pow t (- a 1/2)) z) y)) (* (* (pow t (- a 1/2)) z) y) (* (pow t (- a 1/2)) z) (pow t (- a 1/2)) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (- (+ (* (* (neg (log t)) (/ (- a 1/2) t)) -1) (/ (log (* (+ y x) z)) t)) 1) t) (- (+ (* (* (neg (log t)) (/ (- a 1/2) t)) -1) (/ (log (* (+ y x) z)) t)) 1) (+ (* (* (neg (log t)) (/ (- a 1/2) t)) -1) (/ (log (* (+ y x) z)) t)) (* (neg (log t)) (/ (- a 1/2) t)) (neg (log t)) (/ (- a 1/2) t) -1 (/ (log (* (+ y x) z)) t) (log (* (+ y x) z)) (* (+ y x) z) 1)
187.0ms	y	@	0	((* x (/ (* (log (/ x y)) (log (* y x))) (log (* y x)))) x (/ (* (log (/ x y)) (log (* y x))) (log (* y x))) (* (log (/ x y)) (log (* y x))) (log (/ x y)) (/ x y) y (log (* y x)) (* y x) (log (pow (/ x y) x)) (pow (/ x y) x) (+ (* (* (neg x) (log (neg x))) -1) (* (neg (neg (log (/ -1 y)))) x)) (* (neg x) (log (neg x))) (neg x) (log (neg x)) -1 (* (neg (neg (log (/ -1 y)))) x) (neg (neg (log (/ -1 y)))) (neg (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) (* x (log (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (exp (* (log x) 1/2)))))) (log (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (exp (* (log x) 1/2))))) (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (exp (* (log x) 1/2)))) (* (pow y -1/2) (pow x 1/2)) (pow y -1/2) -1/2 (pow x 1/2) 1/2 (* (pow y -1/2) (exp (* (log x) 1/2))) (exp (* (log x) 1/2)) (* (log x) 1/2) (log x) (/ (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2))) (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (pow (log (neg x)) 3) 3 (pow (log (/ -1 y)) 3) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2)) (log (* x y)) (* x y) (pow (log (/ -1 y)) 2) 2)
177.0ms	a	@	-inf	((/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) (* (- (+ (/ (+ t y) (+ (+ y x) t)) (* (/ z a) (/ (+ y x) (+ (+ y x) t)))) (* (/ b a) (/ y (+ (+ y x) t)))) a) (- (+ (/ (+ t y) (+ (+ y x) t)) (* (/ z a) (/ (+ y x) (+ (+ y x) t)))) (* (/ b a) (/ y (+ (+ y x) t)))) (+ (/ (+ t y) (+ (+ y x) t)) (* (/ z a) (/ (+ y x) (+ (+ y x) t)))) (/ (+ t y) (+ (+ y x) t)) (+ t y) t y (+ (+ y x) t) (+ y x) x (* (/ z a) (/ (+ y x) (+ (+ y x) t))) (/ z a) z a (/ (+ y x) (+ (+ y x) t)) (* (/ b a) (/ y (+ (+ y x) t))) (/ b a) b (/ y (+ (+ y x) t)) (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (* (+ t y) a) (+ (+ x t) y) (+ x t) (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) (+ (* (/ (* -1 (- (+ (* (+ t y) a) (* z y)) (+ (* (+ t y) z) (* b y)))) x) -1) z) (/ (* -1 (- (+ (* (+ t y) a) (* z y)) (+ (* (+ t y) z) (* b y)))) x) (* -1 (- (+ (* (+ t y) a) (* z y)) (+ (* (+ t y) z) (* b y)))) -1 (- (+ (* (+ t y) a) (* z y)) (+ (* (+ t y) z) (* b y))) (+ (* (+ t y) a) (* z y)) (* z y) (+ (* (+ t y) z) (* b y)) (* b y) (+ (* (/ (+ y x) (+ (+ y x) t)) z) (/ (+ (* (+ t y) a) (* (neg b) y)) (+ (+ y x) t))) (/ (+ (* (+ t y) a) (* (neg b) y)) (+ (+ y x) t)) (+ (* (+ t y) a) (* (neg b) y)) (* (neg b) y) (neg b))

eval43.4s (5.1%)

Memory: -1 044.7MiB live, 66 784.9MiB allocated; 15.6s collecting garbage
Compiler: Compiled 9 489 328 to 1 002 106 computations (89.4% saved)

explain40.2s (4.8%)

Memory

48.3MiB live, 53 901.7MiB allocated; 13.6s collecting garbage

Explanations

Click to see full explanations table

Operator	Subexpression	Explanation	Count
`log.f64`	`#f`	sensitivity	1585	2
`/.f64`	`#f`	o/n	1196	0
`sqrt.f64`	`#f`	oflow-rescue	750	0
`-.f64`	`#f`	cancellation	577	9
`/.f64`	`#f`	o/o	562	0
`*.f64`	`#f`	*no**	504	0
`+.f64`	`#f`	nan-rescue	461	0
`-.f64`	`#f`	nan-rescue	426	0
`cos.f64`	`#f`	sensitivity	355	1
`+.f64`	`#f`	cancellation	337	0
`/.f64`	`#f`	n/o	321	0
`/.f64`	`#f`	u/n	272	0
`sin.f64`	`#f`	sensitivity	231	0
`*.f64`	`#f`	*nu**	225	0
`/.f64`	`#f`	n/u	151	0
`cos.f64`	`#f`	oflow-rescue	128	0
`/.f64`	`#f`	u/u	107	0
`tan.f64`	`(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))`	sensitivity	94	0
`log.f64`	`#f`	oflow-rescue	82	0
`log.f64`	`#f`	uflow-rescue	55	0
`sqrt.f64`	`#f`	uflow-rescue	48	0
`*.f64`	`#f`	*ou**	34	0
`tan.f64`	`(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))`	oflow-rescue	31	0
↳	`(/.f64 x (*.f64 y #s(literal 2 binary64)))`	overflow	31
`sin.f64`	`(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))`	oflow-rescue	31	0
↳	`(/.f64 x (*.f64 y #s(literal 2 binary64)))`	overflow	31
`exp.f64`	`#f`	sensitivity	30	5

Confusion

	Predicted +	Predicted -
+	5967	214
-	1760	60923

Precision

0.772227255079591

Recall

0.9653777705872836

Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	5967	2	212
-	1760	17	60906

Precision?

0.7705912729150529

Recall?

0.9657013428247856

Freqs

test

number	freq
0	61137
1	6947
2	715
3	49
4	12
5	3
6	1

Total Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	134	0	0
-	1	2	132

Precision?

0.9781021897810219

Recall?

1.0

Samples

9.9s	130 446×	0	valid
1.6s	5 850×	1	valid
1.0s	1 328×	2	valid
28.0ms	98×	3	valid
2.0ms	6×	4	valid

Compiler

Compiled 24 442 to 8 402 computations (65.6% saved)

Precisions

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

ival-mult!: 2.0s (31.7% of total)

ival-log: 1.2s (18.5% of total)

ival-div!: 909.0ms (14.5% of total)

ival-sub!: 543.0ms (8.7% of total)

ival-add!: 494.0ms (7.9% of total)

adjust: 295.0ms (4.7% of total)

ival-sqrt: 216.0ms (3.4% of total)

ival-sin: 198.0ms (3.2% of total)

ival-cos: 185.0ms (3% of total)

ival-fabs: 128.0ms (2% of total)

ival-exp: 91.0ms (1.5% of total)

ival-cosh: 16.0ms (0.3% of total)

ival-tan: 12.0ms (0.2% of total)

ival-sinh: 11.0ms (0.2% of total)

ival-hypot: 9.0ms (0.1% of total)

ival-tanh: 8.0ms (0.1% of total)

ival-acos: 5.0ms (0.1% of total)

preprocess36.0s (4.3%)

Memory

-1 016.9MiB live, 45 067.7MiB allocated; 8.6s collecting garbage

Stop Event

174×	node-limit
95×	saturated

Compiler

Compiled 496 020 to 135 170 computations (72.7% saved)

bsearch26.7s (3.2%)

Memory

513.0MiB live, 37 545.6MiB allocated; 6.5s collecting garbage

Algorithm

1 725×	binary-search
1 078×	left-value

Stop Event

1 685×	narrow-enough
40×	predicate-same

Samples

12.9s	142 525×	0	valid
946.0ms	4 206×	1	valid
187.0ms	2 490×	0	invalid
22.0ms	156×	2	valid
6.0ms	31×	1	invalid
1.0ms	9×	3	valid

Compiler

Compiled 907 307 to 659 851 computations (27.3% saved)

Precisions

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

ival-mult!: 3.7s (45.7% of total)

ival-sub!: 1.2s (15.1% of total)

ival-add!: 820.0ms (10.1% of total)

ival-div!: 625.0ms (7.7% of total)

ival-log: 488.0ms (6% of total)

ival-sin: 456.0ms (5.6% of total)

ival-cos: 346.0ms (4.3% of total)

adjust: 218.0ms (2.7% of total)

ival-sqrt: 120.0ms (1.5% of total)

ival-exp: 92.0ms (1.1% of total)

ival-cosh: 9.0ms (0.1% of total)

ival-sinh: 9.0ms (0.1% of total)

ival-tanh: 4.0ms (0% of total)

ival-tan: 3.0ms (0% of total)

ival-fabs: 3.0ms (0% of total)

prune21.2s (2.5%)

Memory: 374.4MiB live, 36 618.4MiB allocated; 6.5s collecting garbage
Counts: 254 577 → 12 769
Compiler: Compiled 802 168 to 442 208 computations (44.9% saved)

analyze16.7s (2%)

Memory

-153.2MiB live, 21 277.0MiB allocated; 6.1s collecting garbage

Algorithm

269×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	99.9%	0.1%	0%	0%	0%	0
46.8%	46.8%	53.1%	0.1%	0%	0%	0%	1
50.5%	50.1%	49.2%	0.1%	0%	0.6%	0%	2
58.6%	57%	40.3%	0.1%	0%	2.6%	0%	3
65.2%	62.7%	33.5%	0.1%	0%	3.6%	0%	4
71.2%	68.2%	27.5%	0.1%	0%	4.1%	0%	5
75.9%	72.3%	23%	0.1%	0%	4.6%	0%	6
79.8%	75.6%	19.1%	0.1%	0%	5.1%	0%	7
81.7%	77%	17.3%	0.1%	0%	5.6%	0%	8
84.3%	79.3%	14.7%	0.1%	0%	5.9%	0%	9
85.9%	80.5%	13.2%	0.1%	0%	6.2%	0%	10
88.5%	82.8%	10.8%	0.1%	0%	6.2%	0%	11
89.6%	83.6%	9.8%	0.1%	0%	6.5%	0%	12

Compiler

Compiled 3 462 to 2 977 computations (14% saved)

start17.0ms (0%)

Memory: -25.5MiB live, 19.3MiB allocated; 9ms collecting garbage

end7.0ms (0%)

Memory: -44.3MiB live, 5.1MiB allocated; 9ms collecting garbage

sample5.0min (35.3%)

rewrite3.1min (21.7%)

derivations1.1min (7.6%)

regimes1.1min (7.6%)

series50.9s (6%)

eval43.4s (5.1%)

explain40.2s (4.8%)

preprocess36.0s (4.3%)

bsearch26.7s (3.2%)

prune21.2s (2.5%)

analyze16.7s (2%)

start17.0ms (0%)

end7.0ms (0%)

Profiling