Herbie run

Date:Sunday, January 26th, 2025
Commit:c73a45c1 on main
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:36 895.2 MB

Time bar (total: 39.3s)

sample11.4s (28.9%)

Memory
231.7MiB live, 11 892.9MiB allocated; 5.0s collecting garbage
Samples
6.5s70 133×0valid
1.2s4 166×2valid
216.0ms1 902×0invalid
0.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 5.4s
ival-div: 1.5s (28.3% of total)
ival-mult: 1.5s (27.3% of total)
ival-sqrt: 639.0ms (11.9% of total)
ival-sub: 637.0ms (11.8% of total)
ival-neg: 313.0ms (5.8% of total)
adjust: 224.0ms (4.2% of total)
ival-add: 150.0ms (2.8% of total)
ival-exp: 124.0ms (2.3% of total)
ival-fabs: 105.0ms (2% of total)
ival-log: 92.0ms (1.7% of total)
exact: 64.0ms (1.2% of total)
ival-assert: 28.0ms (0.5% of total)
ival-if: 9.0ms (0.2% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

simplify10.7s (27.1%)

Memory
-10.5MiB live, 8 412.6MiB allocated; 1.2s collecting garbage
Stop Event
85×iter limit
64×node limit
saturated
Counts
3 090 → 3 090

localize3.8s (9.8%)

Memory
-41.5MiB live, 3 888.9MiB allocated; 553ms collecting garbage
Samples
1.2s5 543×0valid
879.0ms852×2valid
610.0ms639×1valid
203.0ms134×3valid
Compiler

Compiled 6 779 to 660 computations (90.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.0s
ival-mult: 470.0ms (23.9% of total)
ival-div: 439.0ms (22.3% of total)
adjust: 365.0ms (18.5% of total)
ival-add: 166.0ms (8.4% of total)
ival-sub: 160.0ms (8.1% of total)
ival-fabs: 93.0ms (4.7% of total)
ival-sqrt: 80.0ms (4.1% of total)
ival-if: 47.0ms (2.4% of total)
ival-neg: 45.0ms (2.3% of total)
ival-pow: 36.0ms (1.8% of total)
ival->=: 30.0ms (1.5% of total)
ival-log: 13.0ms (0.7% of total)
exact: 12.0ms (0.6% of total)
ival-true: 6.0ms (0.3% of total)
ival-exp: 5.0ms (0.3% of total)
ival-assert: 3.0ms (0.2% of total)

preprocess2.5s (6.3%)

Memory
77.3MiB live, 1 924.8MiB allocated; 309ms collecting garbage
Stop Event
18×iter limit
16×node limit
saturated
Compiler

Compiled 7 297 to 1 366 computations (81.3% saved)

derivations2.4s (6.1%)

Memory
-33.1MiB live, 1 540.2MiB allocated; 270ms collecting garbage
Stop Event
done
fuel
Compiler

Compiled 3 365 to 490 computations (85.4% saved)

rewrite2.3s (5.8%)

Memory
-77.9MiB live, 2 130.5MiB allocated; 371ms collecting garbage
Stop Event
91×iter limit
18×node limit
10×unsound
saturated
Counts
355 → 4 228

explain1.9s (4.7%)

Memory
107.5MiB live, 1 933.2MiB allocated; 232ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2690
+.f64#fcancellation1241
-.f64#fcancellation1060
sqrt.f64#fuflow-rescue610
/.f64#fu/n300
/.f64#fn/u280
-.f64#fnan-rescue150
*.f64(*.f64 (/.f64 x y) z)n*u90
*.f64(*.f64 (/.f64 x y) z)n*o80
/.f64(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 4 binary64) a) c)))) (*.f64 #s(literal 2 binary64) a))n/o10
(*.f64 #s(literal 2 binary64) a)overflow1
Confusion
Predicted +Predicted -
+28515
-2401764
Precision
0.5428571428571428
Recall
0.95
Confusion?
Predicted +Predicted MaybePredicted -
+285015
-24011763
Precision?
0.5418250950570342
Recall?
0.95
Freqs
test
numberfreq
01779
1408
2108
39
Total Confusion?
Predicted +Predicted MaybePredicted -
+400
-005
Precision?
1.0
Recall?
1.0
Samples
321.0ms3 680×0valid
170.0ms554×2valid
147.0ms304×1valid
38.0ms70×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 467.0ms
ival-div: 131.0ms (28% of total)
ival-mult: 123.0ms (26.3% of total)
adjust: 65.0ms (13.9% of total)
ival-sub: 48.0ms (10.3% of total)
ival-sqrt: 30.0ms (6.4% of total)
ival-add: 17.0ms (3.6% of total)
ival-neg: 11.0ms (2.4% of total)
ival-if: 10.0ms (2.1% of total)
ival-fabs: 7.0ms (1.5% of total)
ival-exp: 6.0ms (1.3% of total)
ival-log: 6.0ms (1.3% of total)
ival-true: 4.0ms (0.9% of total)
exact: 4.0ms (0.9% of total)
ival->=: 3.0ms (0.6% of total)
ival-assert: 2.0ms (0.4% of total)

eval1.2s (3.1%)

Memory
-19.7MiB live, 1 468.4MiB allocated; 193ms collecting garbage
Compiler

Compiled 398 958 to 32 102 computations (92% saved)

series820.0ms (2.1%)

Memory
136.0MiB live, 918.7MiB allocated; 92ms collecting garbage
Counts
355 → 3 090
Calls

174 calls:

TimeVariablePointExpression
56.0ms
x
@-inf
((neg (log (- (/ 1 x) 1))) (log x) (neg (log (- (/ 1 x) 1))) (+ (log x) x) (neg (log (- (/ 1 x) 1))) (+ (* (+ (* 1/2 x) 1) x) (log x)) (+ (* 1/2 x) 1))
44.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) (neg (log (- (/ 1 x) 1))) (+ (log x) x) (neg (log (- (/ 1 x) 1))) (+ (* (+ (* 1/2 x) 1) x) (log x)) (+ (* 1/2 x) 1))
33.0ms
c
@inf
((- (* b b) (* (* 4 a) c)) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (if (>= b 0) (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (* 2 c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b))) (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (- (+ (* (* -4 a) c) (* b b)) (* b b)) (/ (* 2 c) (/ (- (+ (* (* -4 a) c) (* b b)) (* b b)) (- (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)))) (* (pow (+ (* (* -4 a) c) (* b b)) 1/4) (pow (+ (* (* -4 a) c) (* b b)) 1/4)) (/ (- (neg b) (* (pow (+ (* (* -4 a) c) (* b b)) 1/4) (pow (+ (* (* -4 a) c) (* b b)) 1/4))) (* 2 a)) (if (>= b 0) (/ (- (neg b) (* (pow (+ (* (* -4 a) c) (* b b)) 1/4) (pow (+ (* (* -4 a) c) (* b b)) 1/4))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (- (* b b) (* (* 4 a) c))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (+ (* (* -4 a) c) (* b b))) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (sqrt (- (* b b) (* (* 4 a) c))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (- (+ (* (* -4 a) c) (* b b)) (* b b)) (- (sqrt (+ (* (* -4 a) c) (* b b))) (neg b))) (pow (+ (* (* -4 a) c) (* b b)) 1/4) (- (neg b) (* (pow (+ (* (* -4 a) c) (* b b)) 1/4) (pow (+ (* (* -4 a) c) (* b b)) 1/4))))
31.0ms
b
@-inf
((if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (if (>= b 0) (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2)) (>= b 0) (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (* b b) (* (* 4 a) c)) (if (>= b 0) (* c (/ 2 (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (sqrt (+ (* (* -4 a) c) (* b b))) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))
21.0ms
c
@inf
((+ (* (/ b a) -1) (/ c b)) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (+ (* c (/ a b)) (neg b)) a) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (sqrt (- (* b b) (* (* 4 a) c))) (neg b)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (- (* b b) (- (* b b) (* (* 4 a) c))) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) (neg b)) (* 2 a))) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (+ (sqrt (- (* b b) (* (* 4 a) c))) (neg b)) (if (>= b 0) (/ (- (pow (neg b) 3) (pow (sqrt (- (* b b) (* (* 4 a) c))) 3)) (* (+ (* (sqrt (- (* b b) (* (* 4 a) c))) (+ (sqrt (- (* b b) (* (* 4 a) c))) (neg b))) (* b b)) (* 2 a))) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (pow (neg b) 3) (pow (sqrt (- (* b b) (* (* 4 a) c))) 3)) (* (+ (* (sqrt (- (* b b) (* (* 4 a) c))) (+ (sqrt (- (* b b) (* (* 4 a) c))) (neg b))) (* b b)) (* 2 a))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (- (* b b) (* (* 4 a) c)) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (- (* b b) (* (* 4 a) c))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (- (* b b) (* (* 4 a) c))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (pow (neg b) 3) (pow (sqrt (- (* b b) (* (* 4 a) c))) 3)))

regimes769.0ms (2%)

Memory
45.9MiB live, 764.3MiB allocated; 78ms collecting garbage
Counts
468 → 101
Calls

26 calls:

101.0ms
x
87.0ms
z
83.0ms
(fabs.f64 (-.f64 a b))
69.0ms
b
67.0ms
(-.f64 (/.f64 (+.f64 x #s(literal 4 binary64)) y) (*.f64 (/.f64 x y) z))
Compiler

Compiled 945 to 818 computations (13.4% saved)

analyze570.0ms (1.4%)

Memory
137.7MiB live, 742.6MiB allocated; 193ms collecting garbage
Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
22.2%22.2%77.7%0.1%0%0%0%1
29.4%27.8%66.6%0.1%0%5.6%0%2
50%44.4%44.4%0.1%0%11.1%0%3
59.7%51.3%34.7%0.1%0%13.9%0%4
66.4%56.2%28.4%0.1%0%15.3%0%5
74%62.1%21.8%0.1%0%16%0%6
77.6%63.8%18.4%0.1%0%17.7%0%7
79.3%65%17%0.1%0%17.9%0%8
85%69.2%12.2%0.1%0%18.5%0%9
86.8%69.7%10.6%0.1%0%19.6%0%10
88.7%71.1%9.1%0.1%0%19.8%0%11
91.6%72.9%6.7%0.1%0%20.3%0%12
Compiler

Compiled 153 to 106 computations (30.7% saved)

prune562.0ms (1.4%)

Memory
-144.8MiB live, 730.2MiB allocated; 161ms collecting garbage
Counts
7 124 → 250
Compiler

Compiled 19 196 to 8 870 computations (53.8% saved)

bsearch495.0ms (1.3%)

Memory
74.0MiB live, 546.9MiB allocated; 67ms collecting garbage
Algorithm
38×binary-search
11×left-value
Stop Event
34×narrow-enough
predicate-same
Samples
195.0ms2 608×0valid
37.0ms80×2valid
21.0ms183×0invalid
Compiler

Compiled 19 836 to 12 153 computations (38.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 156.0ms
ival-mult: 47.0ms (30.2% of total)
ival-div: 32.0ms (20.6% of total)
ival-add: 22.0ms (14.1% of total)
ival-sub: 16.0ms (10.3% of total)
ival-sqrt: 8.0ms (5.1% of total)
ival-fabs: 7.0ms (4.5% of total)
ival-neg: 6.0ms (3.9% of total)
adjust: 4.0ms (2.6% of total)
ival-if: 4.0ms (2.6% of total)
ival->=: 3.0ms (1.9% of total)
exact: 3.0ms (1.9% of total)
ival-true: 2.0ms (1.3% of total)
ival-exp: 1.0ms (0.6% of total)
ival-assert: 1.0ms (0.6% of total)

start0.0ms (0%)

Memory
1.0MiB live, 0.9MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...