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