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