Herbie run

Date:Sunday, December 29th, 2024
Commit:fbbe2c7d on main
Seed:2024364
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:47 976.5 MB

Time bar (total: 45.7s)

sample11.0s (24%)

Memory
349.7MiB live, 12 289.6MiB allocated; 5.2s collecting garbage
Samples
6.4s70 225×0valid
1.0s4 072×2valid
263.0ms1 930×0invalid
1.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 5.5s
ival-mult: 1.3s (23.1% of total)
ival-div: 1.2s (21.2% of total)
ival-sub: 883.0ms (15.9% of total)
ival-sqrt: 689.0ms (12.4% of total)
adjust: 406.0ms (7.3% of total)
ival-add: 277.0ms (5% of total)
ival-neg: 220.0ms (4% of total)
ival-fabs: 117.0ms (2.1% of total)
ival->=: 97.0ms (1.8% of total)
ival-log: 90.0ms (1.6% of total)
ival-if: 88.0ms (1.6% of total)
ival-exp: 82.0ms (1.5% of total)
exact: 56.0ms (1% of total)
ival-true: 53.0ms (1% of total)
ival-assert: 29.0ms (0.5% of total)
Bogosity

simplify8.9s (19.5%)

Memory
-277.6MiB live, 8 861.4MiB allocated; 1.7s collecting garbage
Stop Event
93×iter limit
51×node limit
22×saturated
Counts
2 288 → 2 262

rewrite6.4s (14%)

Memory
106.7MiB live, 6 767.3MiB allocated; 1.1s collecting garbage
Stop Event
65×iter limit
29×node limit
unsound
saturated
Counts
367 → 11 884

derivations6.3s (13.8%)

Memory
38.0MiB live, 4 149.5MiB allocated; 603ms collecting garbage
Stop Event
50×iter limit
35×node limit
done
fuel
saturated
Compiler

Compiled 4 436 to 606 computations (86.3% saved)

localize3.5s (7.7%)

Memory
85.3MiB live, 4 268.2MiB allocated; 623ms collecting garbage
Samples
1.0s6 233×0valid
727.0ms798×2valid
519.0ms540×1valid
180.0ms256×0invalid
162.0ms108×3valid
1.0ms5exit
Compiler

