VandenBroeck and Keller, Equation (24)

Time bar (total: 5.5s)

analyze201.0ms (3.7%)

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
25%25%74.9%0.1%0%0%0%5
37.5%37.5%62.4%0.1%0%0%0%6
37.5%37.5%62.4%0.1%0%0%0%7
43.8%43.7%56.2%0.1%0%0%0%8
43.8%43.7%56.2%0.1%0%0%0%9
46.9%46.8%53.1%0.1%0%0%0%10
46.9%46.8%53.1%0.1%0%0%0%11
48.4%48.4%51.5%0.1%0%0%0%12
Compiler

Compiled 15 to 12 computations (20% saved)

Precisions
Click to see histograms. Total time spent on operations: 82.0ms
Operation ival-mult, time spent: 18.0ms, 22.0% of total-time
Operation ival-sin, time spent: 15.0ms, 18.0% of total-time
Operation ival-tan, time spent: 13.0ms, 16.0% of total-time
Operation ival-add, time spent: 11.0ms, 13.0% of total-time
Operation ival-div, time spent: 11.0ms, 13.0% of total-time
Operation ival-neg, time spent: 11.0ms, 13.0% of total-time
Operation const, time spent: 3.0ms, 4.0% of total-time

sample2.1s (39.2%)

Results
1.7s7220×0valid
148.0ms1031×0infinite
7.0ms2valid
0.0ms0valid
1.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 917.0ms
Operation ival-tan, time spent: 295.0ms, 32.0% of total-time
Operation ival-sin, time spent: 200.0ms, 22.0% of total-time
Operation ival-div, time spent: 151.0ms, 16.0% of total-time
Operation ival-add, time spent: 135.0ms, 15.0% of total-time
Operation ival-mult, time spent: 72.0ms, 8.0% of total-time
Operation ival-neg, time spent: 40.0ms, 4.0% of total-time
Operation const, time spent: 25.0ms, 3.0% of total-time
Bogosity

preprocess1.9s (34.3%)

Algorithm
egg-herbie
Rules
1366×fma-def
242×associate-/r*
232×associate-*r/
226×associate-*r*
200×times-frac
FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
00-0-B
00-0-x
00-0-(sin.f64 B)
00-0-(tan.f64 B)
00-0-(*.f64 x (/.f64 1 (tan.f64 B)))
00-0-(/.f64 1 (sin.f64 B))
00-0-(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
00-0-(/.f64 1 (tan.f64 B))
00-0-(neg.f64 (*.f64 x (/.f64 1 (tan.f64 B))))
00-0-1
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
037342
194260
2244252
3581252
4915252
51595252
62145252
72833252
82977252
93019252
103030252
113035252
Stop Event
saturated
Calls
Call 1
Inputs
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 (neg.f64 B))))) (/.f64 1 (sin.f64 (neg.f64 B))))
(+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
(neg.f64 (+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 (neg.f64 B))))) (/.f64 1 (sin.f64 (neg.f64 B)))))
(neg.f64 (+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B))))
(+.f64 (neg.f64 (*.f64 B (/.f64 1 (tan.f64 x)))) (/.f64 1 (sin.f64 x)))
Outputs
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
(+.f64 (/.f64 1 (sin.f64 B)) (/.f64 (*.f64 (neg.f64 x) 1) (tan.f64 B)))
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
(+.f64 (/.f64 1 (sin.f64 B)) (/.f64 (*.f64 (neg.f64 x) 1) (tan.f64 B)))
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 (neg.f64 B))))) (/.f64 1 (sin.f64 (neg.f64 B))))
(+.f64 (*.f64 x (neg.f64 (/.f64 1 (neg.f64 (tan.f64 B))))) (/.f64 1 (neg.f64 (sin.f64 B))))
(-.f64 (/.f64 1 (neg.f64 (sin.f64 B))) (/.f64 x (neg.f64 (tan.f64 B))))
(-.f64 (/.f64 x (tan.f64 B)) (/.f64 1 (sin.f64 B)))
(+.f64 (/.f64 x (tan.f64 B)) (/.f64 -1 (sin.f64 B)))
(+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
(+.f64 (/.f64 1 (sin.f64 B)) (*.f64 (neg.f64 x) (neg.f64 (/.f64 1 (tan.f64 B)))))
(+.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
(neg.f64 (+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 (neg.f64 B))))) (/.f64 1 (sin.f64 (neg.f64 B)))))
(+.f64 (/.f64 1 (sin.f64 B)) (/.f64 (*.f64 (neg.f64 x) 1) (tan.f64 B)))
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
(neg.f64 (+.f64 (neg.f64 (*.f64 (neg.f64 x) (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B))))
(neg.f64 (+.f64 (/.f64 1 (sin.f64 B)) (*.f64 (neg.f64 x) (neg.f64 (/.f64 1 (tan.f64 B))))))
(-.f64 (/.f64 -1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 B (/.f64 1 (tan.f64 x)))) (/.f64 1 (sin.f64 x)))
(+.f64 (*.f64 B (neg.f64 (/.f64 1 (tan.f64 x)))) (/.f64 1 (sin.f64 x)))
(-.f64 (/.f64 1 (sin.f64 x)) (/.f64 B (tan.f64 x)))
Symmetry

