Herbie run

Date:Tuesday, April 1st, 2025
Commit:1da4fb0e on main
Seed:2025091
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:34 717.0 MB

Time bar (total: 26.9s)

sample9.1s (33.6%)

Memory
183.3MiB live, 10 869.9MiB allocated; 4.8s collecting garbage
Samples
5.6s70 157×0valid
542.0ms4 142×2valid
151.0ms1 908×0invalid
0.0ms5×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.3s
ival-mult!: 695.0ms (21.3% of total)
ival-sqrt: 578.0ms (17.7% of total)
ival-div!: 572.0ms (17.5% of total)
ival-exp: 329.0ms (10.1% of total)
ival-sub!: 256.0ms (7.8% of total)
ival-neg: 228.0ms (7% of total)
ival-fabs: 228.0ms (7% of total)
ival-add!: 142.0ms (4.4% of total)
adjust: 123.0ms (3.8% of total)
ival-log: 106.0ms (3.2% of total)
ival-if: 6.0ms (0.2% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.6s (20.8%)

Memory
-13.5MiB live, 6 883.0MiB allocated; 1.0s collecting garbage
Stop Event
81×iter-limit
28×node-limit
4×unsound
1×saturated
Counts
5 010 → 7 922

preprocess2.2s (8.3%)

Memory
215.9MiB live, 2 416.2MiB allocated; 304ms collecting garbage
Stop Event
18×iter-limit
16×node-limit
2×saturated
Compiler

Compiled 13 271 to 2 454 computations (81.5% saved)

derivations2.1s (7.7%)

Memory
-100.0MiB live, 2 313.6MiB allocated; 401ms collecting garbage
Stop Event
5×done
4×fuel
Compiler

Compiled 5 770 to 702 computations (87.8% saved)

eval1.8s (6.7%)

Memory
-21.0MiB live, 2 827.2MiB allocated; 353ms collecting garbage
Compiler

Compiled 569 769 to 42 642 computations (92.5% saved)

explain1.5s (5.7%)

Memory
-53.8MiB live, 2 057.8MiB allocated; 431ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2580
+.f64#fcancellation1310
-.f64#fcancellation1100
sqrt.f64#fuflow-rescue740
/.f64#fn/u230
/.f64#fu/n210
-.f64#fnan-rescue180
*.f64#fn*o60
*.f64(*.f64 (/.f64 x y) z)n*u60
/.f64#fn/o20
exp.f64(exp.f64 (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x))))sensitivity10
/.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))o/n10
↳(-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 4 binary64) a) c))))overflow1
↳(-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 4 binary64) a) c))overflow96
↳(*.f64 #s(literal 4 binary64) a)overflow1
↳(*.f64 (*.f64 #s(literal 4 binary64) a) c)overflow25
↳(*.f64 b b)overflow78
Confusion
Predicted +Predicted -
+29616
-2091783
Precision
0.5861386138613861
Recall
0.9487179487179487
Confusion?
Predicted +Predicted MaybePredicted -
+296016
-20901783
Precision?
0.5861386138613861
Recall?
0.9487179487179487
Freqs
test
numberfreq
01799
1365
2134
36
Total Confusion?
Predicted +Predicted MaybePredicted -
+500
-004
Precision?
1.0
Recall?
1.0
Samples
240.0ms3 686×0valid
220.0ms582×2valid
94.0ms302×1valid
13.0ms38×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 324.0ms
ival-mult!: 87.0ms (26.8% of total)
ival-div!: 69.0ms (21.3% of total)
ival-sqrt: 61.0ms (18.8% of total)
adjust: 36.0ms (11.1% of total)
ival-sub!: 21.0ms (6.5% of total)
ival-neg: 12.0ms (3.7% of total)
ival-if: 10.0ms (3.1% of total)
ival-add!: 8.0ms (2.5% of total)
ival-fabs: 6.0ms (1.9% of total)
ival-log: 6.0ms (1.9% of total)
ival-exp: 4.0ms (1.2% of total)
ival->=: 3.0ms (0.9% of total)

series1.2s (4.5%)

Memory
-42.0MiB live, 1 866.1MiB allocated; 221ms collecting garbage
Counts
772 → 4 238
Calls

186 calls:

TimeVariablePointExpression
59.0ms
c
@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))) a) (/ b a)) 1/2)) (>= b 0) b 0 (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* -2 c) -2 c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a (* b b) (* (- (/ (sqrt (+ (* (* -4 a) c) (* b b))) a) (/ b a)) 1/2) (- (/ (sqrt (+ (* (* -4 a) c) (* b b))) a) (/ b a)) (/ (sqrt (+ (* (* -4 a) c) (* b b))) a) (/ b a) 1/2 (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 (/ (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) a)) (/ (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) a) (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) (neg (sqrt (* (* a c) -1))) (sqrt (* (* a c) -1)) (* (* a c) -1) (* a c) -1 (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) (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) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* -4 (* a c)) (* 2 a) 2 (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 (/ (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) a)) (/ (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) a) (+ (* 1/2 (/ b a)) (sqrt (* (/ c a) -1))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* 4 a) c) (* 4 a) 4 (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 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)))) (* (+ (* (/ b c) -1) (sqrt (* (/ a c) -4))) c) (+ (* (/ b c) -1) (sqrt (* (/ a c) -4))) (/ b c) (sqrt (* (/ a c) -4)) (* (/ a c) -4) (/ a c))
42.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))) (if (>= b 0) (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2)) (>= b 0) b 0 (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* -2 c) -2 c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a (* b b) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2) (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) 1/2 (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 (/ (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) a)) (/ (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) a) (+ (* 1/2 b) (neg (sqrt (* (* a c) -1)))) (neg (sqrt (* (* a c) -1))) (sqrt (* (* a c) -1)) (* (* a c) -1) (* a c) -1 (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* 4 a) c) (* 4 a) 4 (* 2 a) 2 (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 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (* (sqrt (* (/ c a) -4)) 1/2) (* (/ b a) -1/2)) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) (* (/ b a) -1/2) (/ b a) -1/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) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (- (/ (* b b) a) (* 4 c)) a) (- (/ (* b b) a) (* 4 c)) (/ (* b b) a) (* 4 c) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (/ (neg b) (* a 2)) (/ (sqrt (+ (* (* -4 a) c) (* b b))) (* a 2)))) (+ (/ (neg b) (* a 2)) (/ (sqrt (+ (* (* -4 a) c) (* b b))) (* a 2))) (/ (neg b) (* a 2)) (* a 2) (/ (sqrt (+ (* (* -4 a) c) (* b b))) (* a 2)))
34.0ms
b
@inf
((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))) (>= b 0) b 0 (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a c (* b b) -1/2 (/ (* 2 c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* 2 c) 2 (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (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 (* (/ c a) -4)) -1/2) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* 4 a) c) (* 4 a) 4 (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)) (+ (* (/ b a) -1/2) (sqrt (* (/ c a) -1))) (/ b a) (sqrt (* (/ c a) -1)) (* (/ c a) -1) -1 (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)))) (* 2 a) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (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)))))) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg (* (+ (* (sqrt (* (/ a c) -1)) 2) (/ b c)) c)) (* (+ (* (sqrt (* (/ a c) -1)) 2) (/ b c)) c) (+ (* (sqrt (* (/ a c) -1)) 2) (/ b c)) (sqrt (* (/ a c) -1)) (* (/ a c) -1) (/ a c) (/ b c))
30.0ms
x
@inf
((exp (neg (- 1 (* x x)))) (neg (- 1 (* x x))) (- 1 (* x x)) 1 (* x x) x)
30.0ms
x
@-inf
((fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ (+ x 4) y) (+ x 4) x 4 y (* (/ x y) z) (/ x y) z)