Compiled 7 732 to 787 computations (89.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.7s
ival-mult: 524.0ms (31% of total)
ival-div: 310.0ms (18.4% of total)
adjust: 275.0ms (16.3% of total)
ival-sub: 141.0ms (8.4% of total)
ival-add: 133.0ms (7.9% of total)
ival-sqrt: 93.0ms (5.5% of total)
ival-if: 57.0ms (3.4% of total)
ival-fabs: 45.0ms (2.7% of total)
ival-neg: 29.0ms (1.7% of total)
ival-pow2: 27.0ms (1.6% of total)
ival-log: 17.0ms (1% of total)
exact: 12.0ms (0.7% of total)
ival-exp: 8.0ms (0.5% of total)
ival->=: 7.0ms (0.4% of total)
ival-true: 6.0ms (0.4% of total)
ival-assert: 3.0ms (0.2% of total)

eval3.0s (6.5%)

Memory
104.2MiB live, 3 666.6MiB allocated; 779ms collecting garbage
Compiler

Compiled 825 622 to 61 557 computations (92.5% saved)

explain1.6s (3.6%)

Memory
124.5MiB live, 2 310.0MiB allocated; 469ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2570
-.f64#fcancellation1160
+.f64#fcancellation1160
sqrt.f64#fuflow-rescue760
/.f64#fn/u260
/.f64#fu/n240
-.f64#fnan-rescue140
*.f64(*.f64 (/.f64 x y) z)n*o120
*.f64(*.f64 (/.f64 x y) z)n*u70
/.f64(/.f64 (*.f64 #s(literal 2 binary64) c) (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 4 binary64) a) c)))))o/n10
(*.f64 #s(literal 2 binary64) c)overflow1
Confusion
Predicted +Predicted -
+29211
-2321769
Precision
0.5572519083969466
Recall
0.9636963696369637
Confusion?
Predicted +Predicted MaybePredicted -
+292011
-23201769
Precision?
0.5572519083969466
Recall?
0.9636963696369637
Freqs
test
numberfreq
01780
1403
2117
34
Total Confusion?
Predicted +Predicted MaybePredicted -
+400
-005
Precision?
1.0
Recall?
1.0
Samples
360.0ms3 670×0valid
214.0ms572×2valid
121.0ms308×1valid
63.0ms58×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 558.0ms
ival-mult: 156.0ms (28% of total)
adjust: 87.0ms (15.6% of total)
ival-sqrt: 64.0ms (11.5% of total)
ival-neg: 57.0ms (10.2% of total)
ival-div: 56.0ms (10% of total)
ival-if: 52.0ms (9.3% of total)
ival-sub: 40.0ms (7.2% of total)
ival-add: 16.0ms (2.9% of total)
ival-fabs: 6.0ms (1.1% of total)
ival-exp: 5.0ms (0.9% of total)
ival-log: 5.0ms (0.9% of total)
ival-true: 4.0ms (0.7% of total)
exact: 4.0ms (0.7% of total)
ival->=: 3.0ms (0.5% of total)
ival-assert: 2.0ms (0.4% of total)

preprocess1.1s (2.4%)

Memory
35.2MiB live, 1 171.0MiB allocated; 209ms collecting garbage
Stop Event
18×iter limit
14×saturated
node limit
Compiler

Compiled 9 399 to 1 566 computations (83.3% saved)

prune945.0ms (2.1%)

Memory
-9.8MiB live, 1 293.8MiB allocated; 154ms collecting garbage
Counts
14 609 → 287
Compiler

Compiled 24 811 to 11 457 computations (53.8% saved)

regimes915.0ms (2%)

Memory
61.0MiB live, 1 014.0MiB allocated; 99ms collecting garbage
Counts
645 → 121
Calls

26 calls:

138.0ms
b
107.0ms
a
102.0ms
x
83.0ms
z
62.0ms
(-.f64 (/.f64 #s(literal 1 binary64) x) #s(literal 1 binary64))
Compiler

Compiled 940 to 823 computations (12.4% saved)

series870.0ms (1.9%)

Memory
-57.9MiB live, 1 020.7MiB allocated; 214ms collecting garbage
Counts
367 → 2 288
Calls

186 calls:

TimeVariablePointExpression
52.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))
39.0ms
y
@-inf
((fabs (- (/ (+ x 4) y) (* (/ x y) z))) (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ 4 y) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (- 1 z) (/ x y)) (- 1 z) (- (/ (+ x 4) y) (* (/ x y) z)) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (/ (+ x 4) y) (+ x 4) (/ (+ (* y (+ 4 x)) (* (* (neg y) z) x)) (* y y)) (+ (* y (+ 4 x)) (* (* (neg y) z) x)) (fabs (/ (+ (* y (+ 4 x)) (* (* (neg y) z) x)) (* y y))) (+ 4 x) (- -4 x) (* (/ x y) z) (* (* (neg y) z) x))
38.0ms
a
@0
((- (* 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))) (>= b 0) (/ (* 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))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (neg b) 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) (* c (/ -2 (+ (sqrt (+ (* (* -4 c) a) (* b b))) b))) (* (/ (- (sqrt (+ (* (* c a) -4) (* b b))) b) a) 1/2)) (* c (/ -2 (+ (sqrt (+ (* (* -4 c) a) (* b b))) b))) (+ (* (/ b c) -2) (* (/ a b) 2)) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (/ (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b))) (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b)))) (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b))) (* (/ (/ (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b))) (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b)))) a) (/ (- (sqrt (+ (* (* -4 c) a) (* b b))) b) 2)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* a (/ c 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)) (sqrt (+ (* (* -4 c) a) (* b b))) (sqrt (+ (* (* c a) -4) (* b b))) (+ (sqrt (+ (* (* -4 c) a) (* b b))) b) (- (sqrt (+ (* (* c a) -4) (* b b))) b) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* (+ (* (/ b c) -2) (* (/ a b) 2)) c))
36.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)) (sqrt (- (* b b) (* (* 4 a) c))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))))
36.0ms
c
@inf
((- (* b b) (* (* 4 a) c)) (* (+ (* (/ -2 b) (* a (/ c b))) 2) (neg b)) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (>= b 0) (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 (+ (* (* c a) -4) (* b b))) b)) (* (/ (- (sqrt (+ (* (* c a) -4) (* b b))) b) a) 1/2)) (/ (* -2 c) (+ (sqrt (+ (* (* c a) -4) (* b b))) b)) (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))))) (* (- (* (/ 2 b) (* a (/ c b))) 2) b) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b))) (/ (/ (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b))) (+ (sqrt (+ (* (* -4 c) a) (* b b))) b)) (* 2 a)) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (/ (+ (* (neg b) b) (+ (* (* -4 c) a) (* b b))) (+ (sqrt (+ (* (* -4 c) a) (* b b))) b)) (* 2 a))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (+ (* (* c a) -4) (* b b))) (+ (sqrt (+ (* (* c a) -4) (* b b))) b) (- (sqrt (+ (* (* c a) -4) (* b b))) b) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (+ (* (* -4 c) a) (* b b))) (+ (sqrt (+ (* (* -4 c) a) (* b b))) b))

bsearch693.0ms (1.5%)

Memory
32.8MiB live, 595.7MiB allocated; 67ms collecting garbage
Algorithm
49×binary-search
11×left-value
Stop Event
47×narrow-enough
predicate-same
Samples
316.0ms2 944×0valid
17.0ms161×0invalid
10.0ms64×2valid
Compiler

Compiled 38 136 to 22 308 computations (41.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 253.0ms
ival-mult: 59.0ms (23.3% of total)
ival-div: 56.0ms (22.1% of total)
ival-sqrt: 42.0ms (16.6% of total)
ival-if: 32.0ms (12.6% of total)
ival-sub: 19.0ms (7.5% of total)
ival-add: 12.0ms (4.7% of total)
ival-fabs: 11.0ms (4.3% of total)
ival-neg: 7.0ms (2.8% of total)
ival->=: 4.0ms (1.6% of total)
adjust: 3.0ms (1.2% of total)
exact: 3.0ms (1.2% of total)
ival-exp: 2.0ms (0.8% of total)
ival-true: 2.0ms (0.8% of total)
ival-assert: 1.0ms (0.4% of total)

analyze513.0ms (1.1%)

Memory
46.7MiB live, 568.1MiB allocated; 76ms 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
67.2%56.9%27.7%0.1%0%15.3%0%5
74.4%62.4%21.5%0.1%0%16%0%6
78.9%64.9%17.3%0.1%0%17.7%0%7
80.8%66.3%15.8%0.1%0%17.9%0%8
85.9%69.9%11.5%0.1%0%18.5%0%9
88%70.7%9.7%0.1%0%19.6%0%10
90%72.1%8%0.1%0%19.8%0%11
92.3%73.5%6.2%0.1%0%20.3%0%12
Compiler

Compiled 153 to 106 computations (30.7% saved)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...