Herbie run

Date:Wednesday, March 26th, 2025
Commit:a931ba94 on hardware-accelerators
Seed:2025085
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:987 657.9 MB

Time bar (total: 15.2min)

sample4.8min (31.3%)

Memory
4 986.4MiB live, 313 852.7MiB allocated; 1.6min collecting garbage
Samples
2.6min2 144 737×0valid
18.8s69 547×1valid
9.6s63 484×0invalid
1.9s5 919×2valid
875.0ms1 235×5exit
500.0ms1 852×1invalid
261.0ms381×4exit
180.0ms660×3valid
3.0ms24×1exit
0.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 1.6min
ival-mult!: 37.5s (38.2% of total)
ival-div!: 11.1s (11.3% of total)
ival-sub!: 11.0s (11.3% of total)
ival-add!: 9.5s (9.7% of total)
ival-log: 9.0s (9.2% of total)
ival-sqrt: 4.7s (4.8% of total)
ival-sin: 4.2s (4.3% of total)
adjust: 3.8s (3.9% of total)
ival-cos: 3.4s (3.4% of total)
ival-exp: 2.1s (2.1% of total)
ival-cosh: 420.0ms (0.4% of total)
ival-hypot: 291.0ms (0.3% of total)
ival-tan: 276.0ms (0.3% of total)
ival-fabs: 263.0ms (0.3% of total)
ival-acos: 259.0ms (0.3% of total)
ival-sinh: 187.0ms (0.2% of total)
ival-tanh: 132.0ms (0.1% of total)
const: 0.0ms (0% of total)
Bogosity

rewrite3.2min (21.3%)

Memory
2 535.4MiB live, 190 098.2MiB allocated; 1.0min collecting garbage
Stop Event
2 225×iter limit
851×node limit
69×unsound
13×saturated
Counts
122 542 → 222 079

preprocess1.1min (7.5%)

Memory
2 463.8MiB live, 66 574.8MiB allocated; 14.6s collecting garbage
Stop Event
538×iter limit
341×node limit
197×saturated
Compiler

Compiled 314 164 to 56 390 computations (82.1% saved)

derivations1.1min (7.5%)

Memory
306.6MiB live, 55 952.3MiB allocated; 15.2s collecting garbage
Stop Event
148×fuel
121×done
Compiler

Compiled 143 073 to 19 157 computations (86.6% saved)

regimes1.1min (7.1%)

Memory
311.6MiB live, 85 856.5MiB allocated; 17.2s collecting garbage
Counts
33 194 → 4 965
Calls

512 calls:

9.7s
x
8.9s
y
8.0s
z
4.2s
t
2.9s
a
Compiler

Compiled 37 067 to 55 614 computations (-50% saved)

series55.4s (6.1%)

Memory
594.3MiB live, 67 192.8MiB allocated; 19.7s collecting garbage
Counts
18 526 → 104 016
Calls

8880 calls:

