Herbie run

Date:Sunday, January 26th, 2025
Commit:c1ce189f on fix-derivation-reports
Seed:2025026
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:1 628 985.9 MB

Time bar (total: 24.7min)

sample6.5min (26.5%)

Memory
4 540.1MiB live, 448 322.1MiB allocated; 2.3min collecting garbage
Samples
3.8min2 144 861×0valid
27.5s69 618×1valid
11.2s63 839×0invalid
1.8s5 739×2valid
1.7s1 642×5exit
652.0ms1 859×1invalid
188.0ms645×3valid
0.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 2.7min
ival-mult: 52.6s (32.5% of total)
ival-sub: 20.7s (12.8% of total)
ival-add: 20.5s (12.6% of total)
ival-div: 19.9s (12.3% of total)
ival-log: 11.4s (7.1% of total)
adjust: 9.7s (6% of total)
const: 6.9s (4.3% of total)
ival-sqrt: 5.3s (3.3% of total)
ival-sin: 3.9s (2.4% of total)
ival-cos: 3.5s (2.1% of total)
ival-exp: 2.0s (1.2% of total)
ival-true: 1.6s (1% of total)
exact: 1.1s (0.7% of total)
ival-assert: 864.0ms (0.5% of total)
ival-fabs: 351.0ms (0.2% of total)
ival-hypot: 326.0ms (0.2% of total)
ival-acos: 293.0ms (0.2% of total)
ival-tan: 286.0ms (0.2% of total)
ival-cosh: 256.0ms (0.2% of total)
ival-sinh: 218.0ms (0.1% of total)
ival-tanh: 132.0ms (0.1% of total)
Bogosity

simplify5.8min (23.7%)

Memory
3 711.1MiB live, 356 246.5MiB allocated; 1.5min collecting garbage
Stop Event
2 818×iter limit
1 847×node limit
280×saturated
unsound
Counts
93 739 → 93 739

rewrite2.2min (9%)

Memory
664.5MiB live, 131 638.5MiB allocated; 42.2s collecting garbage
Stop Event
2 707×iter limit
742×node limit
180×unsound
11×saturated
Counts
11 508 → 174 746

derivations1.8min (7.4%)

Memory
-2 971.8MiB live, 79 184.3MiB allocated; 24.7s collecting garbage
Stop Event
156×fuel
113×done
Compiler

Compiled 139 486 to 18 984 computations (86.4% saved)

localize1.7min (7%)

Memory
283.2MiB live, 129 052.8MiB allocated; 26.6s collecting garbage
Samples
57.5s218 690×0valid
12.3s11 192×1valid
5.8s3 172×2valid
1.9s3 310×0invalid
1.2s214×5exit
609.0ms989×0exit
191.0ms209×3valid
56.0ms22×1exit
48.0ms26×4valid
Compiler

