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