Rosa's DopplerBench

Time bar (total: 2.2s)

analyze70.0ms (3.2%)

Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
0%0%99.9%0.1%0%0%0%1
0%0%99.9%0.1%0%0%0%2
0%0%99.9%0.1%0%0%0%3
25%25%74.9%0.1%0%0%0%4
37.5%37.4%62.4%0.1%0%0%0%5
37.5%37.4%62.4%0.1%0%0%0%6
56.3%56.2%43.7%0.1%0%0%0%7
65.6%65.5%34.3%0.1%0%0%0%8
65.6%65.5%34.3%0.1%0%0%0%9
76.6%76.5%23.4%0.1%0%0%0%10
82%81.9%17.9%0.1%0%0%0%11
82%81.9%17.9%0.1%0%0%0%12
Compiler

Compiled 16 to 9 computations (43.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 31.0ms
Operation ival-mult, time spent: 16.0ms, 51.0% of total-time
Operation ival-add, time spent: 6.0ms, 19.0% of total-time
Operation ival-neg, time spent: 6.0ms, 19.0% of total-time
Operation ival-div, time spent: 3.0ms, 10.0% of total-time
Operation const, time spent: 1.0ms, 3.0% of total-time

sample1.1s (52.2%)

Results
1.0s7971×0valid
37.0ms284×0infinite
0.0ms0valid
Precisions
Click to see histograms. Total time spent on operations: 411.0ms
Operation ival-add, time spent: 147.0ms, 36.0% of total-time
Operation ival-mult, time spent: 142.0ms, 35.0% of total-time
Operation ival-div, time spent: 62.0ms, 15.0% of total-time
Operation ival-neg, time spent: 48.0ms, 12.0% of total-time
Operation const, time spent: 13.0ms, 3.0% of total-time
Bogosity

preprocess165.0ms (7.6%)

Algorithm
egg-herbie
Rules
1644×fma-def
1442×div-sub
650×associate-/l/
644×distribute-lft-in
574×associate-*l/
FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
860-2(5.944384550941092e-267 5.317396581482263e-281 1.2339979437105166e-36)(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
00-0-u
00-0-(+.f64 t1 u)
00-0-(*.f64 (neg.f64 t1) v)
00-0-(neg.f64 t1)
00-0-v
00-0-(*.f64 (+.f64 t1 u) (+.f64 t1 u))
00-0-t1
Iterations

Useful iterations: 3 (0.0ms)

IterNodesCost
042587
1185571
2661563
32762536
Stop Event
node limit
Calls
Call 1
Inputs
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 (neg.f64 u)) (+.f64 t1 (neg.f64 u))))
(/.f64 (*.f64 (neg.f64 t1) (neg.f64 v)) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(/.f64 (*.f64 (neg.f64 (neg.f64 t1)) v) (*.f64 (+.f64 (neg.f64 t1) u) (+.f64 (neg.f64 t1) u)))
(neg.f64 (/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 (neg.f64 u)) (+.f64 t1 (neg.f64 u)))))
(neg.f64 (/.f64 (*.f64 (neg.f64 t1) (neg.f64 v)) (*.f64 (+.f64 t1 u) (+.f64 t1 u))))
(neg.f64 (/.f64 (*.f64 (neg.f64 (neg.f64 t1)) v) (*.f64 (+.f64 (neg.f64 t1) u) (+.f64 (neg.f64 t1) u))))
(/.f64 (*.f64 (neg.f64 t1) u) (*.f64 (+.f64 t1 v) (+.f64 t1 v)))
(/.f64 (*.f64 (neg.f64 u) v) (*.f64 (+.f64 u t1) (+.f64 u t1)))
(/.f64 (*.f64 (neg.f64 v) t1) (*.f64 (+.f64 v u) (+.f64 v u)))
Outputs
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
(/.f64 v (*.f64 (+.f64 t1 u) (+.f64 (/.f64 u (neg.f64 t1)) -1)))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
(/.f64 v (*.f64 (+.f64 t1 u) (+.f64 (/.f64 u (neg.f64 t1)) -1)))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 (neg.f64 u)) (+.f64 t1 (neg.f64 u))))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (-.f64 t1 u) (-.f64 t1 u)))
(*.f64 (/.f64 (neg.f64 t1) (-.f64 t1 u)) (/.f64 v (-.f64 t1 u)))
(*.f64 v (/.f64 (/.f64 t1 (-.f64 u t1)) (-.f64 t1 u)))
(/.f64 (/.f64 v (-.f64 u t1)) (-.f64 1 (/.f64 u t1)))
(/.f64 (*.f64 (neg.f64 t1) (neg.f64 v)) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(/.f64 (*.f64 t1 v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
(*.f64 (/.f64 v (+.f64 t1 u)) (/.f64 t1 (+.f64 t1 u)))
(/.f64 (/.f64 v (+.f64 t1 u)) (+.f64 (/.f64 u t1) 1))
(/.f64 (*.f64 (neg.f64 (neg.f64 t1)) v) (*.f64 (+.f64 (neg.f64 t1) u) (+.f64 (neg.f64 t1) u)))
(*.f64 (/.f64 t1 (+.f64 (neg.f64 t1) u)) (/.f64 v (+.f64 (neg.f64 t1) u)))
(*.f64 (/.f64 t1 (-.f64 u t1)) (/.f64 v (-.f64 u t1)))
(*.f64 (/.f64 v (-.f64 t1 u)) (/.f64 t1 (-.f64 t1 u)))
(/.f64 v (*.f64 (-.f64 t1 u) (-.f64 1 (/.f64 u t1))))
(neg.f64 (/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 (neg.f64 u)) (+.f64 t1 (neg.f64 u)))))
(*.f64 (/.f64 t1 (+.f64 (neg.f64 t1) u)) (/.f64 v (+.f64 (neg.f64 t1) u)))
(*.f64 (/.f64 t1 (-.f64 u t1)) (/.f64 v (-.f64 u t1)))
(*.f64 (/.f64 v (-.f64 t1 u)) (/.f64 t1 (-.f64 t1 u)))
(/.f64 v (*.f64 (-.f64 t1 u) (-.f64 1 (/.f64 u t1))))
(neg.f64 (/.f64 (*.f64 (neg.f64 t1) (neg.f64 v)) (*.f64 (+.f64 t1 u) (+.f64 t1 u))))
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
(/.f64 v (*.f64 (+.f64 t1 u) (+.f64 (/.f64 u (neg.f64 t1)) -1)))
(neg.f64 (/.f64 (*.f64 (neg.f64 (neg.f64 t1)) v) (*.f64 (+.f64 (neg.f64 t1) u) (+.f64 (neg.f64 t1) u))))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (-.f64 t1 u) (-.f64 t1 u)))
(*.f64 (/.f64 (neg.f64 t1) (-.f64 t1 u)) (/.f64 v (-.f64 t1 u)))
(*.f64 v (/.f64 (/.f64 t1 (-.f64 u t1)) (-.f64 t1 u)))
(/.f64 (/.f64 v (-.f64 u t1)) (-.f64 1 (/.f64 u t1)))
(/.f64 (*.f64 (neg.f64 t1) u) (*.f64 (+.f64 t1 v) (+.f64 t1 v)))
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 v)) (/.f64 u (+.f64 t1 v)))
(*.f64 (/.f64 t1 (+.f64 t1 v)) (/.f64 (neg.f64 u) (+.f64 t1 v)))
(/.f64 (/.f64 (neg.f64 u) (+.f64 (/.f64 v t1) 1)) (+.f64 t1 v))
(/.f64 (*.f64 (neg.f64 u) v) (*.f64 (+.f64 u t1) (+.f64 u t1)))
(*.f64 (/.f64 (neg.f64 u) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
(/.f64 (neg.f64 u) (/.f64 (+.f64 t1 u) (/.f64 v (+.f64 t1 u))))
(*.f64 v (/.f64 (neg.f64 u) (*.f64 (+.f64 t1 u) (+.f64 t1 u))))
(/.f64 (*.f64 (neg.f64 v) t1) (*.f64 (+.f64 v u) (+.f64 v u)))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 v u) (+.f64 v u)))
(/.f64 t1 (/.f64 (*.f64 (+.f64 v u) (+.f64 v u)) (neg.f64 v)))
(*.f64 t1 (/.f64 (neg.f64 v) (*.f64 (+.f64 v u) (+.f64 v u))))
(/.f64 v (/.f64 (*.f64 (+.f64 v u) (+.f64 v u)) (neg.f64 t1)))
Symmetry