TimeVariablePointExpression
3.4s
x
@-inf
((- (- (* x (log y)) z) y) (- (* x (log y)) z) (* (+ (* (/ (log y) z) x) -1) z) (+ (* (/ (log y) z) x) -1) (/ (log y) z) (log y) y z x -1 (- (- (* x (+ (log (pow y 1/2)) (log (pow y 1/2)))) z) y) (neg z) (- (- (* x (log y)) z) y) (* (- (log y) (/ (+ z y) x)) x) (- (log y) (/ (+ z y) x)) (/ (neg z) x) (- (- (* x (log y)) z) y) (* (log y) x) (- (- (* x (log y)) z) y) (* (- (log y) (/ (+ z y) x)) x) (- (log y) (/ (+ z y) x)) (/ (+ z y) x) (+ z y))
697.0ms
y
@0
((/ (+ x (* y (- z x))) z) (+ (* (- 1 y) (/ x z)) y) (* (/ (- 1 y) z) x) (/ (- 1 y) z) (/ (neg y) z) (neg y) y z x (/ (+ x (* y (- z x))) z) (+ (* (- 1 y) (/ x z)) y) (/ (* (- 1 (* y y)) x) (* (+ 1 y) z)) (* (- 1 (* y y)) x) (- 1 (* y y)) 1 (* y y) (* (+ 1 y) z) (+ 1 y) (/ (+ x (* y (- z x))) z) (+ (* (- 1 y) (/ x z)) y) (/ (* (- 1 (pow y 3)) x) (* (+ 1 (+ (* y y) (* 1 y))) z)) (* (- 1 (pow y 3)) x) (- 1 (pow y 3)) (pow y 3) 3 (* (+ 1 (+ (* y y) (* 1 y))) z) (+ 1 (+ (* y y) (* 1 y))) (+ (* y y) (* 1 y)) (* 1 y) (/ (+ x (* y (- z x))) z) (+ x (* y (- z x))) (+ (* (neg y) x) x))
297.0ms
y
@-inf
((* x (/ (- 0 (pow (log (/ y x)) 3)) (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x))))))) x (/ (- 0 (pow (log (/ y x)) 3)) (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x)))))) (- 0 (pow (log (/ y x)) 3)) 0 (pow (log (/ y x)) 3) (log (/ y x)) (/ y x) y 3 (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x))))) (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x)))) (* 0 (log (/ y x))) (* (- (log (neg x)) (log (neg y))) x) (- (log (neg x)) (log (neg y))) (log (neg x)) (neg x) (log (neg y)) (neg y) (+ (* (log (neg x)) x) (* (/ 1 (pow (log (/ -1 y)) -1)) x)) (* (/ 1 (pow (log (/ -1 y)) -1)) x) (/ 1 (pow (log (/ -1 y)) -1)) 1 (pow (log (/ -1 y)) -1) (log (/ -1 y)) (/ -1 y) -1 (* x (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y)))) (/ (- (pow (log (neg x)) 2) (pow (log (neg y)) 2)) (+ (* (log (/ -1 x)) -1) (log (neg y)))) (- (pow (log (neg x)) 2) (pow (log (neg y)) 2)) (pow (log (neg x)) 2) 2 (pow (log (neg y)) 2) (+ (* (log (/ -1 x)) -1) (log (neg y))) (log (/ -1 x)) (/ -1 x) (* x (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (exp (log (log (/ -1 y)))) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (exp (log (log (/ -1 y)))) 2) (log (* x y)))) (/ (pow (log (neg x)) 2) (log (* x y))) (log (* x y)) (* x y) (/ (pow (exp (log (log (/ -1 y)))) 2) (log (* x y))) (pow (exp (log (log (/ -1 y)))) 2) (exp (log (log (/ -1 y)))) (log (log (/ -1 y))))
272.0ms
x
@0
((* (/ (neg (pow (log (/ y x)) 3)) (- (pow (log (/ y x)) 2) 0)) x) (/ (neg (pow (log (/ y x)) 3)) (- (pow (log (/ y x)) 2) 0)) (neg (pow (log (/ y x)) 3)) (pow (log (/ y x)) 3) (log (/ y x)) (/ y x) y x 3 (- (pow (log (/ y x)) 2) 0) (pow (log (/ y x)) 2) 2 0 (- (* (log x) x) (* (log y) x)) (* (log x) x) (log x) (* (log y) x) (log y) (+ (* (log (neg x)) x) (/ (* 1 x) (pow (log (/ -1 y)) -1))) (log (neg x)) (neg x) (/ (* 1 x) (pow (log (/ -1 y)) -1)) (* 1 x) 1 (pow (log (/ -1 y)) -1) (log (/ -1 y)) (/ -1 y) -1 (* (/ (- (pow (log y) 2) (pow (log x) 2)) -1) (/ x (log (* y x)))) (/ (- (pow (log y) 2) (pow (log x) 2)) -1) (- (pow (log y) 2) (pow (log x) 2)) (pow (log y) 2) (pow (log x) 2) (/ x (log (* y x))) (log (* y x)) (* y x) (/ (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (+ (* (log (* y x)) (log (neg x))) (pow (log (neg y)) 2))) (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) (pow (log (neg x)) 3) (pow (log (neg y)) 3) (log (neg y)) (neg y) (+ (* (log (* y x)) (log (neg x))) (pow (log (neg y)) 2)) (pow (log (neg y)) 2))
228.0ms
a
@0
((* x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))))) x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b)))) (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))) (* y (- (log z) t)) y (- (log z) t) (log z) z t (* a (- (log (- 1 z)) b)) a (- (log (- 1 z)) b) (log (- 1 z)) (- 1 z) 1 b)

eval49.3s (5.4%)

Memory
-1 146.7MiB live, 59 154.4MiB allocated; 20.4s collecting garbage
Samples
590.0ms7 037×0valid
486.0ms5 429×0invalid
3.0ms39×1valid
3.0ms23×3valid
2.0ms16×2valid
Compiler