(negabs B)

Compiler

Compiled 100 to 59 computations (41% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.3s
Operation ival-tan, time spent: 682.0ms, 52.0% of total-time
Operation ival-sin, time spent: 283.0ms, 22.0% of total-time
Operation ival-div, time spent: 158.0ms, 12.0% of total-time
Operation ival-mult, time spent: 75.0ms, 6.0% of total-time
Operation ival-add, time spent: 53.0ms, 4.0% of total-time
Operation ival-neg, time spent: 32.0ms, 2.0% of total-time
Operation const, time spent: 20.0ms, 2.0% of total-time

eval1.0ms (0%)

Compiler

Compiled 23 to 15 computations (34.8% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
99.8%
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
99.7%
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
Compiler

Compiled 25 to 19 computations (24% saved)

localize1.0s (18.5%)

Compiler

Compiled 67 to 31 computations (53.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 716.0ms
Operation ival-tan, time spent: 341.0ms, 48.0% of total-time
Operation ival-sin, time spent: 136.0ms, 19.0% of total-time
Operation ival-div, time spent: 112.0ms, 16.0% of total-time
Operation ival-mult, time spent: 45.0ms, 6.0% of total-time
Operation ival-add, time spent: 27.0ms, 4.0% of total-time
Operation ival-sub, time spent: 26.0ms, 4.0% of total-time
Operation ival-neg, time spent: 15.0ms, 2.0% of total-time
Operation const, time spent: 14.0ms, 2.0% of total-time

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune2.0ms (0%)

Pruning

2 alts after pruning (0 fresh and 2 done)

PrunedKeptTotal
New000
Fresh000
Picked022
Done000
Total022
Accuracy
99.8%
Counts
2 → 2
Alt Table
Click to see full alt table
StatusAccuracyProgram
99.8%
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
99.7%
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
Compiler

Compiled 48 to 34 computations (29.2% saved)

regimes11.0ms (0.2%)

Accuracy

Total -0.1b remaining (-67.7%)

Threshold costs -0.1b (-67.7%)

Counts
2 → 1
Calls
Call 1
Inputs
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
Outputs
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
Calls

3 calls:

5.0ms
B
3.0ms
(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
3.0ms
x
Results
AccuracySegmentsBranch
99.8%1B
99.8%1x
99.8%1(+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))
Compiler

Compiled 20 to 15 computations (25% saved)

simplify3.0ms (0.1%)

Algorithm
egg-herbie
Rules
sub-neg
+-commutative
neg-mul-1
*-commutative
neg-sub0
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01436
12136
22736
33136
43436
53536
Stop Event
done
saturated
Calls
Call 1
Inputs
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
Outputs
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B)))
Compiler

Compiled 11 to 8 computations (27.3% saved)

soundness189.0ms (3.5%)

Rules
1366×fma-def
242×associate-/r*
232×associate-*r/
226×associate-*r*
200×times-frac
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
037342
194260
2244252
3581252
4915252
51595252
62145252
72833252
82977252
93019252
103030252
113035252
Stop Event
saturated
Compiler

Compiled 91 to 52 computations (42.9% saved)

end0.0ms (0%)

preprocess27.0ms (0.5%)

Remove

(negabs B)

Compiler

Compiled 94 to 70 computations (25.5% saved)

Profiling

Loading profile data...