Herbie run

Date:Saturday, May 25th, 2024
Commit:445b0ec4 on explanations-trifurcate
Hostname:nightly with Racket 8.11.1
Seed:2024146
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:avg-errorreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default

Time bar (total: 10.7min)

simplify2.3min (21.7%)

Algorithm
269×egg-herbie
Rules
219120×fma-define
126414×distribute-lft-in
123980×times-frac
111072×*-commutative
110556×associate-*r*
Stop Event
64×saturated
205×node limit
Counts
102349 → 73867

sample1.6min (14.8%)

Results
1.2min247610×0valid
1.5s8313×0invalid
960.0ms2058×0precondition
12.0ms70×1valid
Precisions
Click to see histograms. Total time spent on operations: 1.0min
ival-mult: 12.0s (19.6% of total)
ival-<=: 10.6s (17.4% of total)
...c/correct-round.rkt:121:19: 9.3s (15.3% of total)
ival-div: 4.9s (8.1% of total)
ival-sub: 3.1s (5.1% of total)
ival-add: 2.2s (3.6% of total)
ival-sin: 2.2s (3.5% of total)
ival-sqrt: 2.1s (3.5% of total)
ival-fabs: 2.0s (3.4% of total)
ival-log: 2.0s (3.3% of total)
ival-neg: 1.6s (2.7% of total)
ival-and: 1.6s (2.6% of total)
ival-cos: 1.1s (1.8% of total)
ival-exp: 1.0s (1.7% of total)
ival-pi: 839.0ms (1.4% of total)
ival-floor: 798.0ms (1.3% of total)
ival-fmax: 562.0ms (0.9% of total)
ival-if: 542.0ms (0.9% of total)
const: 446.0ms (0.7% of total)
ival-<: 327.0ms (0.5% of total)
ival-tan: 297.0ms (0.5% of total)
ival->: 291.0ms (0.5% of total)
ival-log2: 247.0ms (0.4% of total)
ival-asin: 227.0ms (0.4% of total)
ival-atan: 184.0ms (0.3% of total)
ival-==: 157.0ms (0.3% of total)
ival-sinh: 98.0ms (0.2% of total)
ival->=: 82.0ms (0.1% of total)
backward-pass: 70.0ms (0.1% of total)
Bogosity

soundness1.4min (12.9%)

Rules
96496×fma-define
64882×times-frac
63982×associate-*r*
62260×*-commutative
54036×distribute-lft-in
Stop Event
saturated
161×node limit
30×fuel
Compiler

Compiled 51109 to 11530 computations (77.4% saved)

prune1.3min (12.2%)

Counts
140272 → 4016
Compiler

Compiled 336663 to 130124 computations (61.3% saved)

localize38.6s (6%)

Results
18.3s26309×0valid
1.7s1986×0invalid
1.2s661×1valid
1.1s238×5exit
889.0ms1524×0unsamplable
6.0ms3valid
Compiler

