WORST_CASE(?,O(n^2))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepentryin(A,B,C,D) True (1,1)
1. evalSimpleMultipleDepentryin(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (?,1)
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
3. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepreturnin(A,B,C,D) [B >= C] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepreturnin(A,B,C,D) -> evalSimpleMultipleDepstop(A,B,C,D) True (?,1)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{}]
+ 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)
(<1,0,A>, 0, .= 0) (<1,0,B>, 0, .= 0) (<1,0,C>, C, .= 0) (<1,0,D>, D, .= 0)
(<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0)
(<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0) (<3,0,D>, D, .= 0)
(<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>, C, .= 0) (<4,0,D>, D, .= 0)
(<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0) (<5,0,C>, C, .= 0) (<5,0,D>, D, .= 0)
(<6,0,A>, 1 + A, .+ 1) (<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<6,0,D>, D, .= 0)
(<7,0,A>, 0, .= 0) (<7,0,B>, 1 + B, .+ 1) (<7,0,C>, C, .= 0) (<7,0,D>, D, .= 0)
(<8,0,A>, A, .= 0) (<8,0,B>, B, .= 0) (<8,0,C>, C, .= 0) (<8,0,D>, D, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepentryin(A,B,C,D) True (1,1)
1. evalSimpleMultipleDepentryin(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (?,1)
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
3. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepreturnin(A,B,C,D) [B >= C] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepreturnin(A,B,C,D) -> evalSimpleMultipleDepstop(A,B,C,D) True (?,1)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{}]
Sizebounds:
(<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?)
(<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?)
(<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?)
(<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?)
(<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?)
(<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?)
(<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?)
(<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?)
(<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D)
(<1,0,A>, 0) (<1,0,B>, 0) (<1,0,C>, C) (<1,0,D>, D)
(<2,0,A>, D) (<2,0,B>, C) (<2,0,C>, C) (<2,0,D>, D)
(<3,0,A>, D) (<3,0,B>, C) (<3,0,C>, C) (<3,0,D>, D)
(<4,0,A>, D) (<4,0,B>, C) (<4,0,C>, C) (<4,0,D>, D)
(<5,0,A>, D) (<5,0,B>, C) (<5,0,C>, C) (<5,0,D>, D)
(<6,0,A>, D) (<6,0,B>, C) (<6,0,C>, C) (<6,0,D>, D)
(<7,0,A>, 0) (<7,0,B>, C) (<7,0,C>, C) (<7,0,D>, D)
(<8,0,A>, D) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, D)
* Step 3: LeafRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepentryin(A,B,C,D) True (1,1)
1. evalSimpleMultipleDepentryin(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (?,1)
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
3. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepreturnin(A,B,C,D) [B >= C] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepreturnin(A,B,C,D) -> evalSimpleMultipleDepstop(A,B,C,D) True (?,1)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[0->{1},1->{2,3},2->{4,5},3->{8},4->{6},5->{7},6->{2,3},7->{2,3},8->{}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D)
(<1,0,A>, 0) (<1,0,B>, 0) (<1,0,C>, C) (<1,0,D>, D)
(<2,0,A>, D) (<2,0,B>, C) (<2,0,C>, C) (<2,0,D>, D)
(<3,0,A>, D) (<3,0,B>, C) (<3,0,C>, C) (<3,0,D>, D)
(<4,0,A>, D) (<4,0,B>, C) (<4,0,C>, C) (<4,0,D>, D)
(<5,0,A>, D) (<5,0,B>, C) (<5,0,C>, C) (<5,0,D>, D)
(<6,0,A>, D) (<6,0,B>, C) (<6,0,C>, C) (<6,0,D>, D)
(<7,0,A>, 0) (<7,0,B>, C) (<7,0,C>, C) (<7,0,D>, D)
(<8,0,A>, D) (<8,0,B>, C) (<8,0,C>, C) (<8,0,D>, D)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3,8]
* Step 4: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepentryin(A,B,C,D) True (1,1)
1. evalSimpleMultipleDepentryin(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (?,1)
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{2},7->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D)
(<1,0,A>, 0) (<1,0,B>, 0) (<1,0,C>, C) (<1,0,D>, D)
(<2,0,A>, D) (<2,0,B>, C) (<2,0,C>, C) (<2,0,D>, D)
(<4,0,A>, D) (<4,0,B>, C) (<4,0,C>, C) (<4,0,D>, D)
(<5,0,A>, D) (<5,0,B>, C) (<5,0,C>, C) (<5,0,D>, D)
(<6,0,A>, D) (<6,0,B>, C) (<6,0,C>, C) (<6,0,D>, D)
(<7,0,A>, 0) (<7,0,B>, C) (<7,0,C>, C) (<7,0,D>, D)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSimpleMultipleDepbb1in) = 1
p(evalSimpleMultipleDepbb2in) = 1
p(evalSimpleMultipleDepbb3in) = 1
p(evalSimpleMultipleDepbbin) = 1
p(evalSimpleMultipleDepentryin) = 2
p(evalSimpleMultipleDepstart) = 2
The following rules are strictly oriented:
True ==>
evalSimpleMultipleDepentryin(A,B,C,D) = 2
> 1
= evalSimpleMultipleDepbb3in(0,0,C,D)
The following rules are weakly oriented:
True ==>
evalSimpleMultipleDepstart(A,B,C,D) = 2
>= 2
= evalSimpleMultipleDepentryin(A,B,C,D)
[C >= 1 + B] ==>
evalSimpleMultipleDepbb3in(A,B,C,D) = 1
>= 1
= evalSimpleMultipleDepbbin(A,B,C,D)
[D >= 1 + A] ==>
evalSimpleMultipleDepbbin(A,B,C,D) = 1
>= 1
= evalSimpleMultipleDepbb1in(A,B,C,D)
[A >= D] ==>
evalSimpleMultipleDepbbin(A,B,C,D) = 1
>= 1
= evalSimpleMultipleDepbb2in(A,B,C,D)
True ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = 1
>= 1
= evalSimpleMultipleDepbb3in(1 + A,B,C,D)
True ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = 1
>= 1
= evalSimpleMultipleDepbb3in(0,1 + B,C,D)
* Step 5: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
0. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepentryin(A,B,C,D) True (1,1)
1. evalSimpleMultipleDepentryin(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (2,1)
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[0->{1},1->{2},2->{4,5},4->{6},5->{7},6->{2},7->{2}]
Sizebounds:
(<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<0,0,D>, D)
(<1,0,A>, 0) (<1,0,B>, 0) (<1,0,C>, C) (<1,0,D>, D)
(<2,0,A>, D) (<2,0,B>, C) (<2,0,C>, C) (<2,0,D>, D)
(<4,0,A>, D) (<4,0,B>, C) (<4,0,C>, C) (<4,0,D>, D)
(<5,0,A>, D) (<5,0,B>, C) (<5,0,C>, C) (<5,0,D>, D)
(<6,0,A>, D) (<6,0,B>, C) (<6,0,C>, C) (<6,0,D>, D)
(<7,0,A>, 0) (<7,0,B>, C) (<7,0,C>, C) (<7,0,D>, D)
+ Applied Processor:
ChainProcessor False [0,1,2,4,5,6,7]
+ Details:
We chained rule 0 to obtain the rules [8] .
* Step 6: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
1. evalSimpleMultipleDepentryin(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (2,1)
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (1,2)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[1->{2},2->{4,5},4->{6},5->{7},6->{2},7->{2},8->{2}]
Sizebounds:
(<1,0,A>, 0) (<1,0,B>, 0) (<1,0,C>, C) (<1,0,D>, D)
(<2,0,A>, D) (<2,0,B>, C) (<2,0,C>, C) (<2,0,D>, D)
(<4,0,A>, D) (<4,0,B>, C) (<4,0,C>, C) (<4,0,D>, D)
(<5,0,A>, D) (<5,0,B>, C) (<5,0,C>, C) (<5,0,D>, D)
(<6,0,A>, D) (<6,0,B>, C) (<6,0,C>, C) (<6,0,D>, D)
(<7,0,A>, 0) (<7,0,B>, C) (<7,0,C>, C) (<7,0,D>, D)
(<8,0,A>, 0) (<8,0,B>, 0) (<8,0,C>, C) (<8,0,D>, D)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [1]
* Step 7: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
2. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbbin(A,B,C,D) [C >= 1 + B] (?,1)
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (1,2)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[2->{4,5},4->{6},5->{7},6->{2},7->{2},8->{2}]
Sizebounds:
(<2,0,A>, D) (<2,0,B>, C) (<2,0,C>, C) (<2,0,D>, D)
(<4,0,A>, D) (<4,0,B>, C) (<4,0,C>, C) (<4,0,D>, D)
(<5,0,A>, D) (<5,0,B>, C) (<5,0,C>, C) (<5,0,D>, D)
(<6,0,A>, D) (<6,0,B>, C) (<6,0,C>, C) (<6,0,D>, D)
(<7,0,A>, 0) (<7,0,B>, C) (<7,0,C>, C) (<7,0,D>, D)
(<8,0,A>, 0) (<8,0,B>, 0) (<8,0,C>, C) (<8,0,D>, D)
+ Applied Processor:
ChainProcessor False [2,4,5,6,7,8]
+ Details:
We chained rule 2 to obtain the rules [9,10] .
* Step 8: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
4. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [D >= 1 + A] (?,1)
5. evalSimpleMultipleDepbbin(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [A >= D] (?,1)
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (1,2)
9. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [C >= 1 + B && D >= 1 + A] (?,2)
10. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [C >= 1 + B && A >= D] (?,2)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[4->{6},5->{7},6->{9,10},7->{9,10},8->{9,10},9->{6},10->{7}]
Sizebounds:
(< 4,0,A>, D) (< 4,0,B>, C) (< 4,0,C>, C) (< 4,0,D>, D)
(< 5,0,A>, D) (< 5,0,B>, C) (< 5,0,C>, C) (< 5,0,D>, D)
(< 6,0,A>, D) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, D)
(< 7,0,A>, 0) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D)
(< 8,0,A>, 0) (< 8,0,B>, 0) (< 8,0,C>, C) (< 8,0,D>, D)
(< 9,0,A>, D) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, D)
(<10,0,A>, D) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, D)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [4,5]
* Step 9: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
6. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb3in(1 + A,B,C,D) True (?,1)
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (1,2)
9. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [C >= 1 + B && D >= 1 + A] (?,2)
10. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [C >= 1 + B && A >= D] (?,2)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[6->{9,10},7->{9,10},8->{9,10},9->{6},10->{7}]
Sizebounds:
(< 6,0,A>, D) (< 6,0,B>, C) (< 6,0,C>, C) (< 6,0,D>, D)
(< 7,0,A>, 0) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D)
(< 8,0,A>, 0) (< 8,0,B>, 0) (< 8,0,C>, C) (< 8,0,D>, D)
(< 9,0,A>, D) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, D)
(<10,0,A>, D) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, D)
+ Applied Processor:
ChainProcessor False [6,7,8,9,10]
+ Details:
We chained rule 6 to obtain the rules [11,12] .
* Step 10: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
7. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,1 + B,C,D) True (?,1)
8. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (1,2)
9. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [C >= 1 + B && D >= 1 + A] (?,2)
10. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [C >= 1 + B && A >= D] (?,2)
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[7->{9,10},8->{9,10},9->{11,12},10->{7},11->{11,12},12->{7}]
Sizebounds:
(< 7,0,A>, 0) (< 7,0,B>, C) (< 7,0,C>, C) (< 7,0,D>, D)
(< 8,0,A>, 0) (< 8,0,B>, 0) (< 8,0,C>, C) (< 8,0,D>, D)
(< 9,0,A>, D) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, D)
(<10,0,A>, D) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, D)
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
+ Applied Processor:
ChainProcessor False [7,8,9,10,11,12]
+ Details:
We chained rule 7 to obtain the rules [13,14] .
* Step 11: ChainProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
8. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb3in(0,0,C,D) True (1,2)
9. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [C >= 1 + B && D >= 1 + A] (?,2)
10. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [C >= 1 + B && A >= D] (?,2)
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[8->{9,10},9->{11,12},10->{13,14},11->{11,12},12->{13,14},13->{11,12},14->{13,14}]
Sizebounds:
(< 8,0,A>, 0) (< 8,0,B>, 0) (< 8,0,C>, C) (< 8,0,D>, D)
(< 9,0,A>, D) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, D)
(<10,0,A>, D) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, D)
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, D) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, D) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
+ Applied Processor:
ChainProcessor False [8,9,10,11,12,13,14]
+ Details:
We chained rule 8 to obtain the rules [15,16] .
* Step 12: UnreachableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
9. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb1in(A,B,C,D) [C >= 1 + B && D >= 1 + A] (?,2)
10. evalSimpleMultipleDepbb3in(A,B,C,D) -> evalSimpleMultipleDepbb2in(A,B,C,D) [C >= 1 + B && A >= D] (?,2)
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[9->{11,12},10->{13,14},11->{11,12},12->{13,14},13->{11,12},14->{13,14},15->{11,12},16->{13,14}]
Sizebounds:
(< 9,0,A>, D) (< 9,0,B>, C) (< 9,0,C>, C) (< 9,0,D>, D)
(<10,0,A>, D) (<10,0,B>, C) (<10,0,C>, C) (<10,0,D>, D)
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, D) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, D) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, D) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, D) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
UnreachableRules
+ Details:
The following transitions are not reachable from the starting states and are removed: [9,10]
* Step 13: UnsatPaths WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{13,14},15->{11,12},16->{13,14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, D) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, D) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, D) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, D) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(14,13),(16,13)]
* Step 14: LocalSizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, D) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, D) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, D) (<15,0,B>, C) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, D) (<16,0,B>, C) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<11,0,A>, 1 + A, .+ 1) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0)
(<12,0,A>, 1 + A, .+ 1) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0)
(<13,0,A>, 0, .= 0) (<13,0,B>, 1 + B, .+ 1) (<13,0,C>, C, .= 0) (<13,0,D>, D, .= 0)
(<14,0,A>, 0, .= 0) (<14,0,B>, 1 + B, .+ 1) (<14,0,C>, C, .= 0) (<14,0,D>, D, .= 0)
(<15,0,A>, 0, .= 0) (<15,0,B>, 0, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, D, .= 0)
(<16,0,A>, 0, .= 0) (<16,0,B>, 0, .= 0) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0)
* Step 15: SizeboundsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?)
(<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?)
(<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?)
(<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?)
(<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?)
(<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
* Step 16: LocationConstraintsProc WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
LocationConstraintsProc
+ Details:
We computed the location constraints 11 : [C >= 1] 12 : [C >= 1] 13 : [C >= 1
&& C >= 1 + B] 14 : [C >= 1] 15 : True 16 : True .
* Step 17: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (?,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSimpleMultipleDepbb1in) = -1 + -1*x2 + x3
p(evalSimpleMultipleDepbb2in) = -1 + -1*x2 + x3
p(evalSimpleMultipleDepstart) = x3
The following rules are strictly oriented:
[C >= 2 + B && 0 >= D] ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = -1 + -1*B + C
> -2 + -1*B + C
= evalSimpleMultipleDepbb2in(0,1 + B,C,D)
[C >= 1 && D >= 1] ==>
evalSimpleMultipleDepstart(A,B,C,D) = C
> -1 + C
= evalSimpleMultipleDepbb1in(0,0,C,D)
[C >= 1 && 0 >= D] ==>
evalSimpleMultipleDepstart(A,B,C,D) = C
> -1 + C
= evalSimpleMultipleDepbb2in(0,0,C,D)
The following rules are weakly oriented:
[C >= 1 + B && D >= 2 + A] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1 + -1*B + C
>= -1 + -1*B + C
= evalSimpleMultipleDepbb1in(1 + A,B,C,D)
[C >= 1 + B && 1 + A >= D] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1 + -1*B + C
>= -1 + -1*B + C
= evalSimpleMultipleDepbb2in(1 + A,B,C,D)
[C >= 2 + B && D >= 1] ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = -1 + -1*B + C
>= -2 + -1*B + C
= evalSimpleMultipleDepbb1in(0,1 + B,C,D)
* Step 18: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (?,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (C,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSimpleMultipleDepbb1in) = -1*x2 + x3
p(evalSimpleMultipleDepbb2in) = -1*x2 + x3
p(evalSimpleMultipleDepstart) = x3
The following rules are strictly oriented:
[C >= 2 + B && D >= 1] ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = -1*B + C
> -1 + -1*B + C
= evalSimpleMultipleDepbb1in(0,1 + B,C,D)
[C >= 2 + B && 0 >= D] ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = -1*B + C
> -1 + -1*B + C
= evalSimpleMultipleDepbb2in(0,1 + B,C,D)
The following rules are weakly oriented:
[C >= 1 + B && D >= 2 + A] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1*B + C
>= -1*B + C
= evalSimpleMultipleDepbb1in(1 + A,B,C,D)
[C >= 1 + B && 1 + A >= D] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1*B + C
>= -1*B + C
= evalSimpleMultipleDepbb2in(1 + A,B,C,D)
[C >= 1 && D >= 1] ==>
evalSimpleMultipleDepstart(A,B,C,D) = C
>= C
= evalSimpleMultipleDepbb1in(0,0,C,D)
[C >= 1 && 0 >= D] ==>
evalSimpleMultipleDepstart(A,B,C,D) = C
>= C
= evalSimpleMultipleDepbb2in(0,0,C,D)
* Step 19: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (?,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (C,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (C,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSimpleMultipleDepbb1in) = -1*x2 + x3
p(evalSimpleMultipleDepbb2in) = -1 + -1*x2 + x3
p(evalSimpleMultipleDepstart) = x3
The following rules are strictly oriented:
[C >= 1 + B && 1 + A >= D] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1*B + C
> -1 + -1*B + C
= evalSimpleMultipleDepbb2in(1 + A,B,C,D)
[C >= 2 + B && 0 >= D] ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = -1 + -1*B + C
> -2 + -1*B + C
= evalSimpleMultipleDepbb2in(0,1 + B,C,D)
[C >= 1 && 0 >= D] ==>
evalSimpleMultipleDepstart(A,B,C,D) = C
> -1 + C
= evalSimpleMultipleDepbb2in(0,0,C,D)
The following rules are weakly oriented:
[C >= 1 + B && D >= 2 + A] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1*B + C
>= -1*B + C
= evalSimpleMultipleDepbb1in(1 + A,B,C,D)
[C >= 2 + B && D >= 1] ==>
evalSimpleMultipleDepbb2in(A,B,C,D) = -1 + -1*B + C
>= -1 + -1*B + C
= evalSimpleMultipleDepbb1in(0,1 + B,C,D)
[C >= 1 && D >= 1] ==>
evalSimpleMultipleDepstart(A,B,C,D) = C
>= C
= evalSimpleMultipleDepbb1in(0,0,C,D)
* Step 20: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (C,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (C,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (C,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
LoopRecurrenceProcessor [14]
+ Details:
Applying the recurrence pattern linear * f to the expression C-B yields the solution -1*B + C .
* Step 21: PolyRank WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (?,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (C,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (C,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (C,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [11], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSimpleMultipleDepbb1in) = -1 + -1*x1 + x4
The following rules are strictly oriented:
[C >= 1 + B && D >= 2 + A] ==>
evalSimpleMultipleDepbb1in(A,B,C,D) = -1 + -1*A + D
> -2 + -1*A + D
= evalSimpleMultipleDepbb1in(1 + A,B,C,D)
The following rules are weakly oriented:
We use the following global sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
* Step 22: KnowledgePropagation WORST_CASE(?,O(n^2))
+ Considered Problem:
Rules:
11. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb1in(1 + A,B,C,D) [C >= 1 + B && D >= 2 + A] (1 + C + C*D + D,3)
12. evalSimpleMultipleDepbb1in(A,B,C,D) -> evalSimpleMultipleDepbb2in(1 + A,B,C,D) [C >= 1 + B && 1 + A >= D] (C,3)
13. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,1 + B,C,D) [C >= 2 + B && D >= 1] (C,3)
14. evalSimpleMultipleDepbb2in(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,1 + B,C,D) [C >= 2 + B && 0 >= D] (C,3)
15. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb1in(0,0,C,D) [C >= 1 && D >= 1] (1,4)
16. evalSimpleMultipleDepstart(A,B,C,D) -> evalSimpleMultipleDepbb2in(0,0,C,D) [C >= 1 && 0 >= D] (1,4)
Signature:
{(evalSimpleMultipleDepbb1in,4)
;(evalSimpleMultipleDepbb2in,4)
;(evalSimpleMultipleDepbb3in,4)
;(evalSimpleMultipleDepbbin,4)
;(evalSimpleMultipleDepentryin,4)
;(evalSimpleMultipleDepreturnin,4)
;(evalSimpleMultipleDepstart,4)
;(evalSimpleMultipleDepstop,4)}
Flow Graph:
[11->{11,12},12->{13,14},13->{11,12},14->{14},15->{11,12},16->{14}]
Sizebounds:
(<11,0,A>, D) (<11,0,B>, C) (<11,0,C>, C) (<11,0,D>, D)
(<12,0,A>, 1 + D) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, D)
(<13,0,A>, 0) (<13,0,B>, C) (<13,0,C>, C) (<13,0,D>, D)
(<14,0,A>, 0) (<14,0,B>, C) (<14,0,C>, C) (<14,0,D>, D)
(<15,0,A>, 0) (<15,0,B>, 0) (<15,0,C>, C) (<15,0,D>, D)
(<16,0,A>, 0) (<16,0,B>, 0) (<16,0,C>, C) (<16,0,D>, D)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^2))