bsearch1.2s (4.3%)

Memory
-127.6MiB live, 1 496.0MiB allocated; 833ms collecting garbage
Algorithm
62×binary-search
9×left-value
Stop Event
55×narrow-enough
7×predicate-same
Samples
736.0ms3 824×0valid
56.0ms647×0invalid
4.0ms32×2valid
2.0ms16×1valid
Compiler

Compiled 47 383 to 28 618 computations (39.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 664.0ms
ival-mult!: 503.0ms (75.7% of total)
ival-sub!: 40.0ms (6% of total)
ival-div!: 39.0ms (5.9% of total)
ival-sqrt: 23.0ms (3.5% of total)
ival-if: 14.0ms (2.1% of total)
ival-neg: 14.0ms (2.1% of total)
ival->=: 11.0ms (1.7% of total)
ival-add!: 10.0ms (1.5% of total)
ival-fabs: 6.0ms (0.9% of total)
adjust: 2.0ms (0.3% of total)
ival-exp: 1.0ms (0.2% of total)

prune941.0ms (3.5%)

Memory
146.7MiB live, 1 807.6MiB allocated; 194ms collecting garbage
Counts
10 410 → 335
Compiler

Compiled 26 854 to 13 213 computations (50.8% saved)

regimes912.0ms (3.4%)

Memory
80.2MiB live, 1 740.2MiB allocated; 122ms collecting garbage
Counts
861 → 142
Calls

26 calls:

149.0ms
b
93.0ms
x
68.0ms
(*.f64 x x)
53.0ms
a
44.0ms
(-.f64 #s(literal 1 binary64) (*.f64 x x))
Compiler

Compiled 1 301 to 1 091 computations (16.1% saved)

analyze408.0ms (1.5%)

Memory
24.6MiB live, 438.4MiB allocated; 95ms collecting garbage
Algorithm
9×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)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...