Compiled 102610 to 5487 computations (94.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.0s
ival-mult: 4.2s (32% of total)
ival-div: 1.9s (14.2% of total)
ival-pow: 1.1s (8.6% of total)
ival-add: 690.0ms (5.3% of total)
ival-sqrt: 611.0ms (4.7% of total)
ival-sub: 440.0ms (3.4% of total)
ival-exp: 392.0ms (3% of total)
ival-log: 371.0ms (2.9% of total)
ival-sin: 341.0ms (2.6% of total)
ival-fma: 326.0ms (2.5% of total)
ival-hypot: 325.0ms (2.5% of total)
...c/correct-round.rkt:121:19: 269.0ms (2.1% of total)
ival-log1p: 268.0ms (2.1% of total)
ival-neg: 222.0ms (1.7% of total)
ival-cbrt: 199.0ms (1.5% of total)
ival-fmax: 197.0ms (1.5% of total)
backward-pass: 159.0ms (1.2% of total)
ival-fabs: 148.0ms (1.1% of total)
ival-if: 145.0ms (1.1% of total)
ival-cos: 121.0ms (0.9% of total)
ival-floor: 98.0ms (0.8% of total)
ival-log2: 98.0ms (0.8% of total)
const: 93.0ms (0.7% of total)
ival-pi: 75.0ms (0.6% of total)
ival-expm1: 60.0ms (0.5% of total)
ival-tan: 60.0ms (0.5% of total)
ival-asin: 44.0ms (0.3% of total)
ival->=: 44.0ms (0.3% of total)
ival->: 36.0ms (0.3% of total)
ival-atan: 17.0ms (0.1% of total)
ival-sinh: 12.0ms (0.1% of total)
ival-<: 11.0ms (0.1% of total)
ival-e: 8.0ms (0.1% of total)
ival-acos: 2.0ms (0% of total)

end36.1s (5.6%)

analyze34.9s (5.4%)

Algorithm
30×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%2.6%97.4%0%0%0%0
0%0%2.6%97.4%0%0%0%1
7.8%0.2%2.4%97.4%0%0%0%2
8.5%0.2%2.4%97.4%0%0%0%3
12.8%0.3%2.3%97.4%0%0%0%4
47%1.2%1.4%97.4%0%0%0%5
51.8%1.3%1.2%97.4%0%0%0%6
69.5%1.8%0.8%97.4%0%0%0%7
71.6%1.8%0.7%97.4%0%0.1%0%8
81.1%2.1%0.5%97.4%0%0.1%0%9
82.6%2.1%0.4%97.4%0%0.1%0%10
88.3%2.2%0.3%97.4%0%0.1%0%11
89.1%2.2%0.3%97.4%0%0.1%0%12
Compiler

Compiled 2668 to 1046 computations (60.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 23.1s
ival-mult: 5.7s (24.8% of total)
ival-<=: 4.3s (18.7% of total)
...c/correct-round.rkt:121:19: 2.8s (12% of total)
ival-fabs: 1.9s (8.1% of total)
ival-div: 1.1s (4.7% of total)
ival-floor: 790.0ms (3.4% of total)
ival-if: 786.0ms (3.4% of total)
ival-fmax: 767.0ms (3.3% of total)
ival-add: 751.0ms (3.2% of total)
ival-and: 667.0ms (2.9% of total)
ival-sqrt: 620.0ms (2.7% of total)
ival-sub: 505.0ms (2.2% of total)
ival-log: 411.0ms (1.8% of total)
ival-sin: 375.0ms (1.6% of total)
ival-==: 289.0ms (1.2% of total)
ival-cos: 284.0ms (1.2% of total)
ival-log2: 191.0ms (0.8% of total)
const: 130.0ms (0.6% of total)
ival->: 126.0ms (0.5% of total)
ival-tan: 109.0ms (0.5% of total)
ival-pi: 100.0ms (0.4% of total)
ival-neg: 88.0ms (0.4% of total)
ival-exp: 83.0ms (0.4% of total)
ival->=: 81.0ms (0.3% of total)
ival-<: 67.0ms (0.3% of total)
ival-atan: 41.0ms (0.2% of total)
ival-sinh: 31.0ms (0.1% of total)
backward-pass: 22.0ms (0.1% of total)
ival-asin: 18.0ms (0.1% of total)

rewrite33.2s (5.2%)

Algorithm
119×batch-egg-rewrite
Rules
61948×log1p-expm1-u
50233×expm1-log1p-u
36557×pow1
35362×add-exp-log
35154×log-prod
Stop Event
119×node limit
Counts
2000 → 46442

series31.8s (5%)

Counts
2000 → 55907
Calls

13725 calls:

TimeVariablePointExpression
466.0ms
w
@inf
(pow (fmax (pow (sqrt (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v)))) 2) (pow (sqrt (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) 2)) -1/4)
410.0ms
dX.v
@inf
(pow (fmax (pow (sqrt (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v)))) 2) (pow (sqrt (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) 2)) -1/4)
389.0ms
h
@-inf
(if (< (if (> (/ (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u))))) (floor maxAniso)) (/ (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))))) (floor maxAniso)) (/ (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u)))) (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))))))) 1) (fmax 1 (* (if (> (/ (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u))))) (floor maxAniso)) (floor maxAniso) (/ (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u)))))) (if (> (/ (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u))))) (floor maxAniso)) (/ (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))))) (floor maxAniso)) (/ (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u)))) (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))))))))) (if (> (/ (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (fabs (* (floor h) (* (floor w) (* dX.v (neg dY.u)))))) (floor maxAniso)) (floor maxAniso) (/ (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (fabs (- (* (* (floor w) dX.u) (* (floor h) dY.v)) (* (* (floor h) dX.v) (* (floor w) dY.u)))))))
367.0ms
w
@inf
(sqrt (+ (* (* dX.u (floor w)) (* dX.u (floor w))) (* (* dX.v (floor h)) (* dX.v (floor h)))))
357.0ms
u1
@0
(* (log u1) 1/2)

eval28.3s (4.4%)

Compiler

Compiled 14221927 to 580581 computations (95.9% saved)

regimes24.0s (3.7%)

Counts
8574 → 384
Calls

145 calls:

814.0ms
dX.v
798.0ms
cosTheta_i
651.0ms
dY.v
544.0ms
u2
532.0ms
u0
Compiler

Compiled 13566 to 9335 computations (31.2% saved)

explain9.6s (1.5%)

Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f32#fsensitivity103177
-.f32#fcancellation39424
sqrt.f32#foflow-rescue3330
cos.f32#fsensitivity2047
tan.f32(tan.f32 (+.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u1) (*.f32 #s(literal 1/2 binary32) (PI.f32))))cancellation19219
/.f32#fo/n1100
exp.f32#fsensitivity3229
/.f32#fu/n270
sqrt.f32(sqrt.f32 (-.f32 (*.f32 eta eta) (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O))))))uflow-rescue200
(*.f32 sinTheta_O sinTheta_O)underflow280
(-.f32 (*.f32 eta eta) (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O)))))underflow20
(/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O))))underflow140
(*.f32 eta eta)underflow20
/.f32#fo/o60
/.f32(/.f32 (neg.f32 (log.f32 (-.f32 #s(literal 1 binary32) u0))) (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay))))n/o60
(/.f32 sin2phi (*.f32 alphay alphay))overflow15
(+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay)))overflow15
*.f32(*.f32 (sin.f32 (*.f32 u normAngle)) (/.f32 #s(literal 1 binary32) (sin.f32 normAngle)))n*u20
sin.f32(sin.f32 (*.f32 (*.f32 uy #s(literal 2 binary32)) (PI.f32)))cancellation10
Confusion
Predicted +Predicted -
+166557
-3875571
Precision
0.8114035087719298
Recall
0.9668989547038328
Confusion?
Predicted +Predicted MaybePredicted -
+16653027
-3871025469
Precision?
0.7760989010989011
Recall?
0.9843205574912892
Freqs
test
numberfreq
05628
11752
2294
36
Total Confusion?
Predicted +Predicted MaybePredicted -
+2011
-503
Precision?
0.8076923076923077
Recall?
0.9545454545454546
Results
3.7s15318×0valid
22.0ms42×1valid
Compiler

Compiled 18444 to 2196 computations (88.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.0s
ival-mult: 650.0ms (32.1% of total)
ival-div: 246.0ms (12.2% of total)
ival-floor: 230.0ms (11.4% of total)
ival-sub: 157.0ms (7.8% of total)
ival-sin: 128.0ms (6.3% of total)
ival-add: 123.0ms (6.1% of total)
ival-log: 89.0ms (4.4% of total)
ival-sqrt: 81.0ms (4% of total)
ival-exp: 44.0ms (2.2% of total)
ival-cos: 43.0ms (2.1% of total)
ival-neg: 30.0ms (1.5% of total)
const: 29.0ms (1.4% of total)
...c/correct-round.rkt:121:19: 29.0ms (1.4% of total)
ival-pi: 28.0ms (1.4% of total)
ival-tan: 20.0ms (1% of total)
ival-fmax: 18.0ms (0.9% of total)
ival-if: 16.0ms (0.8% of total)
ival-log2: 15.0ms (0.7% of total)
ival-fabs: 10.0ms (0.5% of total)
ival-atan: 8.0ms (0.4% of total)
backward-pass: 6.0ms (0.3% of total)
ival-sinh: 6.0ms (0.3% of total)
ival->=: 6.0ms (0.3% of total)
ival->: 5.0ms (0.2% of total)
ival-asin: 5.0ms (0.2% of total)
ival-<: 2.0ms (0.1% of total)

preprocess9.2s (1.4%)

Algorithm
30×egg-herbie
Rules
30630×fma-define
21782×fma-neg
15892×unsub-neg
14706×distribute-lft-neg-in
11858×distribute-rgt-neg-in
Stop Event
11×saturated
19×node limit
Compiler

Compiled 46096 to 17158 computations (62.8% saved)

bsearch38.0ms (0%)

Algorithm
50×binary-search
33×left-value
Stop Event
50×narrow-enough
Compiler

Compiled 4084 to 1846 computations (54.8% saved)

Profiling

Loading profile data...