Given's Rotation SVD example

Time bar (total: 2.4s)

start0.0ms (0%)

Memory
0.0MiB live, 0.0MiB allocated

analyze345.0ms (14.4%)

Memory
2.3MiB live, 112.3MiB allocated
Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%48.6%51.4%0%0%0%0
0%0%48.6%51.4%0%0%0%1
0%0%48.6%51.4%0%0%0%2
0%0%48.6%51.4%0%0%0%3
0%0%48.6%51.4%0%0%0%4
31.3%15.2%33.4%51.4%0%0%0%5
34.4%16.7%31.9%51.4%0%0%0%6
51.6%25.1%23.6%51.4%0%0%0%7
53.1%25.8%22.8%51.4%0%0%0%8
62.5%30.4%18.2%51.4%0%0%0%9
63.7%31%17.7%51.4%0%0%0%10
68.6%33.3%15.3%51.4%0%0%0%11
69.2%33.7%15%51.4%0%0%0%12
Compiler

Compiled 27 to 21 computations (22.2% saved)

sample48.0ms (2%)

Memory
0.8MiB live, 16.4MiB allocated
Samples
20.0ms195×0valid
7.0ms28×2valid
5.0ms26×1valid
4.0ms11×3valid
Precisions
Click to see histograms. Total time spent on operations: 30.0ms
ival-mult: 7.0ms (23.3% of total)
const: 7.0ms (23.3% of total)
ival-sqrt: 4.0ms (13.3% of total)
adjust: 3.0ms (10% of total)
ival-add: 3.0ms (10% of total)
ival-div: 2.0ms (6.7% of total)
ival-fabs: 1.0ms (3.3% of total)
ival-<: 1.0ms (3.3% of total)
ival-assert: 0.0ms (0% of total)
ival-and: 0.0ms (0% of total)
exact: 0.0ms (0% of total)
Bogosity

explain1.9s (80.1%)

Memory
17.4MiB live, 1 071.5MiB allocated
FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
660-0-(sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))
420-0-(+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))
190-1(-3.849420558089662e-285 -3.3410861600371506e-128)(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))
00-0-(*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x))))))
00-0-#s(literal 1 binary64)
00-0-(/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x))))
00-0-#s(literal 4 binary64)
00-0-(*.f64 x x)
00-0-p
00-0-(+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x))
00-0-(*.f64 (*.f64 #s(literal 4 binary64) p) p)
00-0-#s(literal 1/2 binary64)
00-0-(*.f64 #s(literal 4 binary64) p)
00-0-x
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64(sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))oflow-rescue660
(+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x))overflow66
(*.f64 (*.f64 #s(literal 4 binary64) p) p)overflow66
+.f64(+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))cancellation420
sqrt.f64(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))uflow-rescue180
(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))underflow4
(*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x))))))underflow22
(+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))underflow22
(/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x))))underflow16
(*.f64 (*.f64 #s(literal 4 binary64) p) p)underflow51
Confusion
Predicted +Predicted -
+600
-66130
Precision
0.47619047619047616
Recall
1.0
Confusion?
Predicted +Predicted MaybePredicted -
+6000
-660130
Precision?
0.47619047619047616
Recall?
1.0
Freqs
test
numberfreq
0130
1126
Total Confusion?
Predicted +Predicted MaybePredicted -
+100
-000
Precision?
1.0
Recall?
1.0
Total Time
33.160888671875
Average Time
0.12953472137451172
Samples
381.0ms4 608×0valid
170.0ms672×2valid
104.0ms600×1valid
88.0ms264×3valid
Compiler

Compiled 3 636 to 720 computations (80.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 498.0ms
ival-mult: 176.0ms (35.3% of total)
ival-sqrt: 108.0ms (21.7% of total)
ival-add: 74.0ms (14.8% of total)
adjust: 68.0ms (13.6% of total)
ival-div: 58.0ms (11.6% of total)
exact: 8.0ms (1.6% of total)
ival-true: 5.0ms (1% of total)
ival-assert: 2.0ms (0.4% of total)

preprocess61.0ms (2.5%)

Memory
-1.7MiB live, 5.9MiB allocated
Algorithm
egg-herbie
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
03693
19087
219487
340187
466187
599987
6133487
7154487
8169887
9193287
10199987
11202787
12202987
01417
02317
13817
24517
34717
44817
04815
Stop Event
iter limit
saturated
iter limit
saturated
Calls
Call 1
Inputs
(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))
Outputs
(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))
(sqrt.f64 (fma.f64 (/.f64 #s(literal 1/2 binary64) (sqrt.f64 (fma.f64 (*.f64 p #s(literal 4 binary64)) p (*.f64 x x)))) x #s(literal 1/2 binary64)))
Symmetry

(abs p)

Compiler

Compiled 17 to 14 computations (17.6% saved)

eval0.0ms (0%)

Memory
0.0MiB live, 0.0MiB allocated
Compiler

Compiled 0 to 2 computations (-∞% saved)

prune1.0ms (0%)

Memory
0.5MiB live, 0.5MiB allocated
Alt Table
Click to see full alt table
StatusAccuracyProgram
78.1%
(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))
Compiler

Compiled 34 to 28 computations (17.6% saved)

simplify20.0ms (0.8%)

Memory
-3.6MiB live, 18.1MiB allocated
Algorithm
egg-herbie
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01417
12217
Stop Event
saturated
Calls
Call 1
Inputs
(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))
Outputs
(sqrt.f64 (*.f64 #s(literal 1/2 binary64) (+.f64 #s(literal 1 binary64) (/.f64 x (sqrt.f64 (+.f64 (*.f64 (*.f64 #s(literal 4 binary64) p) p) (*.f64 x x)))))))
(sqrt.f64 (*.f64 (+.f64 (/.f64 x (sqrt.f64 (+.f64 (*.f64 x x) (*.f64 (*.f64 p #s(literal 4 binary64)) p)))) #s(literal 1 binary64)) #s(literal 1/2 binary64)))

soundness0.0ms (0%)

Memory
0.2MiB live, 0.2MiB allocated
Stop Event
fuel
Compiler

Compiled 17 to 14 computations (17.6% saved)

preprocess3.0ms (0.1%)

Memory
2.3MiB live, 2.3MiB allocated
Remove

(abs p)

Compiler

Compiled 164 to 136 computations (17.1% saved)

end0.0ms (0%)

Memory
0.0MiB live, 0.0MiB allocated

Profiling

Loading profile data...