Herbie run

Date:Wednesday, February 26th, 2025
Commit:141e80a8 on main
Seed:2025057
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:32 925.2 MB

Time bar (total: 29.5s)

sample11.3s (38.3%)

Memory
305.2MiB live, 12 551.7MiB allocated; 4.9s collecting garbage
Samples
6.6s70 094×0valid
1.2s4 204×2valid
310.0ms1 854×0invalid
0.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 4.7s
ival-mult: 1.3s (28.9% of total)
ival-div: 968.0ms (20.8% of total)
ival-sub: 708.0ms (15.2% of total)
ival-sqrt: 502.0ms (10.8% of total)
ival-neg: 326.0ms (7% of total)
adjust: 218.0ms (4.7% of total)
ival-add: 186.0ms (4% of total)
ival-exp: 119.0ms (2.6% of total)
ival-fabs: 93.0ms (2% of total)
ival-log: 93.0ms (2% of total)
exact: 61.0ms (1.3% of total)
ival-assert: 25.0ms (0.5% of total)
ival-if: 7.0ms (0.2% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.7s (19.3%)

Memory
90.2MiB live, 5 820.0MiB allocated; 1.2s collecting garbage
Stop Event
71×iter limit
28×node limit
unsound
saturated
Counts
4 372 → 7 738

derivations2.2s (7.5%)

Memory
-74.4MiB live, 1 524.5MiB allocated; 1.0s collecting garbage
Stop Event
done
fuel
Compiler

Compiled 4 241 to 608 computations (85.7% saved)

preprocess2.2s (7.3%)

Memory
45.0MiB live, 2 024.1MiB allocated; 415ms collecting garbage
Stop Event
18×iter limit
16×node limit
saturated
Compiler

Compiled 9 047 to 1 612 computations (82.2% saved)

eval1.8s (6.1%)

Memory
-149.4MiB live, 2 431.8MiB allocated; 498ms collecting garbage
Compiler

Compiled 478 709 to 39 197 computations (91.8% saved)

explain1.6s (5.3%)

Memory
111.5MiB live, 2 063.7MiB allocated; 350ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2740
-.f64#fcancellation1230
+.f64#fcancellation1220
sqrt.f64#fuflow-rescue730
/.f64#fu/n350
/.f64#fn/u230
-.f64#fnan-rescue220
*.f64(*.f64 (/.f64 x y) z)n*o80
*.f64(*.f64 (/.f64 x y) z)n*u40
/.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
/.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 -
+30914
-2351746
Precision
0.5680147058823529
Recall
0.9566563467492261
Confusion?
Predicted +Predicted MaybePredicted -
+309014
-23501746
Precision?
0.5680147058823529
Recall?
0.9566563467492261
Freqs
test
numberfreq
01760
1410
2126
38
Total Confusion?
Predicted +Predicted MaybePredicted -
+400
-005
Precision?
1.0
Recall?
1.0
Samples
397.0ms3 664×0valid
181.0ms588×2valid
74.0ms296×1valid
46.0ms60×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 482.0ms
ival-mult: 124.0ms (25.7% of total)
ival-div: 69.0ms (14.3% of total)
ival-sub: 68.0ms (14.1% of total)
adjust: 67.0ms (13.9% of total)
ival-neg: 54.0ms (11.2% of total)
ival-sqrt: 35.0ms (7.3% of total)
ival-add: 27.0ms (5.6% of total)
ival-if: 10.0ms (2.1% of total)
ival-log: 6.0ms (1.2% of total)
ival-exp: 5.0ms (1% of total)
ival-fabs: 5.0ms (1% of total)
ival-true: 4.0ms (0.8% of total)
exact: 4.0ms (0.8% of total)
ival->=: 3.0ms (0.6% of total)
ival-assert: 2.0ms (0.4% of total)

series1.1s (3.8%)

Memory
58.9MiB live, 1 671.2MiB allocated; 289ms collecting garbage
Counts
737 → 3 635
Calls

183 calls:

TimeVariablePointExpression
44.0ms
a
@-inf
((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) b 0 (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) 2 c (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* b b) (* (* 4 a) c) (* 4 a) 4 a (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))
43.0ms
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))) (>= b 0) b 0 (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) 2 c (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* b b) (* (* 4 a) c) (* 4 a) 4 a (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))
39.0ms
z
@-inf
((fabs (+ (* (* z x) (/ -1 y)) (/ (- x -4) y))) (+ (* (* z x) (/ -1 y)) (/ (- x -4) y)) (* z x) z x (/ -1 y) -1 y (/ (- x -4) y) (- x -4) -4 (fabs (/ (- (* (- x -4) y) (* (* z y) x)) (* y y))) (/ (- (* (- x -4) y) (* (* z y) x)) (* y y)) (/ (+ 4 x) y) (+ 4 x) 4 (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (* x z) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (- 1 z) 1 (fabs (/ (- (* (- x -4) y) (* (* z y) x)) (* y y))) (/ (- (* (- x -4) y) (* (* z y) x)) (* y y)) (- (* (- x -4) y) (* (* z y) x)) (* (neg x) (* y z)) (neg x) (* y z) (* y y))
32.0ms
y
@0
((fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) z x (- -4 x) -4 y (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ 4 y) 4 (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (neg z) (/ x y)) (neg z) (/ x y) (fabs (+ (* (/ (- 1 z) y) x) (/ 4 y))) (+ (* (/ (- 1 z) y) x) (/ 4 y)) (/ (- 1 z) y) (- 1 z) 1 (fabs (/ (- (* (- x -4) y) (* (* z y) x)) (* y y))) (/ (- (* (- x -4) y) (* (* z y) x)) (* y y)) (- (* (- x -4) y) (* (* z y) x)) (* (- x -4) y) (- x -4) (* (* z y) x) (* z y) (* y y))
31.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) 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) 1/2 1 (neg (log (- (/ 1 x) 1))) (log (- (/ 1 x) 1)) (- (/ 1 x) 1) (/ (- 1 x) x) (- 1 x))