Compiled 8 997 102 to 975 051 computations (89.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 603.0ms
ival-mult!: 331.0ms (54.9% of total)
ival-add!: 268.0ms (44.4% of total)
adjust: 4.0ms (0.7% of total)

explain38.3s (4.2%)

Memory
82.8MiB live, 45 196.6MiB allocated; 12.1s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15656
/.f64#fo/n12300
sqrt.f64#foflow-rescue7950
-.f64#fcancellation5914
/.f64#fo/o5620
*.f64#fn*o5160
-.f64#fnan-rescue4600
+.f64#fnan-rescue4360
cos.f64#fsensitivity3641
+.f64#fcancellation3631
/.f64#fn/o3430
/.f64#fu/n2390
sin.f64#fsensitivity2261
*.f64#fn*u1800
cos.f64#foflow-rescue1430
/.f64#fn/u1360
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity1001
/.f64#fu/u980
log.f64#foflow-rescue790
log.f64#fuflow-rescue710
sqrt.f64#fuflow-rescue420
*.f64#fo*u350
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(exp.f64 (-.f64 (+.f64 (*.f64 y (log.f64 z)) (*.f64 (-.f64 t #s(literal 1 binary64)) (log.f64 a))) b))sensitivity244
*.f64#fu*o30
Confusion
Predicted +Predicted -
+6014186
-169860966
Precision
0.7798236514522822
Recall
0.97
Confusion?
Predicted +Predicted MaybePredicted -
+60140186
-16982060946
Precision?
0.7778065183652354
Recall?
0.97
Freqs
test
numberfreq
061152
16863
2762
372
49
56
Total Confusion?
Predicted +Predicted MaybePredicted -
+13701
-12128
Precision?
0.9785714285714285
Recall?
0.9927536231884058
Samples
9.5s130 334×0valid
1.9s6 038×1valid
453.0ms1 234×2valid
31.0ms110×3valid
3.0ms10×4valid
0.0ms5exit
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 6.0s
ival-mult!: 2.0s (34.1% of total)
ival-log: 856.0ms (14.3% of total)
ival-div!: 696.0ms (11.6% of total)
ival-add!: 586.0ms (9.8% of total)
ival-sub!: 568.0ms (9.5% of total)
ival-cos: 333.0ms (5.6% of total)
adjust: 311.0ms (5.2% of total)
ival-sqrt: 235.0ms (3.9% of total)
ival-sin: 212.0ms (3.5% of total)
ival-exp: 86.0ms (1.4% of total)
ival-fabs: 17.0ms (0.3% of total)
ival-tan: 12.0ms (0.2% of total)
ival-cosh: 12.0ms (0.2% of total)
ival-sinh: 10.0ms (0.2% of total)
ival-hypot: 9.0ms (0.2% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-acos: 5.0ms (0.1% of total)
const: 0.0ms (0% of total)

bsearch29.3s (3.2%)

Memory
380.3MiB live, 33 322.2MiB allocated; 7.6s collecting garbage
Algorithm
1 767×binary-search
1 092×left-value
Stop Event
1 733×narrow-enough
34×predicate-same
Samples
14.2s144 536×0valid
942.0ms4 300×1valid
246.0ms2 971×0invalid
26.0ms174×2valid
11.0ms30×1invalid
6.0ms30×3valid
Compiler

Compiled 918 373 to 658 654 computations (28.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 9.3s
ival-mult!: 4.8s (52.3% of total)
ival-sub!: 1.2s (13% of total)
ival-add!: 905.0ms (9.8% of total)
ival-div!: 740.0ms (8% of total)
ival-log: 528.0ms (5.7% of total)
ival-sin: 413.0ms (4.5% of total)
ival-cos: 198.0ms (2.1% of total)
adjust: 185.0ms (2% of total)
ival-exp: 87.0ms (0.9% of total)
ival-sqrt: 73.0ms (0.8% of total)
ival-sinh: 44.0ms (0.5% of total)
ival-tanh: 30.0ms (0.3% of total)
ival-cosh: 10.0ms (0.1% of total)
ival-fabs: 7.0ms (0.1% of total)

prune25.3s (2.8%)

Memory
-518.4MiB live, 37 275.3MiB allocated; 8.4s collecting garbage
Counts
247 806 → 12 472
Samples
63.0ms480×0invalid
27.0ms288×0valid
Compiler

Compiled 765 137 to 420 976 computations (45% saved)

Precisions
Click to see histograms. Total time spent on operations: 61.0ms
ival-mult!: 57.0ms (93% of total)
ival-add!: 5.0ms (8.2% of total)
adjust: 0.0ms (0% of total)

analyze18.9s (2.1%)

Memory
529.7MiB live, 19 452.9MiB allocated; 8.2s 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)

simplify14.9s (1.6%)

Memory
-722.7MiB live, 13 705.2MiB allocated; 2.5s collecting garbage
Stop Event
205×node limit
64×saturated

start9.0ms (0%)

Memory
20.5MiB live, 20.2MiB allocated; 0ms collecting garbage

end2.0ms (0%)

Memory
4.1MiB live, 3.9MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...