WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1)
2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= B] (?,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1)
9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1)
11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{8,9},3->{4,5,6},4->{7},5->{7},6->{8,9},7->{2,3},8->{10},9->{11},10->{8,9},11->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0)
(< 1,0,A>, 0, .= 0) (< 1,0,B>, B, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0)
(< 7,0,A>, 1 + A, .+ 1) (< 7,0,B>, B, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0)
(<10,0,A>, 1 + A, .+ 1) (<10,0,B>, B, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1)
2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= B] (?,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1)
9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1)
11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{8,9},3->{4,5,6},4->{7},5->{7},6->{8,9},7->{2,3},8->{10},9->{11},10->{8,9},11->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?)
(<10,0,A>, ?) (<10,0,B>, ?)
(<11,0,A>, ?) (<11,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 2,0,A>, B) (< 2,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(< 9,0,A>, B) (< 9,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
(<11,0,A>, B) (<11,0,B>, B)
* Step 3: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1)
2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= B] (?,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1)
9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1)
11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{8,9},3->{4,5,6},4->{7},5->{7},6->{8,9},7->{2,3},8->{10},9->{11},10->{8,9},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 2,0,A>, B) (< 2,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(< 9,0,A>, B) (< 9,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
(<11,0,A>, B) (<11,0,B>, B)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(2,8)]
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1)
2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= B] (?,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1)
9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1)
11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{2,3},2->{9},3->{4,5,6},4->{7},5->{7},6->{8,9},7->{2,3},8->{10},9->{11},10->{8,9},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 2,0,A>, B) (< 2,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(< 9,0,A>, B) (< 9,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
(<11,0,A>, B) (<11,0,B>, B)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [2,9,11]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{3},3->{4,5,6},4->{7},5->{7},6->{8},7->{3},8->{10},10->{8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSequentialSinglebb1in) = 2 + -1*x1 + x2
p(evalSequentialSinglebb2in) = 2 + -1*x1 + x2
p(evalSequentialSinglebb4in) = 1 + -1*x1 + x2
p(evalSequentialSinglebb5in) = 2 + -1*x1 + x2
p(evalSequentialSinglebbin) = 1 + -1*x1 + x2
p(evalSequentialSingleentryin) = 2 + x2
p(evalSequentialSinglestart) = 2 + x2
The following rules are strictly oriented:
[B >= 1 + A] ==>
evalSequentialSinglebb5in(A,B) = 2 + -1*A + B
> 1 + -1*A + B
= evalSequentialSinglebb4in(A,B)
The following rules are weakly oriented:
True ==>
evalSequentialSinglestart(A,B) = 2 + B
>= 2 + B
= evalSequentialSingleentryin(A,B)
True ==>
evalSequentialSingleentryin(A,B) = 2 + B
>= 2 + B
= evalSequentialSinglebb1in(0,B)
[B >= 1 + A] ==>
evalSequentialSinglebb1in(A,B) = 2 + -1*A + B
>= 2 + -1*A + B
= evalSequentialSinglebb2in(A,B)
[0 >= 1 + C] ==>
evalSequentialSinglebb2in(A,B) = 2 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebbin(A,B)
[C >= 1] ==>
evalSequentialSinglebb2in(A,B) = 2 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebbin(A,B)
True ==>
evalSequentialSinglebb2in(A,B) = 2 + -1*A + B
>= 2 + -1*A + B
= evalSequentialSinglebb5in(A,B)
True ==>
evalSequentialSinglebbin(A,B) = 1 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebb1in(1 + A,B)
True ==>
evalSequentialSinglebb4in(A,B) = 1 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebb5in(1 + A,B)
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (2 + B,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{3},3->{4,5,6},4->{7},5->{7},6->{8},7->{3},8->{10},10->{8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 7: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (1,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (2 + B,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (2 + B,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{3},3->{4,5,6},4->{7},5->{7},6->{8},7->{3},8->{10},10->{8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSequentialSinglebb1in) = 1
p(evalSequentialSinglebb2in) = 1
p(evalSequentialSinglebb4in) = 0
p(evalSequentialSinglebb5in) = 0
p(evalSequentialSinglebbin) = 1
p(evalSequentialSingleentryin) = 1
p(evalSequentialSinglestart) = 1
The following rules are strictly oriented:
True ==>
evalSequentialSinglebb2in(A,B) = 1
> 0
= evalSequentialSinglebb5in(A,B)
The following rules are weakly oriented:
True ==>
evalSequentialSinglestart(A,B) = 1
>= 1
= evalSequentialSingleentryin(A,B)
True ==>
evalSequentialSingleentryin(A,B) = 1
>= 1
= evalSequentialSinglebb1in(0,B)
[B >= 1 + A] ==>
evalSequentialSinglebb1in(A,B) = 1
>= 1
= evalSequentialSinglebb2in(A,B)
[0 >= 1 + C] ==>
evalSequentialSinglebb2in(A,B) = 1
>= 1
= evalSequentialSinglebbin(A,B)
[C >= 1] ==>
evalSequentialSinglebb2in(A,B) = 1
>= 1
= evalSequentialSinglebbin(A,B)
True ==>
evalSequentialSinglebbin(A,B) = 1
>= 1
= evalSequentialSinglebb1in(1 + A,B)
[B >= 1 + A] ==>
evalSequentialSinglebb5in(A,B) = 0
>= 0
= evalSequentialSinglebb4in(A,B)
True ==>
evalSequentialSinglebb4in(A,B) = 0
>= 0
= evalSequentialSinglebb5in(1 + A,B)
* Step 8: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (1,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (1,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (2 + B,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (2 + B,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{3},3->{4,5,6},4->{7},5->{7},6->{8},7->{3},8->{10},10->{8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalSequentialSinglebb1in) = 2 + -1*x1 + x2
p(evalSequentialSinglebb2in) = 1 + -1*x1 + x2
p(evalSequentialSinglebb4in) = -1*x1 + x2
p(evalSequentialSinglebb5in) = 1 + -1*x1 + x2
p(evalSequentialSinglebbin) = 1 + -1*x1 + x2
p(evalSequentialSingleentryin) = 2 + x2
p(evalSequentialSinglestart) = 2 + x2
The following rules are strictly oriented:
[B >= 1 + A] ==>
evalSequentialSinglebb1in(A,B) = 2 + -1*A + B
> 1 + -1*A + B
= evalSequentialSinglebb2in(A,B)
[B >= 1 + A] ==>
evalSequentialSinglebb5in(A,B) = 1 + -1*A + B
> -1*A + B
= evalSequentialSinglebb4in(A,B)
The following rules are weakly oriented:
True ==>
evalSequentialSinglestart(A,B) = 2 + B
>= 2 + B
= evalSequentialSingleentryin(A,B)
True ==>
evalSequentialSingleentryin(A,B) = 2 + B
>= 2 + B
= evalSequentialSinglebb1in(0,B)
[0 >= 1 + C] ==>
evalSequentialSinglebb2in(A,B) = 1 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebbin(A,B)
[C >= 1] ==>
evalSequentialSinglebb2in(A,B) = 1 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebbin(A,B)
True ==>
evalSequentialSinglebb2in(A,B) = 1 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebb5in(A,B)
True ==>
evalSequentialSinglebbin(A,B) = 1 + -1*A + B
>= 1 + -1*A + B
= evalSequentialSinglebb1in(1 + A,B)
True ==>
evalSequentialSinglebb4in(A,B) = -1*A + B
>= -1*A + B
= evalSequentialSinglebb5in(1 + A,B)
* Step 9: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (1,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (2 + B,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (1,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (2 + B,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (2 + B,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{3},3->{4,5,6},4->{7},5->{7},6->{8},7->{3},8->{10},10->{8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 10: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1)
1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (1,1)
3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (2 + B,1)
4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (2 + B,1)
5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (2 + B,1)
6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (1,1)
7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (4 + 2*B,1)
8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (2 + B,1)
10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (2 + B,1)
Signature:
{(evalSequentialSinglebb1in,2)
;(evalSequentialSinglebb2in,2)
;(evalSequentialSinglebb4in,2)
;(evalSequentialSinglebb5in,2)
;(evalSequentialSinglebbin,2)
;(evalSequentialSingleentryin,2)
;(evalSequentialSinglereturnin,2)
;(evalSequentialSinglestart,2)
;(evalSequentialSinglestop,2)}
Flow Graph:
[0->{1},1->{3},3->{4,5,6},4->{7},5->{7},6->{8},7->{3},8->{10},10->{8}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B)
(< 1,0,A>, 0) (< 1,0,B>, B)
(< 3,0,A>, B) (< 3,0,B>, B)
(< 4,0,A>, B) (< 4,0,B>, B)
(< 5,0,A>, B) (< 5,0,B>, B)
(< 6,0,A>, B) (< 6,0,B>, B)
(< 7,0,A>, B) (< 7,0,B>, B)
(< 8,0,A>, B) (< 8,0,B>, B)
(<10,0,A>, B) (<10,0,B>, B)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))