WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (?,1)
2. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + A] (?,1)
3. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + B] (?,1)
4. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + C] (?,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (?,1)
6. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [D >= A] (?,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (?,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
14. evalnestedLoopreturnin(A,B,C,D,E,F,G,H) -> evalnestedLoopstop(A,B,C,D,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1,2,3,4},1->{5,6},2->{14},3->{14},4->{14},5->{7,8},6->{14},7->{9},8->{13},9->{10,11},10->{12},11->{7
,8},12->{10,11},13->{5,6},14->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) (< 0,0,G>, G, .= 0) (< 0,0,H>, H, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, 0, .= 0) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) (< 1,0,G>, G, .= 0) (< 1,0,H>, H, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, E, .= 0) (< 2,0,F>, F, .= 0) (< 2,0,G>, G, .= 0) (< 2,0,H>, H, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0) (< 3,0,G>, G, .= 0) (< 3,0,H>, H, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) (< 4,0,G>, G, .= 0) (< 4,0,H>, H, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, 0, .= 0) (< 5,0,F>, D, .= 0) (< 5,0,G>, G, .= 0) (< 5,0,H>, H, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 6,0,F>, F, .= 0) (< 6,0,G>, G, .= 0) (< 6,0,H>, H, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 7,0,G>, G, .= 0) (< 7,0,H>, H, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0) (< 9,0,G>, 1 + E, .+ 1) (< 9,0,H>, F, .= 0)
(<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0) (<10,0,G>, G, .= 0) (<10,0,H>, H, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, G, .= 0) (<11,0,F>, H, .= 0) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0)
(<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, F, .= 0) (<12,0,G>, G, .= 0) (<12,0,H>, 1 + H, .+ 1)
(<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0) (<13,0,D>, 1 + F, .+ 1) (<13,0,E>, E, .= 0) (<13,0,F>, F, .= 0) (<13,0,G>, G, .= 0) (<13,0,H>, H, .= 0)
(<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0) (<14,0,E>, E, .= 0) (<14,0,F>, F, .= 0) (<14,0,G>, G, .= 0) (<14,0,H>, H, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (?,1)
2. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + A] (?,1)
3. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + B] (?,1)
4. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + C] (?,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (?,1)
6. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [D >= A] (?,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (?,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
14. evalnestedLoopreturnin(A,B,C,D,E,F,G,H) -> evalnestedLoopstop(A,B,C,D,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1,2,3,4},1->{5,6},2->{14},3->{14},4->{14},5->{7,8},6->{14},7->{9},8->{13},9->{10,11},10->{12},11->{7
,8},12->{10,11},13->{5,6},14->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 0,0,G>, ?) (< 0,0,H>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 1,0,G>, ?) (< 1,0,H>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 2,0,G>, ?) (< 2,0,H>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 3,0,G>, ?) (< 3,0,H>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 4,0,G>, ?) (< 4,0,H>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 6,0,H>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?) (< 9,0,G>, ?) (< 9,0,H>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C) (< 2,0,D>, D) (< 2,0,E>, E) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, C) (< 3,0,D>, D) (< 3,0,E>, E) (< 3,0,F>, F) (< 3,0,G>, G) (< 3,0,H>, H)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 4,0,F>, F) (< 4,0,G>, G) (< 4,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, C) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 6,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?)
* Step 3: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (?,1)
2. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + A] (?,1)
3. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + B] (?,1)
4. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [0 >= 1 + C] (?,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (?,1)
6. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H) [D >= A] (?,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (?,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
14. evalnestedLoopreturnin(A,B,C,D,E,F,G,H) -> evalnestedLoopstop(A,B,C,D,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1,2,3,4},1->{5,6},2->{14},3->{14},4->{14},5->{7,8},6->{14},7->{9},8->{13},9->{10,11},10->{12},11->{7
,8},12->{10,11},13->{5,6},14->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C) (< 2,0,D>, D) (< 2,0,E>, E) (< 2,0,F>, F) (< 2,0,G>, G) (< 2,0,H>, H)
(< 3,0,A>, A) (< 3,0,B>, B) (< 3,0,C>, C) (< 3,0,D>, D) (< 3,0,E>, E) (< 3,0,F>, F) (< 3,0,G>, G) (< 3,0,H>, H)
(< 4,0,A>, A) (< 4,0,B>, B) (< 4,0,C>, C) (< 4,0,D>, D) (< 4,0,E>, E) (< 4,0,F>, F) (< 4,0,G>, G) (< 4,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 6,0,A>, A) (< 6,0,B>, B) (< 6,0,C>, C) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 6,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
(<14,0,A>, A) (<14,0,B>, B) (<14,0,C>, C) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [2,3,4,6,14]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (?,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (?,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (?,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalnestedLoopbb4in) = 1
p(evalnestedLoopbb5in) = 1
p(evalnestedLoopbb6in) = 1
p(evalnestedLoopbb7in) = 1
p(evalnestedLoopbb8in) = 1
p(evalnestedLoopbb9in) = 1
p(evalnestedLoopentryin) = 2
p(evalnestedLoopstart) = 2
The following rules are strictly oriented:
[A >= 0 && B >= 0 && C >= 0] ==>
evalnestedLoopentryin(A,B,C,D,E,F,G,H) = 2
> 1
= evalnestedLoopbb9in(A,B,C,0,E,F,G,H)
The following rules are weakly oriented:
True ==>
evalnestedLoopstart(A,B,C,D,E,F,G,H) = 2
>= 2
= evalnestedLoopentryin(A,B,C,D,E,F,G,H)
[A >= 1 + D] ==>
evalnestedLoopbb9in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb7in(A,B,C,D,0,D,G,H)
[B >= 1 + E] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb4in(A,B,C,D,E,F,G,H)
[E >= B] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb8in(A,B,C,D,E,F,G,H)
True ==>
evalnestedLoopbb4in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F)
[C >= 1 + H] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb5in(A,B,C,D,E,F,G,H)
[H >= C] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb7in(A,B,C,D,G,H,G,H)
True ==>
evalnestedLoopbb5in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H)
True ==>
evalnestedLoopbb8in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H)
* Step 5: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (?,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (?,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalnestedLoopbb4in) = -1 + x1 + -1*x6
p(evalnestedLoopbb5in) = -1 + x1 + -1*x8
p(evalnestedLoopbb6in) = -1 + x1 + -1*x8
p(evalnestedLoopbb7in) = -1 + x1 + -1*x6
p(evalnestedLoopbb8in) = -1 + x1 + -1*x6
p(evalnestedLoopbb9in) = x1 + -1*x4
p(evalnestedLoopentryin) = x1
p(evalnestedLoopstart) = x1
The following rules are strictly oriented:
[A >= 1 + D] ==>
evalnestedLoopbb9in(A,B,C,D,E,F,G,H) = A + -1*D
> -1 + A + -1*D
= evalnestedLoopbb7in(A,B,C,D,0,D,G,H)
The following rules are weakly oriented:
True ==>
evalnestedLoopstart(A,B,C,D,E,F,G,H) = A
>= A
= evalnestedLoopentryin(A,B,C,D,E,F,G,H)
[A >= 0 && B >= 0 && C >= 0] ==>
evalnestedLoopentryin(A,B,C,D,E,F,G,H) = A
>= A
= evalnestedLoopbb9in(A,B,C,0,E,F,G,H)
[B >= 1 + E] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = -1 + A + -1*F
>= -1 + A + -1*F
= evalnestedLoopbb4in(A,B,C,D,E,F,G,H)
[E >= B] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = -1 + A + -1*F
>= -1 + A + -1*F
= evalnestedLoopbb8in(A,B,C,D,E,F,G,H)
True ==>
evalnestedLoopbb4in(A,B,C,D,E,F,G,H) = -1 + A + -1*F
>= -1 + A + -1*F
= evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F)
[C >= 1 + H] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = -1 + A + -1*H
>= -1 + A + -1*H
= evalnestedLoopbb5in(A,B,C,D,E,F,G,H)
[H >= C] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = -1 + A + -1*H
>= -1 + A + -1*H
= evalnestedLoopbb7in(A,B,C,D,G,H,G,H)
True ==>
evalnestedLoopbb5in(A,B,C,D,E,F,G,H) = -1 + A + -1*H
>= -2 + A + -1*H
= evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H)
True ==>
evalnestedLoopbb8in(A,B,C,D,E,F,G,H) = -1 + A + -1*F
>= -1 + A + -1*F
= evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H)
* Step 6: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (?,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalnestedLoopbb4in) = x3 + -1*x6
p(evalnestedLoopbb5in) = -1 + x3 + -1*x8
p(evalnestedLoopbb6in) = x3 + -1*x8
p(evalnestedLoopbb7in) = x3 + -1*x6
p(evalnestedLoopbb8in) = x3 + -1*x6
p(evalnestedLoopbb9in) = x3 + -1*x4
p(evalnestedLoopentryin) = x3
p(evalnestedLoopstart) = x3
The following rules are strictly oriented:
[C >= 1 + H] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = C + -1*H
> -1 + C + -1*H
= evalnestedLoopbb5in(A,B,C,D,E,F,G,H)
The following rules are weakly oriented:
True ==>
evalnestedLoopstart(A,B,C,D,E,F,G,H) = C
>= C
= evalnestedLoopentryin(A,B,C,D,E,F,G,H)
[A >= 0 && B >= 0 && C >= 0] ==>
evalnestedLoopentryin(A,B,C,D,E,F,G,H) = C
>= C
= evalnestedLoopbb9in(A,B,C,0,E,F,G,H)
[A >= 1 + D] ==>
evalnestedLoopbb9in(A,B,C,D,E,F,G,H) = C + -1*D
>= C + -1*D
= evalnestedLoopbb7in(A,B,C,D,0,D,G,H)
[B >= 1 + E] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = C + -1*F
>= C + -1*F
= evalnestedLoopbb4in(A,B,C,D,E,F,G,H)
[E >= B] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = C + -1*F
>= C + -1*F
= evalnestedLoopbb8in(A,B,C,D,E,F,G,H)
True ==>
evalnestedLoopbb4in(A,B,C,D,E,F,G,H) = C + -1*F
>= C + -1*F
= evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F)
[H >= C] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = C + -1*H
>= C + -1*H
= evalnestedLoopbb7in(A,B,C,D,G,H,G,H)
True ==>
evalnestedLoopbb5in(A,B,C,D,E,F,G,H) = -1 + C + -1*H
>= -1 + C + -1*H
= evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H)
True ==>
evalnestedLoopbb8in(A,B,C,D,E,F,G,H) = C + -1*F
>= -1 + C + -1*F
= evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H)
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (C,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (?,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 8: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (C,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (C,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (?,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [13,8,11,9,7,12,10], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalnestedLoopbb4in) = 1
p(evalnestedLoopbb5in) = 1
p(evalnestedLoopbb6in) = 1
p(evalnestedLoopbb7in) = 1
p(evalnestedLoopbb8in) = 1
p(evalnestedLoopbb9in) = 0
The following rules are strictly oriented:
True ==>
evalnestedLoopbb8in(A,B,C,D,E,F,G,H) = 1
> 0
= evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H)
The following rules are weakly oriented:
[B >= 1 + E] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb4in(A,B,C,D,E,F,G,H)
[E >= B] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb8in(A,B,C,D,E,F,G,H)
True ==>
evalnestedLoopbb4in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F)
[C >= 1 + H] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb5in(A,B,C,D,E,F,G,H)
[H >= C] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb7in(A,B,C,D,G,H,G,H)
True ==>
evalnestedLoopbb5in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
* Step 9: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (?,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (C,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (C,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (A,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [13,8,11,9,7,12,10], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalnestedLoopbb4in) = 1
p(evalnestedLoopbb5in) = 1
p(evalnestedLoopbb6in) = 1
p(evalnestedLoopbb7in) = 1
p(evalnestedLoopbb8in) = 0
p(evalnestedLoopbb9in) = 0
The following rules are strictly oriented:
[E >= B] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1
> 0
= evalnestedLoopbb8in(A,B,C,D,E,F,G,H)
The following rules are weakly oriented:
[B >= 1 + E] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb4in(A,B,C,D,E,F,G,H)
True ==>
evalnestedLoopbb4in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F)
[C >= 1 + H] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb5in(A,B,C,D,E,F,G,H)
[H >= C] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb7in(A,B,C,D,G,H,G,H)
True ==>
evalnestedLoopbb5in(A,B,C,D,E,F,G,H) = 1
>= 1
= evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H)
True ==>
evalnestedLoopbb8in(A,B,C,D,E,F,G,H) = 0
>= 0
= evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
* Step 10: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (?,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (A,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (C,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (C,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (A,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [5,8,11,9,7,12,10], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalnestedLoopbb4in) = x2 + -1*x5
p(evalnestedLoopbb5in) = 1 + x2 + -1*x7
p(evalnestedLoopbb6in) = 1 + x2 + -1*x7
p(evalnestedLoopbb7in) = 1 + x2 + -1*x5
p(evalnestedLoopbb8in) = 1 + x2 + -1*x5
p(evalnestedLoopbb9in) = 1 + x2
The following rules are strictly oriented:
[B >= 1 + E] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1 + B + -1*E
> B + -1*E
= evalnestedLoopbb4in(A,B,C,D,E,F,G,H)
The following rules are weakly oriented:
[A >= 1 + D] ==>
evalnestedLoopbb9in(A,B,C,D,E,F,G,H) = 1 + B
>= 1 + B
= evalnestedLoopbb7in(A,B,C,D,0,D,G,H)
[E >= B] ==>
evalnestedLoopbb7in(A,B,C,D,E,F,G,H) = 1 + B + -1*E
>= 1 + B + -1*E
= evalnestedLoopbb8in(A,B,C,D,E,F,G,H)
True ==>
evalnestedLoopbb4in(A,B,C,D,E,F,G,H) = B + -1*E
>= B + -1*E
= evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F)
[C >= 1 + H] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1 + B + -1*G
>= 1 + B + -1*G
= evalnestedLoopbb5in(A,B,C,D,E,F,G,H)
[H >= C] ==>
evalnestedLoopbb6in(A,B,C,D,E,F,G,H) = 1 + B + -1*G
>= 1 + B + -1*G
= evalnestedLoopbb7in(A,B,C,D,G,H,G,H)
True ==>
evalnestedLoopbb5in(A,B,C,D,E,F,G,H) = 1 + B + -1*G
>= 1 + B + -1*G
= evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H)
We use the following global sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
* Step 11: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (2 + A + A*B + 2*B,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (A,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (?,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (C,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (?,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (C,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (A,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 12: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalnestedLoopstart(A,B,C,D,E,F,G,H) -> evalnestedLoopentryin(A,B,C,D,E,F,G,H) True (1,1)
1. evalnestedLoopentryin(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H) [A >= 0 && B >= 0 && C >= 0] (2,1)
5. evalnestedLoopbb9in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H) [A >= 1 + D] (A,1)
7. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H) [B >= 1 + E] (2 + A + A*B + 2*B,1)
8. evalnestedLoopbb7in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H) [E >= B] (A,1)
9. evalnestedLoopbb4in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) True (2 + A + A*B + 2*B,1)
10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H) [C >= 1 + H] (C,1)
11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H) [H >= C] (2 + A + A*B + 2*B + C,1)
12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) True (C,1)
13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H) -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) True (A,1)
Signature:
{(evalnestedLoopbb4in,8)
;(evalnestedLoopbb5in,8)
;(evalnestedLoopbb6in,8)
;(evalnestedLoopbb7in,8)
;(evalnestedLoopbb8in,8)
;(evalnestedLoopbb9in,8)
;(evalnestedLoopentryin,8)
;(evalnestedLoopreturnin,8)
;(evalnestedLoopstart,8)
;(evalnestedLoopstop,8)}
Flow Graph:
[0->{1},1->{5},5->{7,8},7->{9},8->{13},9->{10,11},10->{12},11->{7,8},12->{10,11},13->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 0,0,F>, F) (< 0,0,G>, G) (< 0,0,H>, H)
(< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, F) (< 1,0,G>, G) (< 1,0,H>, H)
(< 5,0,A>, A) (< 5,0,B>, B) (< 5,0,C>, C) (< 5,0,D>, ?) (< 5,0,E>, 0) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?)
(< 7,0,A>, A) (< 7,0,B>, B) (< 7,0,C>, C) (< 7,0,D>, ?) (< 7,0,E>, B) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?)
(< 8,0,A>, A) (< 8,0,B>, B) (< 8,0,C>, C) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?)
(< 9,0,A>, A) (< 9,0,B>, B) (< 9,0,C>, C) (< 9,0,D>, ?) (< 9,0,E>, B) (< 9,0,F>, ?) (< 9,0,G>, B) (< 9,0,H>, ?)
(<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, C)
(<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?)
(<12,0,A>, A) (<12,0,B>, B) (<12,0,C>, C) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, C)
(<13,0,A>, A) (<13,0,B>, B) (<13,0,C>, C) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))