Compiled 140 544 to 22 258 computations (84.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 54.3s
ival-mult: 17.8s (32.8% of total)
ival-add: 8.3s (15.2% of total)
ival-div: 7.5s (13.7% of total)
ival-sub: 4.0s (7.3% of total)
adjust: 3.5s (6.5% of total)
const: 2.7s (4.9% of total)
ival-log: 2.5s (4.6% of total)
ival-sin: 2.0s (3.6% of total)
ival-pow: 1.5s (2.8% of total)
ival-neg: 967.0ms (1.8% of total)
ival-cos: 856.0ms (1.6% of total)
ival-sqrt: 779.0ms (1.4% of total)
ival-exp: 537.0ms (1% of total)
ival-pow2: 411.0ms (0.8% of total)
exact: 225.0ms (0.4% of total)
ival-true: 184.0ms (0.3% of total)
ival-log1p: 134.0ms (0.2% of total)
ival-assert: 112.0ms (0.2% of total)
ival-sinh: 102.0ms (0.2% of total)
ival-expm1: 91.0ms (0.2% of total)
ival-cosh: 75.0ms (0.1% of total)
ival-hypot: 32.0ms (0.1% of total)
ival-tan: 22.0ms (0% of total)
ival-acos: 20.0ms (0% of total)
ival-fabs: 16.0ms (0% of total)
ival-tanh: 14.0ms (0% of total)
ival-pi: 14.0ms (0% of total)
ival->: 1.0ms (0% of total)
ival-then: 0.0ms (0% of total)

regimes1.3min (5.4%)

Memory
81.1MiB live, 94 430.4MiB allocated; 26.6s collecting garbage
Counts
33 632 → 4 979
Calls

510 calls:

9.7s
x
9.0s
y
7.8s
z
4.3s
t
2.7s
a
Compiler

Compiled 37 299 to 55 969 computations (-50.1% saved)

preprocess1.1min (4.6%)

Memory
3 917.6MiB live, 74 487.7MiB allocated; 14.6s collecting garbage
Stop Event
538×iter limit
341×node limit
197×saturated
Compiler

Compiled 316 366 to 61 950 computations (80.4% saved)

series56.3s (3.8%)

Memory
399.2MiB live, 70 852.5MiB allocated; 18.0s collecting garbage
Counts
11 508 → 93 739
Calls

8928 calls:

TimeVariablePointExpression
2.5s
t
@0
((- (/ (+ (* (+ (* (neg t) a) (* z y)) x) (* (+ (* (neg z) b) (* j t)) c)) i) (* (neg b) a)) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))) (* (+ (* (neg j) y) (- (/ (+ (* (+ (* (neg t) a) (* z y)) x) (* (+ (* (neg z) b) (* j t)) c)) i) (* (neg b) a))) i) (+ (* (neg j) y) (- (/ (+ (* (+ (* (neg t) a) (* z y)) x) (* (+ (* (neg z) b) (* j t)) c)) i) (* (neg b) a))) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))) (* (+ (* (neg a) x) (* j c)) t) (+ (* (neg a) x) (* j c)) (neg a) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))) (* (+ (* (neg t) a) (* z y)) x) (+ (* (neg t) a) (* z y)) (neg t) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))) (* (+ (* (neg z) c) (* i a)) b) (+ (* (neg z) c) (* i a)) (neg z) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))) (+ (* (+ (* (neg t) a) (* z y)) x) (* (+ (* (neg y) j) (* b a)) i)) (* (+ (* (neg z) b) (* j t)) c) (/ (+ (* (+ (* (neg t) a) (* z y)) x) (* (+ (* (neg z) b) (* j t)) c)) i) (+ (* (+ (* (neg t) a) (* z y)) x) (* (+ (* (neg z) b) (* j t)) c)) (* (+ (* (neg y) j) (* b a)) i) (+ (* (neg y) j) (* b a)))
356.0ms
x
@0
((- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (+ (* (/ (neg x) t) (/ (log (+ 1 (* y (- (exp z) 1)))) x)) x) (/ (neg x) t) (neg x) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (+ (* (- (* (/ (* (- y (* y y)) z) t) -1/2) (/ y t)) z) x) (- (* (/ (* (- y (* y y)) z) t) -1/2) (/ y t)) (/ (neg y) t) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (* (/ (+ (* (* -1/2 z) (+ (* y y) (neg y))) y) t) z) (* (* y z) (/ (+ (* 1/2 z) 1) t)) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (* (* (+ (* z (+ (* -1/2 y) 1/2)) 1) y) z) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (* (/ (- (exp z) 1) t) y) (/ (- (exp z) 1) t) (/ (log (+ 1 (* y (- (exp z) 1)))) x) (log (+ 1 (* y (- (exp z) 1)))) (* y (- (exp z) 1)) (neg y) (* (+ (* z (+ (* -1/2 y) 1/2)) 1) y))
327.0ms
y
@-inf
((* x (- (/ (pow (log (neg x)) 3) (+ (* (log (neg y)) (log (* (neg x) (neg y)))) (pow (log (neg x)) 2))) (/ (pow (log (neg y)) 3) (+ (* (log (neg y)) (log (* (neg x) (neg y)))) (pow (log (neg x)) 2))))) (- (/ (pow (log (neg x)) 3) (+ (* (log (neg y)) (log (* (neg x) (neg y)))) (pow (log (neg x)) 2))) (/ (pow (log (neg y)) 3) (+ (* (log (neg y)) (log (* (neg x) (neg y)))) (pow (log (neg x)) 2)))) (/ (+ (pow (log (/ -1 y)) 3) (pow (log (neg x)) 3)) (+ (* (log (/ -1 y)) (- (log (/ -1 y)) (log (neg x)))) (pow (log (neg x)) 2))) (+ (pow (log (/ -1 y)) 3) (pow (log (neg x)) 3)) (log (pow (/ x y) x)) (pow (/ x y) x) (/ x y) (* (- (pow (log x) 2) (pow (log y) 2)) (/ x (+ (log y) (log x)))) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) (log x) (* (neg y) (neg x)) (/ (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (+ (* (log (* (neg y) (neg x))) (log (neg y))) (pow (log (neg x)) 2))) (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) (* x (* (/ (- (pow (log x) 2) (pow (log y) 2)) (+ (pow (log y) 3) (pow (log x) 3))) (+ (* (log y) (- (log y) (log x))) (pow (log x) 2)))) (* (/ (- (pow (log x) 2) (pow (log y) 2)) (+ (pow (log y) 3) (pow (log x) 3))) (+ (* (log y) (- (log y) (log x))) (pow (log x) 2))) (/ (- (pow (log x) 2) (pow (log y) 2)) (+ (pow (log y) 3) (pow (log x) 3))) (log (neg x)) (log (/ -1 y)) (neg x) (log y) (+ (log y) (log x)) (log (neg y)) (log (* (neg y) (neg x))))
260.0ms
x
@0
((- (* x (log (/ x y))) z) (+ (* (log (/ x y)) x) (neg z)) (log (/ x y)) (/ x y) (- (* x (log (/ x y))) z) (neg z) (- (* x (- (log (neg x)) (log (neg y)))) z) (* x (- (log (neg x)) (log (neg y)))) (- (log (neg x)) (log (neg y))) (log (neg x)) (- (* x (/ (- (pow (log x) 2) (pow (log y) 2)) (log (* y x)))) z) (* x (/ (- (pow (log x) 2) (pow (log y) 2)) (log (* y x)))) (/ (- (pow (log x) 2) (pow (log y) 2)) (log (* y x))) (- (pow (log x) 2) (pow (log y) 2)) (- (/ (pow (log (neg x)) 2) (log (* (neg x) (neg y)))) (/ (pow (log (neg y)) 2) (log (* (neg x) (neg y))))) (* (neg x) (neg y)) (- (* x (- (/ (pow (log (neg x)) 2) (log (* (neg x) (neg y)))) (/ (pow (log (neg y)) 2) (log (* (neg x) (neg y)))))) z) (* x (- (/ (pow (log (neg x)) 2) (log (* (neg x) (neg y)))) (/ (pow (log (neg y)) 2) (log (* (neg x) (neg y)))))) (log (neg y)) (neg x) (neg y) (log x) (log y) (log (* y x)) (log (* (neg x) (neg y))))
213.0ms
y
@inf
((/ (/ x (- y z)) (- t z)) (/ x (- y z)) (- y z) (- t z) (/ x (* (- y z) (- t z))) (* (- y z) (- t z)) (* z z) (/ x (* (- y z) (- t z))) (* (- y z) (- t z)) (- t z) (/ x (* (- y z) (- t z))) (/ (/ x (- y z)) t) (/ x (* (- y z) (- t z))) (* (- y z) (- t z)) (+ (* (- (neg y) t) z) (* y t)) (- (neg y) t) (neg y))

eval50.9s (3.4%)

Memory
-1 291.1MiB live, 69 134.8MiB allocated; 18.0s collecting garbage
Compiler

Compiled 10 462 202 to 1 024 690 computations (90.2% saved)

explain48.5s (3.3%)

Memory
-734.8MiB live, 61 759.6MiB allocated; 15.2s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15298
/.f64#fo/n11810
sqrt.f64#foflow-rescue7750
-.f64#fcancellation5917
/.f64#fo/o5490
*.f64#fn*o5100
+.f64#fnan-rescue4610
-.f64#fnan-rescue4430
cos.f64#fsensitivity3602
+.f64#fcancellation3243
/.f64#fn/o3150
/.f64#fu/n2480
sin.f64#fsensitivity2050
*.f64#fn*u1950
cos.f64#foflow-rescue1420
/.f64#fn/u1190
log.f64#foflow-rescue1030
/.f64#fu/u1020
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity790
log.f64#fuflow-rescue760
sqrt.f64#fuflow-rescue430
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue340
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow34
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue340
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow34
exp.f64#fsensitivity305
*.f64(*.f64 (cosh.f64 x) (/.f64 y x))o*u210
(cosh.f64 x)overflow127
(/.f64 y x)underflow21
*.f64(*.f64 (*.f64 (-.f64 (*.f64 x #s(literal 1/2 binary64)) y) (sqrt.f64 (*.f64 z #s(literal 2 binary64)))) (exp.f64 (/.f64 (*.f64 t t) #s(literal 2 binary64))))u*o40
(*.f64 (-.f64 (*.f64 x #s(literal 1/2 binary64)) y) (sqrt.f64 (*.f64 z #s(literal 2 binary64))))underflow6
(exp.f64 (/.f64 (*.f64 t t) #s(literal 2 binary64)))overflow131
(/.f64 (*.f64 t t) #s(literal 2 binary64))overflow65
(*.f64 t t)overflow65
Confusion
Predicted +Predicted -
+5922183
-168961070
Precision
0.7780843515963737
Recall
0.97002457002457
Confusion?
Predicted +Predicted MaybePredicted -
+59225178
-16891961051
Precision?
0.7762933857236411
Recall?
0.9708435708435709
Freqs
test
numberfreq
061253
16849
2687
357
414
51
63
Total Confusion?
Predicted +Predicted MaybePredicted -
+14200
-10126
Precision?
0.993006993006993
Recall?
1.0
Samples
13.8s130 522×0valid
2.4s5 892×1valid
808.0ms1 224×2valid
32.0ms88×3valid
1.0ms5exit
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 10.1s
ival-mult: 2.9s (28.7% of total)
ival-add: 1.5s (14.5% of total)
ival-div: 1.4s (13.5% of total)
ival-sub: 1.2s (11.5% of total)
ival-log: 788.0ms (7.8% of total)
adjust: 627.0ms (6.2% of total)
ival-cos: 412.0ms (4.1% of total)
const: 364.0ms (3.6% of total)
ival-sin: 314.0ms (3.1% of total)
ival-sqrt: 211.0ms (2.1% of total)
ival-exp: 191.0ms (1.9% of total)
ival-true: 114.0ms (1.1% of total)
exact: 66.0ms (0.7% of total)
ival-assert: 54.0ms (0.5% of total)
ival-tan: 15.0ms (0.1% of total)
ival-hypot: 15.0ms (0.1% of total)
ival-cosh: 12.0ms (0.1% of total)
ival-fabs: 11.0ms (0.1% of total)
ival-sinh: 10.0ms (0.1% of total)
ival-acos: 8.0ms (0.1% of total)
ival-tanh: 6.0ms (0.1% of total)

bsearch37.3s (2.5%)

Memory
699.2MiB live, 44 285.2MiB allocated; 10.5s collecting garbage
Algorithm
1 764×binary-search
1 119×left-value
Stop Event
1 736×narrow-enough
28×predicate-same
Samples
19.9s142 826×0valid
1.2s3 695×1valid
240.0ms2 629×0invalid
42.0ms192×2valid
11.0ms42×1invalid
6.0ms23×3valid
Compiler

Compiled 891 437 to 656 135 computations (26.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.0s
ival-mult: 5.1s (39.6% of total)
ival-sub: 2.3s (17.8% of total)
ival-add: 1.5s (11.5% of total)
ival-div: 1.2s (9.4% of total)
const: 668.0ms (5.1% of total)
ival-log: 613.0ms (4.7% of total)
ival-sin: 428.0ms (3.3% of total)
ival-cos: 290.0ms (2.2% of total)
adjust: 267.0ms (2.1% of total)
ival-exp: 162.0ms (1.2% of total)
ival-sqrt: 116.0ms (0.9% of total)
ival-true: 106.0ms (0.8% of total)
exact: 59.0ms (0.5% of total)
ival-assert: 57.0ms (0.4% of total)
ival-fabs: 21.0ms (0.2% of total)
ival-cosh: 17.0ms (0.1% of total)
ival-sinh: 11.0ms (0.1% of total)
ival-tanh: 10.0ms (0.1% of total)

prune26.2s (1.8%)

Memory
-571.8MiB live, 40 477.2MiB allocated; 6.9s collecting garbage
Counts
258 988 → 12 819
Compiler

Compiled 803 010 to 437 600 computations (45.5% saved)

analyze25.8s (1.7%)

Memory
-304.9MiB live, 29 084.3MiB allocated; 11.3s collecting garbage
Algorithm
269×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
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)

start10.0ms (0%)

Memory
24.9MiB live, 24.4MiB allocated; 0ms collecting garbage

end2.0ms (0%)

Memory
5.8MiB live, 5.5MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...