WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f7(8,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (1,1)
1. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f7(A,1 + B,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V,A1 + B1 + X + Y [7 >= B] (?,1)
,-1*A1 + -1*B1 + X + Y,-3196,G1,H1,I1 + J1,J1 + K1,J1)
2. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f62(A,1 + B,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V,A1 + B1 + X + Y[7 >= B] (?,1)
,-1*A1 + -1*B1 + X + Y,-3196,G1,H1,I1 + J1,J1 + K1,J1)
3. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [B >= 8] (?,1)
4. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f62(A,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [B >= 8] (?,1)
Signature:
{(f0,20);(f118,20);(f62,20);(f7,20)}
Flow Graph:
[0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [A,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (?,1)
3. f62(B) -> f118(B) [B >= 8] (?,1)
4. f7(B) -> f62(0) [B >= 8] (?,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,B>, 0, .= 0)
(<1,0,B>, 1 + B, .+ 1)
(<2,0,B>, 1 + B, .+ 1)
(<3,0,B>, B, .= 0)
(<4,0,B>, 0, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (?,1)
3. f62(B) -> f118(B) [B >= 8] (?,1)
4. f7(B) -> f62(0) [B >= 8] (?,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
Sizebounds:
(<0,0,B>, ?)
(<1,0,B>, ?)
(<2,0,B>, ?)
(<3,0,B>, ?)
(<4,0,B>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<3,0,B>, 8)
(<4,0,B>, 0)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (?,1)
3. f62(B) -> f118(B) [B >= 8] (?,1)
4. f7(B) -> f62(0) [B >= 8] (?,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1,4},1->{1,4},2->{2,3},3->{},4->{2,3}]
Sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<3,0,B>, 8)
(<4,0,B>, 0)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,4),(4,3)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (?,1)
3. f62(B) -> f118(B) [B >= 8] (?,1)
4. f7(B) -> f62(0) [B >= 8] (?,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1},1->{1,4},2->{2,3},3->{},4->{2}]
Sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<3,0,B>, 8)
(<4,0,B>, 0)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [3]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (?,1)
4. f7(B) -> f62(0) [B >= 8] (?,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1},1->{1,4},2->{2},4->{2}]
Sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<4,0,B>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1
p(f62) = 0
p(f7) = 1
The following rules are strictly oriented:
[B >= 8] ==>
f7(B) = 1
> 0
= f62(0)
The following rules are weakly oriented:
True ==>
f0(B) = 1
>= 1
= f7(0)
[7 >= B] ==>
f7(B) = 1
>= 1
= f7(1 + B)
[7 >= B] ==>
f62(B) = 0
>= 0
= f62(1 + B)
* Step 7: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (?,1)
4. f7(B) -> f62(0) [B >= 8] (1,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1},1->{1,4},2->{2},4->{2}]
Sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<4,0,B>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 8
p(f62) = 8 + -1*x1
p(f7) = 8
The following rules are strictly oriented:
[7 >= B] ==>
f62(B) = 8 + -1*B
> 7 + -1*B
= f62(1 + B)
The following rules are weakly oriented:
True ==>
f0(B) = 8
>= 8
= f7(0)
[7 >= B] ==>
f7(B) = 8
>= 8
= f7(1 + B)
[B >= 8] ==>
f7(B) = 8
>= 8
= f62(0)
* Step 8: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (?,1)
2. f62(B) -> f62(1 + B) [7 >= B] (8,1)
4. f7(B) -> f62(0) [B >= 8] (1,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1},1->{1,4},2->{2},4->{2}]
Sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<4,0,B>, 0)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [1], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f7) = 8 + -1*x1
The following rules are strictly oriented:
[7 >= B] ==>
f7(B) = 8 + -1*B
> 7 + -1*B
= f7(1 + B)
The following rules are weakly oriented:
We use the following global sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<4,0,B>, 0)
* Step 9: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B) -> f7(0) True (1,1)
1. f7(B) -> f7(1 + B) [7 >= B] (8,1)
2. f62(B) -> f62(1 + B) [7 >= B] (8,1)
4. f7(B) -> f62(0) [B >= 8] (1,1)
Signature:
{(f0,1);(f118,1);(f62,1);(f7,1)}
Flow Graph:
[0->{1},1->{1,4},2->{2},4->{2}]
Sizebounds:
(<0,0,B>, 0)
(<1,0,B>, 8)
(<2,0,B>, 8)
(<4,0,B>, 0)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))