bsearch909.0ms (3.1%)

Memory
-70.8MiB live, 939.6MiB allocated; 190ms collecting garbage
Algorithm
55×binary-search
left-value
Stop Event
47×narrow-enough
predicate-same
Samples
419.0ms3 856×0valid
91.0ms565×0invalid
10.0ms64×2valid
2.0ms32×1valid
Compiler

Compiled 34 566 to 22 357 computations (35.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 343.0ms
ival-mult: 137.0ms (39.9% of total)
ival-div: 67.0ms (19.5% of total)
ival-sub: 45.0ms (13.1% of total)
ival-add: 21.0ms (6.1% of total)
ival-sqrt: 18.0ms (5.2% of total)
ival-neg: 12.0ms (3.5% of total)
ival-if: 10.0ms (2.9% of total)
ival-fabs: 9.0ms (2.6% of total)
ival->=: 8.0ms (2.3% of total)
exact: 5.0ms (1.5% of total)
adjust: 4.0ms (1.2% of total)
ival-exp: 3.0ms (0.9% of total)
ival-true: 3.0ms (0.9% of total)
ival-assert: 2.0ms (0.6% of total)

regimes827.0ms (2.8%)

Memory
85.3MiB live, 1 471.6MiB allocated; 152ms collecting garbage
Counts
659 → 121
Calls

26 calls:

114.0ms
b
109.0ms
x
58.0ms
a
56.0ms
z
46.0ms
c
Compiler

Compiled 1 178 to 994 computations (15.6% saved)

prune760.0ms (2.6%)

Memory
137.3MiB live, 1 319.8MiB allocated; 134ms collecting garbage
Counts
10 147 → 304
Compiler

Compiled 23 880 to 12 083 computations (49.4% saved)

analyze630.0ms (2.1%)

Memory
-79.0MiB live, 651.3MiB allocated; 360ms 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)

simplify594.0ms (2%)

Memory
23.6MiB live, 455.1MiB allocated; 76ms collecting garbage
Stop Event
node limit

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...