41561
|
1 |
-------------------------------------------------------------------------------
|
|
2 |
-- Longest increasing subsequence of an array of integers
|
|
3 |
-------------------------------------------------------------------------------
|
|
4 |
|
|
5 |
package body Liseq is
|
|
6 |
|
|
7 |
procedure Liseq_length(A: in Vector; L: in out Vector; maxi: out Integer)
|
|
8 |
is
|
|
9 |
maxj,i,j,pmax : Integer;
|
|
10 |
begin
|
|
11 |
L(0) := 1;
|
|
12 |
pmax := 0;
|
|
13 |
maxi := 1;
|
|
14 |
i := 1;
|
|
15 |
while i <= L'Last
|
|
16 |
--# assert
|
|
17 |
--# (for all i2 in Integer range 0 .. i-1 =>
|
|
18 |
--# (L(i2) = Liseq_ends_at(A, i2))) and
|
|
19 |
--# L(pmax) = maxi and L(pmax) = Liseq_prfx(A, i) and
|
|
20 |
--# 0 <= i and i <= L'Last+1 and 0 <= pmax and pmax < i and
|
|
21 |
--# A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
|
|
22 |
loop
|
|
23 |
if A(i) < A(pmax) then
|
|
24 |
maxj := 0;
|
|
25 |
j := 0;
|
|
26 |
while j < i
|
|
27 |
--# assert
|
|
28 |
--# (for all i2 in Integer range 0 .. i-1 =>
|
|
29 |
--# (L(i2) = Liseq_ends_at(A, i2))) and
|
|
30 |
--# L(pmax) = maxi and L(pmax) = Liseq_prfx(A, I) and
|
|
31 |
--# 0 <= i and i <= L'Last and 0 <= pmax and pmax < i and
|
|
32 |
--# 0 <= j and j <= i and
|
|
33 |
--# maxj = Max_ext (A, i, j) and
|
|
34 |
--# A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last;
|
|
35 |
loop
|
|
36 |
if (A(j) <= A(i) and
|
|
37 |
maxj < L(j)) then
|
|
38 |
maxj := L(j);
|
|
39 |
end if;
|
|
40 |
j := j+1;
|
|
41 |
end loop;
|
|
42 |
L(i) := maxj+1;
|
|
43 |
if L(i) > maxi then
|
|
44 |
maxi := maxi+1;
|
|
45 |
pmax := i;
|
|
46 |
end if;
|
|
47 |
else
|
|
48 |
maxi := maxi+1;
|
|
49 |
L(i) := maxi;
|
|
50 |
pmax := i;
|
|
51 |
end if;
|
|
52 |
i := i+1;
|
|
53 |
end loop;
|
|
54 |
end Liseq_length;
|
|
55 |
end Liseq;
|