(negabs v)

Compiler

Compiled 85 to 26 computations (69.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 26.0ms
Operation ival-mult, time spent: 9.0ms, 35.0% of total-time
Operation ival-add, time spent: 9.0ms, 35.0% of total-time
Operation ival-div, time spent: 5.0ms, 19.0% of total-time
Operation ival-neg, time spent: 3.0ms, 12.0% of total-time
Operation const, time spent: 1.0ms, 4.0% of total-time

eval0.0ms (0%)

Compiler

Compiled 27 to 13 computations (51.9% saved)

prune2.0ms (0.1%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
68.1%
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
94.2%
(/.f64 v (*.f64 (+.f64 t1 u) (+.f64 (/.f64 u (neg.f64 t1)) -1)))
98.4%
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
Compiler

Compiled 45 to 26 computations (42.2% saved)

localize651.0ms (30.2%)

Compiler

Compiled 107 to 23 computations (78.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 479.0ms
Operation ival-mult, time spent: 317.0ms, 66.0% of total-time
Operation ival-add, time spent: 89.0ms, 19.0% of total-time
Operation ival-div, time spent: 57.0ms, 12.0% of total-time
Operation ival-neg, time spent: 10.0ms, 2.0% of total-time
Operation const, time spent: 6.0ms, 1.0% of total-time

eval0.0ms (0%)

Compiler

Compiled 3 to 3 computations (0% saved)

prune2.0ms (0.1%)

Pruning

3 alts after pruning (0 fresh and 3 done)

PrunedKeptTotal
New000
Fresh000
Picked033
Done000
Total033
Accuracy
99.6%
Counts
3 → 3
Alt Table
Click to see full alt table
StatusAccuracyProgram
68.1%
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
94.2%
(/.f64 v (*.f64 (+.f64 t1 u) (+.f64 (/.f64 u (neg.f64 t1)) -1)))
98.4%
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
Compiler

Compiled 84 to 42 computations (50% saved)

regimes17.0ms (0.8%)

Accuracy

Total -20.2b remaining (-1997.5%)

Threshold costs -20.2b (-1997.5%)

Counts
3 → 1
Calls
Call 1
Inputs
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
(/.f64 v (*.f64 (+.f64 t1 u) (+.f64 (/.f64 u (neg.f64 t1)) -1)))
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
Outputs
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
Calls

4 calls:

8.0ms
t1
3.0ms
v
3.0ms
u
2.0ms
(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
Results
AccuracySegmentsBranch
98.4%1u
98.4%1v
98.4%1t1
98.4%1(/.f64 (*.f64 (neg.f64 t1) v) (*.f64 (+.f64 t1 u) (+.f64 t1 u)))
Compiler

Compiled 27 to 17 computations (37% saved)

simplify4.0ms (0.2%)

Algorithm
egg-herbie
Rules
14×*-commutative
12×neg-mul-1
12×+-commutative
12×neg-sub0
10×sub-neg
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01553
12353
23153
34153
44853
55353
65653
75753
Stop Event
done
saturated
Calls
Call 1
Inputs
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
Outputs
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
Compiler

Compiled 15 to 8 computations (46.7% saved)

soundness99.0ms (4.6%)

Rules
1644×fma-def
1442×div-sub
650×associate-/l/
644×distribute-lft-in
574×associate-*l/
Iterations

Useful iterations: 3 (0.0ms)

IterNodesCost
042587
1185571
2661563
32762536
Stop Event
node limit
Compiler

Compiled 27 to 11 computations (59.3% saved)

end0.0ms (0%)

preprocess22.0ms (1%)

Remove

(negabs v)

Compiler

Compiled 120 to 64 computations (46.7% saved)

Profiling

Loading profile data...