invcot (example 3.9)

Time bar (total: 18.6s)

analyze12.0ms (0.1%)

Memory
3.9MiB live, 3.9MiB allocated
Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%49.7%50.3%0%0%0%0
0%0%49.7%50.3%0%0%0%1
50%24.8%24.8%50.3%0%0%0%2
75%37.3%12.4%50.3%0%0%0%3
87.5%43.5%6.2%50.3%0%0%0%4
93.8%46.6%3.1%50.3%0%0%0%5
96.9%48.1%1.6%50.3%0%0%0%6
98.4%48.9%0.8%50.3%0%0%0%7
99.2%49.3%0.4%50.3%0%0%0%8
99.6%49.5%0.2%50.3%0%0%0%9
99.8%49.6%0.1%50.3%0%0%0%10
99.9%49.6%0%50.3%0%0%0%11
100%49.7%0%50.3%0%0%0%12
Compiler

Compiled 20 to 15 computations (25% saved)

sample18.5s (99.5%)

Memory
8.9MiB live, 2 136.5MiB allocated
Samples
3.8s4 471×2valid-baseline
3.7s4 471×2valid-sollya
3.3s4 471×2valid-rival
3.2s1 363×3valid-baseline
1.7s1 363×3valid-sollya
912.0ms1 363×3valid-rival
400.0ms2 372×1valid-baseline
281.0ms2 372×1valid-rival
253.0ms2 372×1valid-sollya
4.0ms50×0valid-baseline
3.0ms50×0valid-sollya
2.0ms50×0valid-rival
Bogosity

preprocess43.0ms (0.2%)

Memory
-11.3MiB live, 19.2MiB allocated
Algorithm
egg-herbie
Rules
44×fmm-def
21×fma-define
15×sub-neg
14×distribute-lft-neg-in
12×neg-mul-1
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
017124
133116
268116
3146116
4229116
5278116
6287116
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x))))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x)))))
Outputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x))))
(-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (neg.f64 (tan.f64 x))))
(-.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x)))))
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
Symmetry

(negabs x)

Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated
Compiler

Compiled 1 to 1 computations (0% saved)

prune1.0ms (0%)

Memory
0.9MiB live, 0.9MiB allocated
Alt Table
Click to see full alt table
StatusAccuracyProgram
7.3%
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
Compiler

Compiled 18 to 12 computations (33.3% saved)

simplify2.0ms (0%)

Memory
0.5MiB live, 0.5MiB allocated
Algorithm
egg-herbie
Rules
neg-mul-1
unsub-neg
sub-neg
+-commutative
*-rgt-identity
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01129
11829
22629
33229
43929
55129
66729
Stop Event
saturated
Calls
Call 1
Inputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
Outputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))

soundness0.0ms (0%)

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

Compiled 9 to 7 computations (22.2% saved)

preprocess30.0ms (0.2%)

Memory
3.4MiB live, 36.7MiB allocated
Remove

(negabs x)

Compiler

Compiled 122 to 88 computations (27.9% saved)

end0.0ms (0%)

Memory
0.0MiB live, 0.0MiB allocated

Profiling

Loading profile data...