VandenBroeck and Keller, Equation (6)

Time bar (total: 17.0s)

analyze273.0ms (1.6%)

Algorithm
1×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
0%0%99.9%0.1%0%0%0%4
0%0%99.9%0.1%0%0%0%5
0%0%99.9%0.1%0%0%0%6
21.9%21.9%78%0.1%0%0%0%7
23.4%23.4%76.5%0.1%0%0%0%8
35.2%35.1%64.8%0.1%0%0%0%9
36.3%36.3%63.6%0.1%0%0%0%10
42.4%42.3%57.6%0.1%0%0%0%11
43.1%43%56.9%0.1%0%0%0%12
Compiler

Compiled 17 to 11 computations (35.3% saved)

sample16.4s (96.5%)

Results
1.2s4387×0valid-rival
451.0ms4370×0valid-sollya
5.8s3762×1valid-rival
2.2s3735×1valid-sollya
413.0ms107×2valid-rival
183.0ms106×2valid-sollya
135.0ms27×1exit-sollya
85.0ms17×0exit-sollya
3.0ms2×5exit-rival
10.0ms2×5exit-sollya
5.0ms1×2exit-sollya
Bogosity

preprocess185.0ms (1.1%)

Algorithm
1×egg-herbie
Rules
394×fma-define
301×times-frac
209×fma-neg
96×associate-*r*
87×associate-/r*
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
034415
197357
2270357
3708357
41312357
51876357
62255357
72424357
82435357
Stop Event
1×saturated
Calls
Call 1
Inputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l)))))
(neg.f64 (-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l)))))
(neg.f64 (-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l))))))
(-.f64 (*.f64 (PI.f64) F) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 l l)) (tan.f64 (*.f64 (PI.f64) F))))
Outputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l)))))
(fma.f64 (PI.f64) (neg.f64 l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(-.f64 (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)) (*.f64 (PI.f64) l))
(neg.f64 (-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 (neg.f64 F) (neg.f64 F))) (tan.f64 (*.f64 (PI.f64) l)))))
(-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l)))))
(fma.f64 (PI.f64) (neg.f64 l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(-.f64 (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)) (*.f64 (PI.f64) l))
(neg.f64 (-.f64 (*.f64 (PI.f64) (neg.f64 l)) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) (neg.f64 l))))))
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(-.f64 (*.f64 (PI.f64) l) (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F F)))
(fma.f64 (PI.f64) l (/.f64 (tan.f64 (*.f64 (PI.f64) l)) (*.f64 F (neg.f64 F))))
(-.f64 (*.f64 (PI.f64) F) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 l l)) (tan.f64 (*.f64 (PI.f64) F))))
(-.f64 (*.f64 (PI.f64) F) (/.f64 (/.f64 (tan.f64 (*.f64 (PI.f64) F)) l) l))
(-.f64 (*.f64 (PI.f64) F) (/.f64 (tan.f64 (*.f64 (PI.f64) F)) (*.f64 l l)))
Symmetry

(abs F)

(negabs l)

Compiler

Compiled 16 to 10 computations (37.5% saved)

eval0.0ms (0%)

Compiler

Compiled 2 to 2 computations (0% saved)

prune2.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
74.4%
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
Compiler

Compiled 32 to 20 computations (37.5% saved)

simplify6.0ms (0%)

Algorithm
1×egg-herbie
Rules
16×neg-mul-1
12×unsub-neg
9×*-commutative
8×distribute-lft-neg-in
8×distribute-rgt-neg-in
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01657
12857
24357
35657
46857
59357
612757
712957
Stop Event
1×saturated
Calls
Call 1
Inputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
Outputs
(-.f64 (*.f64 (PI.f64) l) (*.f64 (/.f64 #s(literal 1 binary64) (*.f64 F F)) (tan.f64 (*.f64 (PI.f64) l))))
(+.f64 (*.f64 (PI.f64) l) (*.f64 (tan.f64 (*.f64 (PI.f64) l)) (/.f64 #s(literal -1 binary64) (*.f64 F F))))

soundness1.0ms (0%)

Stop Event
1×fuel
Compiler

Compiled 16 to 10 computations (37.5% saved)

preprocess134.0ms (0.8%)

Remove

(negabs l)

(abs F)

Compiler

Compiled 192 to 120 computations (37.5% saved)

end0.0ms (0%)

Profiling

Loading profile data...