WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (?,1)
2. evalaaron2entryin(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [B >= 1 + C] (?,1)
4. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (?,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
11. evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1,2},1->{3,4,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5}
,11->{}]
+ Applied Processor:
LocalSizeboundsProc
+ Details:
LocalSizebounds generated; rvgraph
(< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0)
(< 1,0,A>, A, .= 0) (< 1,0,B>, C, .= 0) (< 1,0,C>, B, .= 0)
(< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0)
(< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0)
(< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0)
(< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0)
(< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0)
(< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0)
(< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0)
(< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, 1 + A + C, .* 1)
(<10,0,A>, A, .= 0) (<10,0,B>, 1 + A + B, .* 1) (<10,0,C>, C, .= 0)
(<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0)
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (?,1)
2. evalaaron2entryin(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [B >= 1 + C] (?,1)
4. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (?,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
11. evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1,2},1->{3,4,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5}
,11->{}]
Sizebounds:
(< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?)
(< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?)
(< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?)
(< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?)
+ Applied Processor:
SizeboundsProc
+ Details:
Sizebounds computed:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?)
* Step 3: UnsatPaths WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (?,1)
2. evalaaron2entryin(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [B >= 1 + C] (?,1)
4. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (?,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
11. evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1,2},1->{3,4,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5}
,11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?)
+ Applied Processor:
UnsatPaths
+ Details:
We remove following edges from the transition graph: [(1,4)]
* Step 4: LeafRules WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (?,1)
2. evalaaron2entryin(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
3. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [B >= 1 + C] (?,1)
4. evalaaron2bb6in(A,B,C) -> evalaaron2returnin(A,B,C) [0 >= 1 + A] (?,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (?,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
11. evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1,2},1->{3,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5},11->{}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 2,0,A>, A) (< 2,0,B>, B) (< 2,0,C>, C)
(< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, ?)
(< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
(<11,0,A>, A) (<11,0,B>, ?) (<11,0,C>, ?)
+ Applied Processor:
LeafRules
+ Details:
The following transitions are estimated by its predecessors and are removed [2,3,4,11]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (?,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (?,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1},1->{5},5->{6,7,8},6->{9},7->{9},8->{10},9->{5},10->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalaaron2bb3in) = 0
p(evalaaron2bb4in) = 0
p(evalaaron2bb5in) = 0
p(evalaaron2bb6in) = 0
p(evalaaron2entryin) = 1
p(evalaaron2start) = 1
The following rules are strictly oriented:
[A >= 0] ==>
evalaaron2entryin(A,B,C) = 1
> 0
= evalaaron2bb6in(A,C,B)
The following rules are weakly oriented:
True ==>
evalaaron2start(A,B,C) = 1
>= 1
= evalaaron2entryin(A,B,C)
[C >= B && A >= 0] ==>
evalaaron2bb6in(A,B,C) = 0
>= 0
= evalaaron2bb3in(A,B,C)
[0 >= 1 + D] ==>
evalaaron2bb3in(A,B,C) = 0
>= 0
= evalaaron2bb4in(A,B,C)
[D >= 1] ==>
evalaaron2bb3in(A,B,C) = 0
>= 0
= evalaaron2bb4in(A,B,C)
True ==>
evalaaron2bb3in(A,B,C) = 0
>= 0
= evalaaron2bb5in(A,B,C)
True ==>
evalaaron2bb4in(A,B,C) = 0
>= 0
= evalaaron2bb6in(A,B,-1 + -1*A + C)
True ==>
evalaaron2bb5in(A,B,C) = 0
>= 0
= evalaaron2bb6in(A,1 + A + B,C)
* Step 6: PolyRank WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (1,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (?,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1},1->{5},5->{6,7,8},6->{9},7->{9},8->{10},9->{5},10->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
+ Details:
We apply a polynomial interpretation of shape linear:
p(evalaaron2bb3in) = -1*x1 + -1*x2 + x3
p(evalaaron2bb4in) = -1*x1 + -1*x2 + x3
p(evalaaron2bb5in) = -1*x1 + -1*x2 + x3
p(evalaaron2bb6in) = 1 + -1*x2 + x3
p(evalaaron2entryin) = 1 + x2 + -1*x3
p(evalaaron2start) = 1 + x2 + -1*x3
The following rules are strictly oriented:
[C >= B && A >= 0] ==>
evalaaron2bb6in(A,B,C) = 1 + -1*B + C
> -1*A + -1*B + C
= evalaaron2bb3in(A,B,C)
The following rules are weakly oriented:
True ==>
evalaaron2start(A,B,C) = 1 + B + -1*C
>= 1 + B + -1*C
= evalaaron2entryin(A,B,C)
[A >= 0] ==>
evalaaron2entryin(A,B,C) = 1 + B + -1*C
>= 1 + B + -1*C
= evalaaron2bb6in(A,C,B)
[0 >= 1 + D] ==>
evalaaron2bb3in(A,B,C) = -1*A + -1*B + C
>= -1*A + -1*B + C
= evalaaron2bb4in(A,B,C)
[D >= 1] ==>
evalaaron2bb3in(A,B,C) = -1*A + -1*B + C
>= -1*A + -1*B + C
= evalaaron2bb4in(A,B,C)
True ==>
evalaaron2bb3in(A,B,C) = -1*A + -1*B + C
>= -1*A + -1*B + C
= evalaaron2bb5in(A,B,C)
True ==>
evalaaron2bb4in(A,B,C) = -1*A + -1*B + C
>= -1*A + -1*B + C
= evalaaron2bb6in(A,B,-1 + -1*A + C)
True ==>
evalaaron2bb5in(A,B,C) = -1*A + -1*B + C
>= -1*A + -1*B + C
= evalaaron2bb6in(A,1 + A + B,C)
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (1,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (1 + B + C,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (?,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (?,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (?,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (?,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (?,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1},1->{5},5->{6,7,8},6->{9},7->{9},8->{10},9->{5},10->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
KnowledgePropagation
+ Details:
We propagate bounds from predecessors.
* Step 8: LocalSizeboundsProc WORST_CASE(?,O(n^1))
+ Considered Problem:
Rules:
0. evalaaron2start(A,B,C) -> evalaaron2entryin(A,B,C) True (1,1)
1. evalaaron2entryin(A,B,C) -> evalaaron2bb6in(A,C,B) [A >= 0] (1,1)
5. evalaaron2bb6in(A,B,C) -> evalaaron2bb3in(A,B,C) [C >= B && A >= 0] (1 + B + C,1)
6. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [0 >= 1 + D] (1 + B + C,1)
7. evalaaron2bb3in(A,B,C) -> evalaaron2bb4in(A,B,C) [D >= 1] (1 + B + C,1)
8. evalaaron2bb3in(A,B,C) -> evalaaron2bb5in(A,B,C) True (1 + B + C,1)
9. evalaaron2bb4in(A,B,C) -> evalaaron2bb6in(A,B,-1 + -1*A + C) True (2 + 2*B + 2*C,1)
10. evalaaron2bb5in(A,B,C) -> evalaaron2bb6in(A,1 + A + B,C) True (1 + B + C,1)
Signature:
{(evalaaron2bb3in,3)
;(evalaaron2bb4in,3)
;(evalaaron2bb5in,3)
;(evalaaron2bb6in,3)
;(evalaaron2entryin,3)
;(evalaaron2returnin,3)
;(evalaaron2start,3)
;(evalaaron2stop,3)}
Flow Graph:
[0->{1},1->{5},5->{6,7,8},6->{9},7->{9},8->{10},9->{5},10->{5}]
Sizebounds:
(< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C)
(< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, B)
(< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, ?)
(< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, ?)
(< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, ?)
(< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, ?)
(< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, ?)
(<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, ?)
+ Applied Processor:
LocalSizeboundsProc
+ Details:
The problem is already solved.
WORST_CASE(?,O(n^1))