WORST_CASE(?,O(1))
* Step 1: RestrictVarsProcessor WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(A,B,C,D,E) -> f7(F,0,0,D,E) [0 >= 1 + F] (1,1)
1. f0(A,B,C,D,E) -> f7(F,0,0,D,E) [F >= 1] (1,1)
2. f0(A,B,C,D,E) -> f7(0,1023,0,D,E) True (1,1)
3. f7(A,B,C,D,E) -> f7(A,B,1 + C,2 + D,E) [B >= C] (?,1)
4. f7(A,B,C,D,E) -> f21(A,B,C,D,E) [E >= 0 && C >= 1 + B && 1022 >= E] (?,1)
5. f7(A,B,C,D,E) -> f21(A,B,C,D,E) [C >= 1 + B && E >= 1023] (?,1)
6. f7(A,B,C,D,E) -> f21(A,B,C,D,E) [C >= 1 + B && 0 >= 1 + E] (?,1)
Signature:
{(f0,5);(f21,5);(f7,5)}
Flow Graph:
[0->{3,4,5,6},1->{3,4,5,6},2->{3,4,5,6},3->{3,4,5,6},4->{},5->{},6->{}]
+ Applied Processor:
RestrictVarsProcessor
+ Details:
We removed the arguments [A,D] .
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1)
1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1)
2. f0(B,C,E) -> f7(1023,0,E) True (1,1)
3. f7(B,C,E) -> f7(B,1 + C,E) [B >= C] (?,1)
4. f7(B,C,E) -> f21(B,C,E) [E >= 0 && C >= 1 + B && 1022 >= E] (?,1)
5. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && E >= 1023] (?,1)
6. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && 0 >= 1 + E] (?,1)
Signature:
{(f0,3);(f21,3);(f7,3)}
Flow Graph:
[0->{3,4,5,6},1->{3,4,5,6},2->{3,4,5,6},3->{3,4,5,6},4->{},5->{},6->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(<0,0,B>, 0, .= 0) (<0,0,C>, 0, .= 0) (<0,0,E>, E, .= 0)
(<1,0,B>, 0, .= 0) (<1,0,C>, 0, .= 0) (<1,0,E>, E, .= 0)
(<2,0,B>, 1023, .= 1023) (<2,0,C>, 0, .= 0) (<2,0,E>, E, .= 0)
(<3,0,B>, B, .= 0) (<3,0,C>, 1 + C, .+ 1) (<3,0,E>, E, .= 0)
(<4,0,B>, B, .= 0) (<4,0,C>, C, .= 0) (<4,0,E>, E, .= 0)
(<5,0,B>, B, .= 0) (<5,0,C>, C, .= 0) (<5,0,E>, E, .= 0)
(<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<6,0,E>, E, .= 0)
* Step 3: SizeboundsProc WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1)
1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1)
2. f0(B,C,E) -> f7(1023,0,E) True (1,1)
3. f7(B,C,E) -> f7(B,1 + C,E) [B >= C] (?,1)
4. f7(B,C,E) -> f21(B,C,E) [E >= 0 && C >= 1 + B && 1022 >= E] (?,1)
5. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && E >= 1023] (?,1)
6. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && 0 >= 1 + E] (?,1)
Signature:
{(f0,3);(f21,3);(f7,3)}
Flow Graph:
[0->{3,4,5,6},1->{3,4,5,6},2->{3,4,5,6},3->{3,4,5,6},4->{},5->{},6->{}]
Sizebounds:
(<0,0,B>, ?) (<0,0,C>, ?) (<0,0,E>, ?)
(<1,0,B>, ?) (<1,0,C>, ?) (<1,0,E>, ?)
(<2,0,B>, ?) (<2,0,C>, ?) (<2,0,E>, ?)
(<3,0,B>, ?) (<3,0,C>, ?) (<3,0,E>, ?)
(<4,0,B>, ?) (<4,0,C>, ?) (<4,0,E>, ?)
(<5,0,B>, ?) (<5,0,C>, ?) (<5,0,E>, ?)
(<6,0,B>, ?) (<6,0,C>, ?) (<6,0,E>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(<0,0,B>, 0) (<0,0,C>, 0) (<0,0,E>, E)
(<1,0,B>, 0) (<1,0,C>, 0) (<1,0,E>, E)
(<2,0,B>, 1023) (<2,0,C>, 0) (<2,0,E>, E)
(<3,0,B>, 1023) (<3,0,C>, 1024) (<3,0,E>, E)
(<4,0,B>, 1023) (<4,0,C>, 1024) (<4,0,E>, E)
(<5,0,B>, 1023) (<5,0,C>, 1024) (<5,0,E>, E)
(<6,0,B>, 1023) (<6,0,C>, 1024) (<6,0,E>, E)
* Step 4: UnsatPaths WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1)
1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1)
2. f0(B,C,E) -> f7(1023,0,E) True (1,1)
3. f7(B,C,E) -> f7(B,1 + C,E) [B >= C] (?,1)
4. f7(B,C,E) -> f21(B,C,E) [E >= 0 && C >= 1 + B && 1022 >= E] (?,1)
5. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && E >= 1023] (?,1)
6. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && 0 >= 1 + E] (?,1)
Signature:
{(f0,3);(f21,3);(f7,3)}
Flow Graph:
[0->{3,4,5,6},1->{3,4,5,6},2->{3,4,5,6},3->{3,4,5,6},4->{},5->{},6->{}]
Sizebounds:
(<0,0,B>, 0) (<0,0,C>, 0) (<0,0,E>, E)
(<1,0,B>, 0) (<1,0,C>, 0) (<1,0,E>, E)
(<2,0,B>, 1023) (<2,0,C>, 0) (<2,0,E>, E)
(<3,0,B>, 1023) (<3,0,C>, 1024) (<3,0,E>, E)
(<4,0,B>, 1023) (<4,0,C>, 1024) (<4,0,E>, E)
(<5,0,B>, 1023) (<5,0,C>, 1024) (<5,0,E>, E)
(<6,0,B>, 1023) (<6,0,C>, 1024) (<6,0,E>, E)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(0,4),(0,5),(0,6),(1,4),(1,5),(1,6),(2,4),(2,5),(2,6)]
* Step 5: LeafRules WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1)
1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1)
2. f0(B,C,E) -> f7(1023,0,E) True (1,1)
3. f7(B,C,E) -> f7(B,1 + C,E) [B >= C] (?,1)
4. f7(B,C,E) -> f21(B,C,E) [E >= 0 && C >= 1 + B && 1022 >= E] (?,1)
5. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && E >= 1023] (?,1)
6. f7(B,C,E) -> f21(B,C,E) [C >= 1 + B && 0 >= 1 + E] (?,1)
Signature:
{(f0,3);(f21,3);(f7,3)}
Flow Graph:
[0->{3},1->{3},2->{3},3->{3,4,5,6},4->{},5->{},6->{}]
Sizebounds:
(<0,0,B>, 0) (<0,0,C>, 0) (<0,0,E>, E)
(<1,0,B>, 0) (<1,0,C>, 0) (<1,0,E>, E)
(<2,0,B>, 1023) (<2,0,C>, 0) (<2,0,E>, E)
(<3,0,B>, 1023) (<3,0,C>, 1024) (<3,0,E>, E)
(<4,0,B>, 1023) (<4,0,C>, 1024) (<4,0,E>, E)
(<5,0,B>, 1023) (<5,0,C>, 1024) (<5,0,E>, E)
(<6,0,B>, 1023) (<6,0,C>, 1024) (<6,0,E>, E)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [4,5,6]
* Step 6: PolyRank WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1)
1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1)
2. f0(B,C,E) -> f7(1023,0,E) True (1,1)
3. f7(B,C,E) -> f7(B,1 + C,E) [B >= C] (?,1)
Signature:
{(f0,3);(f21,3);(f7,3)}
Flow Graph:
[0->{3},1->{3},2->{3},3->{3}]
Sizebounds:
(<0,0,B>, 0) (<0,0,C>, 0) (<0,0,E>, E)
(<1,0,B>, 0) (<1,0,C>, 0) (<1,0,E>, E)
(<2,0,B>, 1023) (<2,0,C>, 0) (<2,0,E>, E)
(<3,0,B>, 1023) (<3,0,C>, 1024) (<3,0,E>, E)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(f0) = 1024
p(f7) = 1 + x1 + -1*x2
The following rules are strictly oriented:
[B >= C] ==>
f7(B,C,E) = 1 + B + -1*C
> B + -1*C
= f7(B,1 + C,E)
The following rules are weakly oriented:
[0 >= 1 + F] ==>
f0(B,C,E) = 1024
>= 1
= f7(0,0,E)
[F >= 1] ==>
f0(B,C,E) = 1024
>= 1
= f7(0,0,E)
True ==>
f0(B,C,E) = 1024
>= 1024
= f7(1023,0,E)
* Step 7: KnowledgePropagation WORST_CASE(?,O(1))
+ Considered Problem:
Rules:
0. f0(B,C,E) -> f7(0,0,E) [0 >= 1 + F] (1,1)
1. f0(B,C,E) -> f7(0,0,E) [F >= 1] (1,1)
2. f0(B,C,E) -> f7(1023,0,E) True (1,1)
3. f7(B,C,E) -> f7(B,1 + C,E) [B >= C] (1024,1)
Signature:
{(f0,3);(f21,3);(f7,3)}
Flow Graph:
[0->{3},1->{3},2->{3},3->{3}]
Sizebounds:
(<0,0,B>, 0) (<0,0,C>, 0) (<0,0,E>, E)
(<1,0,B>, 0) (<1,0,C>, 0) (<1,0,E>, E)
(<2,0,B>, 1023) (<2,0,C>, 0) (<2,0,E>, E)
(<3,0,B>, 1023) (<3,0,C>, 1024) (<3,0,E>, E)
+ Applied Processor:
KnowledgePropagation
+ Details:
The problem is already solved.
WORST_CASE(?,O(1))