WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (?,1)
3. m2(A) -> m5(A) True (?,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
5. m1(A) -> m6(A) True (?,1)
6. m1(A) -> m4(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,A>, A, .= 0)
(<1,0,A>, A, .= 0)
(<2,0,A>, A, .= 0)
(<2,1,A>, A, .= 0)
(<3,0,A>, A, .= 0)
(<4,0,A>, 1 + A, .+ 1)
(<5,0,A>, A, .= 0)
(<6,0,A>, A, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (?,1)
3. m2(A) -> m5(A) True (?,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
5. m1(A) -> m6(A) True (?,1)
6. m1(A) -> m4(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}]
Sizebounds:
(<0,0,A>, ?)
(<1,0,A>, ?)
(<2,0,A>, ?)
(<2,1,A>, ?)
(<3,0,A>, ?)
(<4,0,A>, ?)
(<5,0,A>, ?)
(<6,0,A>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
(<6,0,A>, 1 + A)
* Step 3: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (?,1)
3. m2(A) -> m5(A) True (?,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
5. m1(A) -> m6(A) True (?,1)
6. m1(A) -> m4(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}]
Sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
(<6,0,A>, 1 + A)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [6]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (?,1)
3. m2(A) -> m5(A) True (?,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
5. m1(A) -> m6(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5},2->{1},3->{2},4->{1},5->{4}]
Sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(arrayReverse) = 2
p(m0) = 1
p(m1) = 1
p(m2) = 2
p(m3) = 0
p(m5) = 1
p(m6) = 1
The following rules are strictly oriented:
True ==>
m2(A) = 2
> 1
= m5(A)
The following rules are weakly oriented:
True ==>
arrayReverse(A) = 2
>= 2
= m2(A)
True ==>
m0(A) = 1
>= 1
= m1(A)
[A >= B && B >= A] ==>
m5(A) = 1
>= 1
= c2(m3(B),m0(B))
[B >= 0 && A >= 1 + B && 1 + B >= A] ==>
m6(A) = 1
>= 1
= m0(B)
True ==>
m1(A) = 1
>= 1
= m6(A)
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (?,1)
3. m2(A) -> m5(A) True (2,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
5. m1(A) -> m6(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5},2->{1},3->{2},4->{1},5->{4}]
Sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 6: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (2,1)
3. m2(A) -> m5(A) True (2,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (?,1)
5. m1(A) -> m6(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5},2->{1},3->{2},4->{1},5->{4}]
Sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [1,4,5], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(m0) = 1 + x1
p(m1) = 1 + x1
p(m6) = 1 + x1
The following rules are strictly oriented:
[B >= 0 && A >= 1 + B && 1 + B >= A] ==>
m6(A) = 1 + A
> 1 + B
= m0(B)
The following rules are weakly oriented:
True ==>
m0(A) = 1 + A
>= 1 + A
= m1(A)
True ==>
m1(A) = 1 + A
>= 1 + A
= m6(A)
We use the following global sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (?,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (2,1)
3. m2(A) -> m5(A) True (2,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (2 + 2*A,1)
5. m1(A) -> m6(A) True (?,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5},2->{1},3->{2},4->{1},5->{4}]
Sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 8: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. arrayReverse(A) -> m2(A) True (1,1)
1. m0(A) -> m1(A) True (4 + 2*A,1)
2. m5(A) -> c2(m3(B),m0(B)) [A >= B && B >= A] (2,1)
3. m2(A) -> m5(A) True (2,1)
4. m6(A) -> m0(B) [B >= 0 && A >= 1 + B && 1 + B >= A] (2 + 2*A,1)
5. m1(A) -> m6(A) True (4 + 2*A,1)
Signature:
{(arrayReverse,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
Flow Graph:
[0->{3},1->{5},2->{1},3->{2},4->{1},5->{4}]
Sizebounds:
(<0,0,A>, A)
(<1,0,A>, 1 + A)
(<2,0,A>, A)
(<2,1,A>, A)
(<3,0,A>, A)
(<4,0,A>, 1)
(<5,0,A>, 1 + A)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))