1499 lines
34 KiB
MiniZinc
1499 lines
34 KiB
MiniZinc
%
|
|
% jp-encoding.mzn
|
|
%
|
|
|
|
%
|
|
% There are several popular character encodings in Japan.
|
|
% (EUC-JP, SJIS, UTF-8)
|
|
%
|
|
% If they are mixed into one text file (by accident or something),
|
|
% text information will be lost.
|
|
% So we can define a problem "recovering original encodings" for byte stream.
|
|
%
|
|
% In this problem, byte stream (as variable 'stream') is given as input
|
|
% and encodings are assigned as output (as variable 'encoding').
|
|
%
|
|
|
|
include "table.mzn";
|
|
|
|
% *_score tables have -log(probability of appearance) * 10 for each encoding.
|
|
|
|
array[1..256] of int: sjis_score = [
|
|
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 57, 135, 135, 135, 135, 135,
|
|
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
|
|
74, 135, 128, 119, 135, 100, 135, 135, 96, 96, 112, 104, 106, 92, 106, 107,
|
|
97, 92, 99, 95, 98, 106, 107, 103, 97, 101, 105, 135, 135, 111, 135, 119,
|
|
65, 46, 45, 64, 75, 74, 79, 78, 71, 74, 79, 76, 71, 79, 59, 64,
|
|
81, 78, 70, 67, 80, 81, 70, 82, 69, 81, 75, 72, 62, 60, 73, 70,
|
|
76, 79, 75, 66, 77, 75, 78, 73, 77, 43, 43, 79, 54, 68, 68, 61,
|
|
73, 67, 80, 66, 69, 53, 51, 72, 73, 68, 74, 71, 77, 80, 77, 135,
|
|
77, 28, 11, 51, 75, 73, 69, 69, 51, 47, 49, 49, 44, 49, 41, 47,
|
|
44, 48, 48, 47, 50, 46, 45, 48, 63, 76, 75, 79, 74, 68, 63, 73,
|
|
50, 67, 40, 80, 45, 79, 56, 71, 59, 42, 45, 55, 67, 49, 68, 58,
|
|
69, 53, 65, 54, 69, 45, 57, 50, 64, 60, 65, 54, 67, 44, 49, 58,
|
|
66, 47, 58, 74, 43, 47, 43, 59, 43, 45, 62, 62, 40, 45, 60, 72,
|
|
71, 69, 72, 68, 61, 80, 62, 68, 72, 68, 70, 75, 51, 66, 67, 61,
|
|
47, 56, 59, 61, 62, 53, 53, 47, 51, 43, 49, 60, 74, 60, 83, 74,
|
|
47, 47, 76, 71, 78, 82, 77, 83, 80, 81, 70, 67, 67, 135, 135, 135
|
|
];
|
|
array[1..256] of int: eucjp_score = [
|
|
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 57, 135, 135, 135, 135, 135,
|
|
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
|
|
74, 135, 128, 119, 135, 100, 135, 135, 96, 96, 112, 104, 106, 92, 106, 107,
|
|
97, 92, 99, 95, 98, 106, 107, 103, 97, 101, 105, 135, 135, 111, 135, 119,
|
|
135, 112, 114, 100, 108, 102, 135, 113, 121, 110, 124, 135, 111, 106, 111, 111,
|
|
100, 135, 114, 109, 112, 124, 135, 135, 124, 119, 128, 128, 121, 128, 135, 135,
|
|
135, 94, 128, 102, 104, 95, 113, 97, 108, 90, 124, 124, 99, 101, 95, 90,
|
|
105, 135, 93, 99, 94, 108, 128, 113, 135, 124, 117, 135, 135, 135, 135, 135,
|
|
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
|
|
135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135, 135,
|
|
135, 28, 41, 44, 11, 50, 45, 72, 55, 64, 57, 42, 45, 54, 65, 46,
|
|
49, 49, 51, 48, 50, 48, 54, 41, 45, 45, 52, 44, 48, 45, 49, 39,
|
|
43, 50, 51, 43, 49, 53, 40, 43, 41, 50, 34, 36, 48, 45, 38, 43,
|
|
53, 66, 62, 66, 61, 62, 49, 50, 59, 62, 62, 63, 63, 68, 50, 63,
|
|
63, 58, 46, 55, 57, 59, 58, 52, 50, 46, 49, 43, 48, 58, 63, 58,
|
|
73, 67, 46, 46, 70, 68, 58, 66, 71, 73, 72, 74, 66, 61, 58, 135
|
|
];
|
|
array[1..256] of int: utf8_score = [
|
|
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 61, 139, 139, 139, 139, 139,
|
|
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139,
|
|
78, 139, 132, 123, 139, 104, 139, 139, 100, 100, 116, 108, 110, 96, 110, 111,
|
|
101, 96, 103, 99, 102, 110, 111, 107, 101, 105, 109, 139, 139, 115, 139, 139,
|
|
139, 116, 118, 104, 112, 107, 139, 117, 125, 114, 128, 139, 115, 110, 115, 115,
|
|
104, 139, 118, 113, 116, 128, 139, 139, 128, 123, 132, 132, 125, 132, 139, 139,
|
|
139, 98, 132, 107, 108, 99, 117, 101, 112, 95, 128, 128, 103, 105, 99, 94,
|
|
109, 139, 97, 103, 98, 112, 132, 117, 139, 128, 121, 139, 139, 139, 139, 139,
|
|
36, 17, 27, 51, 42, 55, 47, 54, 41, 40, 49, 38, 42, 47, 64, 48,
|
|
53, 52, 49, 45, 56, 51, 56, 46, 58, 50, 58, 52, 57, 51, 65, 46,
|
|
51, 53, 63, 48, 54, 54, 44, 48, 45, 54, 45, 46, 61, 53, 42, 47,
|
|
53, 61, 63, 57, 61, 63, 62, 62, 48, 59, 45, 53, 39, 57, 49, 57,
|
|
139, 139, 139, 132, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 118, 139,
|
|
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139,
|
|
139, 139, 68, 14, 42, 36, 40, 44, 44, 47, 139, 139, 139, 139, 139, 40,
|
|
139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139, 139
|
|
];
|
|
|
|
|
|
%
|
|
% labels for encoding
|
|
%
|
|
|
|
int: e_ascii = 0;
|
|
int: e_euc_jp = 1;
|
|
int: e_sjis = 2;
|
|
int: e_utf8 = 3;
|
|
int: e_unknown = 4;
|
|
|
|
%
|
|
% labels for byte_status
|
|
%
|
|
|
|
int: b_ascii = 0;
|
|
|
|
int: b_euc1 = 1;
|
|
int: b_euc2 = 2;
|
|
|
|
int: b_sjis1_1 = 3;
|
|
int: b_sjis2_1 = 4;
|
|
int: b_sjis2_2 = 5;
|
|
|
|
int: b_utf8_2_1 = 6;
|
|
int: b_utf8_2_2 = 7;
|
|
int: b_utf8_3_1 = 8;
|
|
int: b_utf8_3_2 = 9;
|
|
int: b_utf8_3_3 = 10;
|
|
int: b_utf8_4_1 = 11;
|
|
int: b_utf8_4_2 = 12;
|
|
int: b_utf8_4_3 = 13;
|
|
int: b_utf8_4_4 = 14;
|
|
|
|
int: b_unknown = 15;
|
|
|
|
%
|
|
% test data
|
|
%
|
|
% int: len = 12;
|
|
% array[1..len] of int: stream = [ 227, 129, 138, 227, 129, 175, 227, 130, 136, 227, 129, 134 ];
|
|
int: len;
|
|
set of int: rng = 1..len;
|
|
|
|
array[rng] of int: stream;
|
|
|
|
% int: len = 3 ;
|
|
% array[rng] of int: stream = [ 65, 66, 67 ];
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Variables
|
|
|
|
array[rng] of var 0..b_unknown: byte_status;
|
|
array[rng] of var 0..e_unknown: encoding;
|
|
array[rng] of var 0..1: char_start;
|
|
|
|
set of int: scoreType = 0..max(i in 1..256)(eucjp_score[i] + sjis_score[i] + utf8_score[i]) + 1000;
|
|
int: maxObj = len * (max(i in 1..256)(eucjp_score[i] + sjis_score[i] + utf8_score[i]) + 1000);
|
|
var 0..maxObj: objective;
|
|
|
|
constraint objective = sum (i in rng) (
|
|
score_of(encoding[i],stream[i])
|
|
);
|
|
|
|
function var scoreType: score_of(var int: encoding_i, int: stream_i) =
|
|
let{
|
|
var scoreType: score_i;
|
|
constraint score_computation(encoding_i,stream_i, score_i);
|
|
} in score_i;
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Constraints
|
|
|
|
constraint forall (i in rng) (
|
|
if i >= 2 then link_statuses(byte_status[i],byte_status[i-1]) else true endif
|
|
/\
|
|
link_vars(encoding[i],byte_status[i],char_start[i])
|
|
/\
|
|
init(byte_status[i],i)
|
|
/\
|
|
stream_to_status(i,stream,byte_status[i])
|
|
);
|
|
|
|
|
|
predicate stream_to_status(int:i, array[int] of int: stream, var int: byte_status_i) =
|
|
( forall([
|
|
%
|
|
% ASCII
|
|
%
|
|
if (stream[i] < 128) then true else
|
|
byte_status_i != b_ascii endif
|
|
,
|
|
%
|
|
% UTF-8
|
|
%
|
|
|
|
% C2-DF, 80-BF
|
|
if (i >= len) then
|
|
byte_status_i != b_utf8_2_1
|
|
else
|
|
if ((194 <= stream[i] /\ stream[i] <= 223)
|
|
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191))
|
|
then true else
|
|
byte_status_i != b_utf8_2_1
|
|
endif
|
|
endif
|
|
,
|
|
|
|
% E0-EF, 80-BF, 80-BF
|
|
if (i >= len - 1) then
|
|
byte_status_i != b_utf8_3_1
|
|
else
|
|
if ((224 <= stream[i] /\ stream[i] <= 239)
|
|
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191)
|
|
/\ (128 <= stream[i+2] /\ stream[i+2] <= 191))
|
|
then true else
|
|
byte_status_i != b_utf8_3_1
|
|
endif
|
|
endif
|
|
,
|
|
|
|
% F0-F7, 80-BF, 80-BF, 80-BF
|
|
if (i >= len - 2) then
|
|
byte_status_i != b_utf8_4_1
|
|
else
|
|
if (240 <= stream[i] /\ stream[i] <= 247
|
|
/\ 128 <= stream[i+1] /\ stream[i+1] <= 191
|
|
/\ 128 <= stream[i+2] /\ stream[i+2] <= 191
|
|
/\ 128 <= stream[i+3] /\ stream[i+3] <= 191)
|
|
then true else
|
|
byte_status_i != b_utf8_4_1
|
|
endif
|
|
endif
|
|
,
|
|
|
|
%
|
|
% EUC-JP (CP51932)
|
|
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
|
|
%
|
|
if (i >= len) then
|
|
byte_status_i !=b_euc1
|
|
else
|
|
if ((161 <= stream[i] /\ stream[i] <= 168)
|
|
\/ (173 = stream[i])
|
|
\/ (176 <= stream[i] /\ stream[i] <= 244)
|
|
\/ (249 <= stream[i] /\ stream[i] <= 252))
|
|
/\ (161 <= stream[i+1] /\ stream[i+1] <= 254)
|
|
then true else
|
|
byte_status_i != b_euc1
|
|
endif
|
|
endif
|
|
,
|
|
|
|
%
|
|
% SJIS
|
|
%
|
|
|
|
% (A1-DF)
|
|
if (161 <= stream[i] /\ stream[i] <= 223)
|
|
then true else
|
|
byte_status_i != b_sjis1_1
|
|
endif
|
|
,
|
|
|
|
% (81-9F, E0-FC), (40-7E, 80-FC)
|
|
if (i >= len) then
|
|
byte_status_i != b_sjis2_1
|
|
else
|
|
if ((129 <= stream[i] /\ stream[i] <= 159)
|
|
\/ (224 <= stream[i] /\ stream[i] <= 252))
|
|
/\ ((64 <= stream[i+1] /\ stream[i+1] <= 126)
|
|
\/ (128 <= stream[i+1] /\ stream[i+1] <= 252))
|
|
then true else
|
|
byte_status_i != b_sjis2_1
|
|
endif
|
|
endif
|
|
])
|
|
);
|
|
|
|
predicate stream_to_status_old(int:i, array[int] of int: stream, var int: byte_status_i) =
|
|
( forall([
|
|
%
|
|
% ASCII
|
|
%
|
|
if (stream[i] < 128) then true else
|
|
byte_status_i != b_ascii endif
|
|
,
|
|
%
|
|
% UTF-8
|
|
%
|
|
|
|
% C2-DF, 80-BF
|
|
if (i >= len) then
|
|
byte_status_i != b_utf8_2_1
|
|
else
|
|
byte_status_i = b_utf8_2_1 ->
|
|
((194 <= stream[i] /\ stream[i] <= 223)
|
|
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191))
|
|
endif
|
|
,
|
|
|
|
% E0-EF, 80-BF, 80-BF
|
|
if (i >= len - 1) then
|
|
byte_status_i != b_utf8_3_1
|
|
else
|
|
byte_status_i = b_utf8_3_1 ->
|
|
((224 <= stream[i] /\ stream[i] <= 239)
|
|
/\ (128 <= stream[i+1] /\ stream[i+1] <= 191)
|
|
/\ (128 <= stream[i+2] /\ stream[i+2] <= 191))
|
|
endif
|
|
,
|
|
|
|
% F0-F7, 80-BF, 80-BF, 80-BF
|
|
if (i >= len - 2) then
|
|
byte_status_i != b_utf8_4_1
|
|
else
|
|
byte_status_i = b_utf8_4_1 ->
|
|
(240 <= stream[i] /\ stream[i] <= 247
|
|
/\ 128 <= stream[i+1] /\ stream[i+1] <= 191
|
|
/\ 128 <= stream[i+2] /\ stream[i+2] <= 191
|
|
/\ 128 <= stream[i+3] /\ stream[i+3] <= 191)
|
|
endif
|
|
,
|
|
|
|
%
|
|
% EUC-JP (CP51932)
|
|
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
|
|
%
|
|
if (i >= len) then
|
|
byte_status_i !=b_euc1
|
|
else
|
|
byte_status_i = b_euc1 ->
|
|
((161 <= stream[i] /\ stream[i] <= 168)
|
|
\/ (173 = stream[i])
|
|
\/ (176 <= stream[i] /\ stream[i] <= 244)
|
|
\/ (249 <= stream[i] /\ stream[i] <= 252))
|
|
/\ (161 <= stream[i+1] /\ stream[i+1] <= 254)
|
|
endif
|
|
,
|
|
|
|
%
|
|
% SJIS
|
|
%
|
|
|
|
% (A1-DF)
|
|
byte_status_i = b_sjis1_1 ->
|
|
(161 <= stream[i] /\ stream[i] <= 223)
|
|
,
|
|
|
|
% (81-9F, E0-FC), (40-7E, 80-FC)
|
|
if (i >= len) then
|
|
byte_status_i != b_sjis2_1
|
|
else
|
|
byte_status_i = b_sjis2_1 ->
|
|
((129 <= stream[i] /\ stream[i] <= 159)
|
|
\/ (224 <= stream[i] /\ stream[i] <= 252))
|
|
/\ ((64 <= stream[i+1] /\ stream[i+1] <= 126)
|
|
\/ (128 <= stream[i+1] /\ stream[i+1] <= 252))
|
|
endif
|
|
])
|
|
);
|
|
|
|
|
|
predicate init(var int: byte_status_i, int: i) =
|
|
( forall([
|
|
%
|
|
% UTF-8
|
|
%
|
|
|
|
% C2-DF, 80-BF
|
|
if (i < 2) then
|
|
byte_status_i != b_utf8_2_2
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
|
|
% E0-EF, 80-BF, 80-BF
|
|
if (i < 2) then
|
|
byte_status_i != b_utf8_3_2
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
if (i < 3) then
|
|
byte_status_i != b_utf8_3_3
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
|
|
% F0-F7, 80-BF, 80-BF, 80-BF
|
|
if (i < 2) then
|
|
byte_status_i != b_utf8_4_2
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
if (i < 3) then
|
|
byte_status_i != b_utf8_4_3
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
if (i < 4) then
|
|
byte_status_i != b_utf8_4_4
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
|
|
%
|
|
% EUC-JP (CP51932)
|
|
% (A1-A8, AD, B0-F4, F9-FC), (A1-FE)
|
|
%
|
|
if (i < 2) then
|
|
byte_status_i != b_euc2
|
|
else
|
|
true
|
|
endif
|
|
,
|
|
|
|
%
|
|
% SJIS
|
|
%
|
|
|
|
% (A1-DF)
|
|
|
|
% (81-9F, E0-FC), (40-7E, 80-FC)
|
|
if (i < 2) then
|
|
byte_status_i != b_sjis2_2
|
|
else
|
|
true
|
|
endif
|
|
])
|
|
);
|
|
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Search and Solve
|
|
|
|
solve
|
|
:: seq_search([
|
|
int_search(byte_status, first_fail, indomain_split, complete),
|
|
int_search(char_start, input_order, indomain_max, complete),
|
|
int_search(encoding, first_fail, indomain_split, complete)
|
|
])
|
|
minimize objective;
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Output
|
|
|
|
output [
|
|
"encoding = ", show(encoding), ";\n",
|
|
"byte_status = ", show(byte_status), ";\n",
|
|
"char_start = ", show(char_start), ";\n",
|
|
"constraint objective = ", show(objective), ";\n"
|
|
];
|
|
|
|
%------------------------------------------------------------------------------%
|
|
%% ---------- DATA ----------
|
|
len = 824;
|
|
stream = [
|
|
130,
|
|
187,
|
|
130,
|
|
177,
|
|
130,
|
|
197,
|
|
129,
|
|
65,
|
|
147,
|
|
250,
|
|
130,
|
|
204,
|
|
150,
|
|
218,
|
|
130,
|
|
170,
|
|
140,
|
|
169,
|
|
130,
|
|
166,
|
|
130,
|
|
200,
|
|
130,
|
|
173,
|
|
130,
|
|
200,
|
|
130,
|
|
233,
|
|
130,
|
|
198,
|
|
129,
|
|
65,
|
|
146,
|
|
78,
|
|
130,
|
|
197,
|
|
130,
|
|
224,
|
|
139,
|
|
67,
|
|
150,
|
|
161,
|
|
130,
|
|
240,
|
|
136,
|
|
171,
|
|
130,
|
|
233,
|
|
130,
|
|
170,
|
|
130,
|
|
193,
|
|
130,
|
|
196,
|
|
129,
|
|
65,
|
|
130,
|
|
177,
|
|
130,
|
|
204,
|
|
150,
|
|
229,
|
|
130,
|
|
204,
|
|
139,
|
|
223,
|
|
143,
|
|
138,
|
|
130,
|
|
214,
|
|
130,
|
|
205,
|
|
145,
|
|
171,
|
|
130,
|
|
212,
|
|
130,
|
|
221,
|
|
130,
|
|
240,
|
|
130,
|
|
181,
|
|
130,
|
|
200,
|
|
130,
|
|
162,
|
|
142,
|
|
150,
|
|
130,
|
|
201,
|
|
130,
|
|
200,
|
|
130,
|
|
193,
|
|
130,
|
|
196,
|
|
130,
|
|
181,
|
|
130,
|
|
220,
|
|
130,
|
|
193,
|
|
130,
|
|
189,
|
|
130,
|
|
204,
|
|
130,
|
|
197,
|
|
130,
|
|
160,
|
|
130,
|
|
233,
|
|
129,
|
|
66,
|
|
10,
|
|
84,
|
|
104,
|
|
101,
|
|
32,
|
|
113,
|
|
117,
|
|
105,
|
|
99,
|
|
107,
|
|
32,
|
|
98,
|
|
114,
|
|
111,
|
|
119,
|
|
110,
|
|
32,
|
|
102,
|
|
111,
|
|
120,
|
|
32,
|
|
106,
|
|
117,
|
|
109,
|
|
112,
|
|
115,
|
|
32,
|
|
111,
|
|
118,
|
|
101,
|
|
114,
|
|
32,
|
|
116,
|
|
104,
|
|
101,
|
|
32,
|
|
108,
|
|
97,
|
|
122,
|
|
121,
|
|
32,
|
|
100,
|
|
111,
|
|
103,
|
|
10,
|
|
130,
|
|
187,
|
|
130,
|
|
234,
|
|
130,
|
|
170,
|
|
129,
|
|
65,
|
|
130,
|
|
177,
|
|
130,
|
|
204,
|
|
146,
|
|
106,
|
|
130,
|
|
204,
|
|
130,
|
|
217,
|
|
130,
|
|
169,
|
|
130,
|
|
201,
|
|
130,
|
|
205,
|
|
146,
|
|
78,
|
|
130,
|
|
224,
|
|
130,
|
|
162,
|
|
130,
|
|
200,
|
|
130,
|
|
162,
|
|
129,
|
|
66,
|
|
10,
|
|
178,
|
|
191,
|
|
184,
|
|
206,
|
|
164,
|
|
171,
|
|
164,
|
|
200,
|
|
177,
|
|
190,
|
|
164,
|
|
166,
|
|
164,
|
|
200,
|
|
161,
|
|
162,
|
|
164,
|
|
179,
|
|
164,
|
|
206,
|
|
198,
|
|
243,
|
|
187,
|
|
176,
|
|
199,
|
|
175,
|
|
161,
|
|
162,
|
|
181,
|
|
254,
|
|
197,
|
|
212,
|
|
164,
|
|
203,
|
|
164,
|
|
207,
|
|
161,
|
|
162,
|
|
195,
|
|
207,
|
|
191,
|
|
204,
|
|
164,
|
|
200,
|
|
164,
|
|
171,
|
|
196,
|
|
212,
|
|
201,
|
|
247,
|
|
164,
|
|
200,
|
|
164,
|
|
171,
|
|
178,
|
|
208,
|
|
187,
|
|
246,
|
|
164,
|
|
200,
|
|
164,
|
|
171,
|
|
241,
|
|
192,
|
|
241,
|
|
188,
|
|
164,
|
|
200,
|
|
164,
|
|
171,
|
|
177,
|
|
190,
|
|
164,
|
|
166,
|
|
186,
|
|
210,
|
|
164,
|
|
172,
|
|
164,
|
|
196,
|
|
164,
|
|
197,
|
|
164,
|
|
164,
|
|
164,
|
|
198,
|
|
181,
|
|
175,
|
|
164,
|
|
195,
|
|
164,
|
|
191,
|
|
161,
|
|
163,
|
|
10,
|
|
151,
|
|
133,
|
|
144,
|
|
182,
|
|
150,
|
|
229,
|
|
130,
|
|
170,
|
|
129,
|
|
65,
|
|
142,
|
|
233,
|
|
144,
|
|
157,
|
|
145,
|
|
229,
|
|
152,
|
|
72,
|
|
130,
|
|
201,
|
|
130,
|
|
160,
|
|
130,
|
|
233,
|
|
136,
|
|
200,
|
|
143,
|
|
227,
|
|
130,
|
|
205,
|
|
129,
|
|
65,
|
|
130,
|
|
177,
|
|
130,
|
|
204,
|
|
146,
|
|
106,
|
|
130,
|
|
204,
|
|
130,
|
|
217,
|
|
130,
|
|
169,
|
|
130,
|
|
201,
|
|
130,
|
|
224,
|
|
129,
|
|
65,
|
|
137,
|
|
74,
|
|
130,
|
|
226,
|
|
130,
|
|
221,
|
|
130,
|
|
240,
|
|
130,
|
|
183,
|
|
130,
|
|
233,
|
|
142,
|
|
115,
|
|
143,
|
|
151,
|
|
138,
|
|
125,
|
|
130,
|
|
226,
|
|
157,
|
|
134,
|
|
137,
|
|
71,
|
|
150,
|
|
88,
|
|
142,
|
|
113,
|
|
130,
|
|
170,
|
|
129,
|
|
65,
|
|
130,
|
|
224,
|
|
130,
|
|
164,
|
|
147,
|
|
241,
|
|
142,
|
|
79,
|
|
144,
|
|
108,
|
|
130,
|
|
205,
|
|
130,
|
|
160,
|
|
130,
|
|
232,
|
|
130,
|
|
187,
|
|
130,
|
|
164,
|
|
130,
|
|
200,
|
|
130,
|
|
224,
|
|
130,
|
|
204,
|
|
130,
|
|
197,
|
|
130,
|
|
160,
|
|
130,
|
|
233,
|
|
129,
|
|
66,
|
|
10,
|
|
227,
|
|
129,
|
|
157,
|
|
227,
|
|
130,
|
|
140,
|
|
227,
|
|
129,
|
|
140,
|
|
227,
|
|
128,
|
|
129,
|
|
227,
|
|
129,
|
|
147,
|
|
227,
|
|
129,
|
|
174,
|
|
231,
|
|
148,
|
|
183,
|
|
227,
|
|
129,
|
|
174,
|
|
227,
|
|
129,
|
|
187,
|
|
227,
|
|
129,
|
|
139,
|
|
227,
|
|
129,
|
|
171,
|
|
227,
|
|
129,
|
|
175,
|
|
232,
|
|
170,
|
|
176,
|
|
227,
|
|
130,
|
|
130,
|
|
227,
|
|
129,
|
|
132,
|
|
227,
|
|
129,
|
|
170,
|
|
227,
|
|
129,
|
|
132,
|
|
227,
|
|
128,
|
|
130,
|
|
10,
|
|
144,
|
|
101,
|
|
143,
|
|
247,
|
|
130,
|
|
232,
|
|
130,
|
|
204,
|
|
150,
|
|
179,
|
|
147,
|
|
83,
|
|
150,
|
|
67,
|
|
130,
|
|
197,
|
|
143,
|
|
172,
|
|
139,
|
|
159,
|
|
130,
|
|
204,
|
|
142,
|
|
158,
|
|
130,
|
|
169,
|
|
130,
|
|
231,
|
|
145,
|
|
185,
|
|
130,
|
|
206,
|
|
130,
|
|
169,
|
|
130,
|
|
232,
|
|
130,
|
|
181,
|
|
130,
|
|
196,
|
|
130,
|
|
162,
|
|
130,
|
|
233,
|
|
129,
|
|
66,
|
|
10,
|
|
229,
|
|
136,
|
|
165,
|
|
230,
|
|
174,
|
|
181,
|
|
230,
|
|
183,
|
|
177,
|
|
227,
|
|
129,
|
|
132,
|
|
231,
|
|
144,
|
|
134,
|
|
231,
|
|
148,
|
|
177,
|
|
227,
|
|
129,
|
|
167,
|
|
227,
|
|
130,
|
|
130,
|
|
227,
|
|
129,
|
|
170,
|
|
227,
|
|
129,
|
|
132,
|
|
227,
|
|
128,
|
|
130,
|
|
10,
|
|
142,
|
|
227,
|
|
146,
|
|
142,
|
|
130,
|
|
226,
|
|
129,
|
|
91,
|
|
130,
|
|
162,
|
|
129,
|
|
66,
|
|
130,
|
|
198,
|
|
154,
|
|
146,
|
|
130,
|
|
181,
|
|
130,
|
|
189,
|
|
130,
|
|
169,
|
|
130,
|
|
231,
|
|
130,
|
|
197,
|
|
130,
|
|
160,
|
|
130,
|
|
233,
|
|
129,
|
|
66,
|
|
143,
|
|
172,
|
|
142,
|
|
103,
|
|
130,
|
|
201,
|
|
149,
|
|
137,
|
|
130,
|
|
212,
|
|
130,
|
|
179,
|
|
130,
|
|
193,
|
|
130,
|
|
196,
|
|
139,
|
|
65,
|
|
130,
|
|
193,
|
|
130,
|
|
196,
|
|
151,
|
|
136,
|
|
130,
|
|
189,
|
|
142,
|
|
158,
|
|
129,
|
|
65,
|
|
130,
|
|
168,
|
|
130,
|
|
226,
|
|
130,
|
|
182,
|
|
130,
|
|
170,
|
|
145,
|
|
229,
|
|
130,
|
|
171,
|
|
130,
|
|
200,
|
|
138,
|
|
225,
|
|
130,
|
|
240,
|
|
130,
|
|
181,
|
|
130,
|
|
196,
|
|
147,
|
|
241,
|
|
138,
|
|
75,
|
|
130,
|
|
174,
|
|
130,
|
|
231,
|
|
130,
|
|
162,
|
|
130,
|
|
169,
|
|
130,
|
|
231,
|
|
148,
|
|
242,
|
|
130,
|
|
209,
|
|
141,
|
|
126,
|
|
130,
|
|
232,
|
|
130,
|
|
196,
|
|
141,
|
|
152,
|
|
130,
|
|
240,
|
|
148,
|
|
178,
|
|
130,
|
|
169,
|
|
130,
|
|
183,
|
|
147,
|
|
122,
|
|
130,
|
|
170,
|
|
130,
|
|
160,
|
|
130,
|
|
233,
|
|
130,
|
|
169,
|
|
130,
|
|
198,
|
|
137,
|
|
93,
|
|
130,
|
|
193,
|
|
130,
|
|
189,
|
|
130,
|
|
169,
|
|
130,
|
|
231,
|
|
129,
|
|
65,
|
|
130,
|
|
177,
|
|
130,
|
|
204,
|
|
142,
|
|
159,
|
|
130,
|
|
205,
|
|
148,
|
|
178,
|
|
130,
|
|
169,
|
|
130,
|
|
179,
|
|
130,
|
|
184,
|
|
130,
|
|
201,
|
|
148,
|
|
242,
|
|
130,
|
|
241,
|
|
130,
|
|
197,
|
|
140,
|
|
169,
|
|
130,
|
|
185,
|
|
130,
|
|
220,
|
|
130,
|
|
183,
|
|
130,
|
|
198,
|
|
147,
|
|
154,
|
|
130,
|
|
166,
|
|
130,
|
|
189,
|
|
129,
|
|
66,
|
|
10,
|
|
137,
|
|
189,
|
|
140,
|
|
204,
|
|
130,
|
|
169,
|
|
130,
|
|
198,
|
|
137,
|
|
93,
|
|
130,
|
|
164,
|
|
130,
|
|
198,
|
|
129,
|
|
65,
|
|
130,
|
|
177,
|
|
130,
|
|
204,
|
|
147,
|
|
241,
|
|
142,
|
|
79,
|
|
148,
|
|
78,
|
|
129,
|
|
65,
|
|
139,
|
|
158,
|
|
147,
|
|
115,
|
|
130,
|
|
201,
|
|
130,
|
|
205,
|
|
129,
|
|
65,
|
|
146,
|
|
110,
|
|
144,
|
|
107,
|
|
130,
|
|
198,
|
|
130,
|
|
169,
|
|
146,
|
|
210,
|
|
149,
|
|
151,
|
|
130,
|
|
198,
|
|
130,
|
|
169,
|
|
137,
|
|
206,
|
|
142,
|
|
150,
|
|
130,
|
|
198,
|
|
130,
|
|
169,
|
|
233,
|
|
95,
|
|
233,
|
|
91,
|
|
130,
|
|
198,
|
|
130,
|
|
169,
|
|
137,
|
|
93,
|
|
130,
|
|
164,
|
|
141,
|
|
208,
|
|
130,
|
|
170,
|
|
130,
|
|
194,
|
|
130,
|
|
195,
|
|
130,
|
|
162,
|
|
130,
|
|
196,
|
|
139,
|
|
78,
|
|
130,
|
|
193,
|
|
130,
|
|
189,
|
|
129,
|
|
66,
|
|
10
|
|
];
|
|
%% ---------- GENERATED TABLE ----------
|
|
include "table.mzn";
|
|
|
|
predicate score_computation(var 0..e_unknown: encoding_i, var 0..255: stream_i,
|
|
var scoreType: score_i) =
|
|
table_int([encoding_i, stream_i, score_i], array2d(1..1280,
|
|
index_set([encoding_i, stream_i, score_i]), [0, 0, 0, 0, 1, 0, 0, 2, 0, 0,
|
|
3, 0, 0, 4, 0, 0, 5, 0, 0, 6, 0, 0, 7, 0, 0, 8, 0, 0, 9, 0, 0, 10, 0, 0,
|
|
11, 0, 0, 12, 0, 0, 13, 0, 0, 14, 0, 0, 15, 0, 0, 16, 0, 0, 17, 0, 0, 18,
|
|
0, 0, 19, 0, 0, 20, 0, 0, 21, 0, 0, 22, 0, 0, 23, 0, 0, 24, 0, 0, 25, 0, 0,
|
|
26, 0, 0, 27, 0, 0, 28, 0, 0, 29, 0, 0, 30, 0, 0, 31, 0, 0, 32, 0, 0, 33,
|
|
0, 0, 34, 0, 0, 35, 0, 0, 36, 0, 0, 37, 0, 0, 38, 0, 0, 39, 0, 0, 40, 0, 0,
|
|
41, 0, 0, 42, 0, 0, 43, 0, 0, 44, 0, 0, 45, 0, 0, 46, 0, 0, 47, 0, 0, 48,
|
|
0, 0, 49, 0, 0, 50, 0, 0, 51, 0, 0, 52, 0, 0, 53, 0, 0, 54, 0, 0, 55, 0, 0,
|
|
56, 0, 0, 57, 0, 0, 58, 0, 0, 59, 0, 0, 60, 0, 0, 61, 0, 0, 62, 0, 0, 63,
|
|
0, 0, 64, 0, 0, 65, 0, 0, 66, 0, 0, 67, 0, 0, 68, 0, 0, 69, 0, 0, 70, 0, 0,
|
|
71, 0, 0, 72, 0, 0, 73, 0, 0, 74, 0, 0, 75, 0, 0, 76, 0, 0, 77, 0, 0, 78,
|
|
0, 0, 79, 0, 0, 80, 0, 0, 81, 0, 0, 82, 0, 0, 83, 0, 0, 84, 0, 0, 85, 0, 0,
|
|
86, 0, 0, 87, 0, 0, 88, 0, 0, 89, 0, 0, 90, 0, 0, 91, 0, 0, 92, 0, 0, 93,
|
|
0, 0, 94, 0, 0, 95, 0, 0, 96, 0, 0, 97, 0, 0, 98, 0, 0, 99, 0, 0, 100, 0,
|
|
0, 101, 0, 0, 102, 0, 0, 103, 0, 0, 104, 0, 0, 105, 0, 0, 106, 0, 0, 107,
|
|
0, 0, 108, 0, 0, 109, 0, 0, 110, 0, 0, 111, 0, 0, 112, 0, 0, 113, 0, 0,
|
|
114, 0, 0, 115, 0, 0, 116, 0, 0, 117, 0, 0, 118, 0, 0, 119, 0, 0, 120, 0,
|
|
0, 121, 0, 0, 122, 0, 0, 123, 0, 0, 124, 0, 0, 125, 0, 0, 126, 0, 0, 127,
|
|
0, 0, 128, 0, 0, 129, 0, 0, 130, 0, 0, 131, 0, 0, 132, 0, 0, 133, 0, 0,
|
|
134, 0, 0, 135, 0, 0, 136, 0, 0, 137, 0, 0, 138, 0, 0, 139, 0, 0, 140, 0,
|
|
0, 141, 0, 0, 142, 0, 0, 143, 0, 0, 144, 0, 0, 145, 0, 0, 146, 0, 0, 147,
|
|
0, 0, 148, 0, 0, 149, 0, 0, 150, 0, 0, 151, 0, 0, 152, 0, 0, 153, 0, 0,
|
|
154, 0, 0, 155, 0, 0, 156, 0, 0, 157, 0, 0, 158, 0, 0, 159, 0, 0, 160, 0,
|
|
0, 161, 0, 0, 162, 0, 0, 163, 0, 0, 164, 0, 0, 165, 0, 0, 166, 0, 0, 167,
|
|
0, 0, 168, 0, 0, 169, 0, 0, 170, 0, 0, 171, 0, 0, 172, 0, 0, 173, 0, 0,
|
|
174, 0, 0, 175, 0, 0, 176, 0, 0, 177, 0, 0, 178, 0, 0, 179, 0, 0, 180, 0,
|
|
0, 181, 0, 0, 182, 0, 0, 183, 0, 0, 184, 0, 0, 185, 0, 0, 186, 0, 0, 187,
|
|
0, 0, 188, 0, 0, 189, 0, 0, 190, 0, 0, 191, 0, 0, 192, 0, 0, 193, 0, 0,
|
|
194, 0, 0, 195, 0, 0, 196, 0, 0, 197, 0, 0, 198, 0, 0, 199, 0, 0, 200, 0,
|
|
0, 201, 0, 0, 202, 0, 0, 203, 0, 0, 204, 0, 0, 205, 0, 0, 206, 0, 0, 207,
|
|
0, 0, 208, 0, 0, 209, 0, 0, 210, 0, 0, 211, 0, 0, 212, 0, 0, 213, 0, 0,
|
|
214, 0, 0, 215, 0, 0, 216, 0, 0, 217, 0, 0, 218, 0, 0, 219, 0, 0, 220, 0,
|
|
0, 221, 0, 0, 222, 0, 0, 223, 0, 0, 224, 0, 0, 225, 0, 0, 226, 0, 0, 227,
|
|
0, 0, 228, 0, 0, 229, 0, 0, 230, 0, 0, 231, 0, 0, 232, 0, 0, 233, 0, 0,
|
|
234, 0, 0, 235, 0, 0, 236, 0, 0, 237, 0, 0, 238, 0, 0, 239, 0, 0, 240, 0,
|
|
0, 241, 0, 0, 242, 0, 0, 243, 0, 0, 244, 0, 0, 245, 0, 0, 246, 0, 0, 247,
|
|
0, 0, 248, 0, 0, 249, 0, 0, 250, 0, 0, 251, 0, 0, 252, 0, 0, 253, 0, 0,
|
|
254, 0, 0, 255, 0, 1, 164, 11, 1, 161, 28, 1, 202, 34, 1, 203, 36, 1, 206,
|
|
38, 1, 191, 39, 1, 198, 40, 1, 162, 41, 1, 183, 41, 1, 200, 41, 1, 171, 42,
|
|
1, 192, 43, 1, 195, 43, 1, 199, 43, 1, 207, 43, 1, 235, 43, 1, 163, 44, 1,
|
|
187, 44, 1, 166, 45, 1, 172, 45, 1, 184, 45, 1, 185, 45, 1, 189, 45, 1,
|
|
205, 45, 1, 175, 46, 1, 226, 46, 1, 233, 46, 1, 242, 46, 1, 243, 46, 1,
|
|
179, 48, 1, 181, 48, 1, 188, 48, 1, 204, 48, 1, 236, 48, 1, 176, 49, 1,
|
|
177, 49, 1, 190, 49, 1, 196, 49, 1, 214, 49, 1, 234, 49, 1, 165, 50, 1,
|
|
180, 50, 1, 193, 50, 1, 201, 50, 1, 215, 50, 1, 222, 50, 1, 232, 50, 1,
|
|
178, 51, 1, 194, 51, 1, 186, 52, 1, 231, 52, 1, 197, 53, 1, 208, 53, 1,
|
|
173, 54, 1, 182, 54, 1, 168, 55, 1, 227, 55, 1, 10, 57, 1, 170, 57, 1, 228,
|
|
57, 1, 225, 58, 1, 230, 58, 1, 237, 58, 1, 239, 58, 1, 246, 58, 1, 254, 58,
|
|
1, 216, 59, 1, 229, 59, 1, 212, 61, 1, 253, 61, 1, 210, 62, 1, 213, 62, 1,
|
|
217, 62, 1, 218, 62, 1, 219, 63, 1, 220, 63, 1, 223, 63, 1, 224, 63, 1,
|
|
238, 63, 1, 169, 64, 1, 174, 65, 1, 209, 66, 1, 211, 66, 1, 247, 66, 1,
|
|
252, 66, 1, 241, 67, 1, 221, 68, 1, 245, 68, 1, 244, 70, 1, 248, 71, 1,
|
|
167, 72, 1, 250, 72, 1, 240, 73, 1, 249, 73, 1, 32, 74, 1, 251, 74, 1, 105,
|
|
90, 1, 111, 90, 1, 45, 92, 1, 49, 92, 1, 114, 93, 1, 97, 94, 1, 116, 94, 1,
|
|
51, 95, 1, 101, 95, 1, 110, 95, 1, 40, 96, 1, 41, 96, 1, 48, 97, 1, 56, 97,
|
|
1, 103, 97, 1, 52, 98, 1, 50, 99, 1, 108, 99, 1, 115, 99, 1, 37, 100, 1,
|
|
67, 100, 1, 80, 100, 1, 57, 101, 1, 109, 101, 1, 69, 102, 1, 99, 102, 1,
|
|
55, 103, 1, 43, 104, 1, 100, 104, 1, 58, 105, 1, 112, 105, 1, 44, 106, 1,
|
|
46, 106, 1, 53, 106, 1, 77, 106, 1, 47, 107, 1, 54, 107, 1, 68, 108, 1,
|
|
104, 108, 1, 117, 108, 1, 83, 109, 1, 73, 110, 1, 61, 111, 1, 76, 111, 1,
|
|
78, 111, 1, 79, 111, 1, 42, 112, 1, 65, 112, 1, 84, 112, 1, 71, 113, 1,
|
|
102, 113, 1, 119, 113, 1, 66, 114, 1, 82, 114, 1, 122, 117, 1, 35, 119, 1,
|
|
63, 119, 1, 89, 119, 1, 72, 121, 1, 92, 121, 1, 74, 124, 1, 85, 124, 1, 88,
|
|
124, 1, 106, 124, 1, 107, 124, 1, 121, 124, 1, 34, 128, 1, 90, 128, 1, 91,
|
|
128, 1, 93, 128, 1, 98, 128, 1, 118, 128, 1, 0, 135, 1, 1, 135, 1, 2, 135,
|
|
1, 3, 135, 1, 4, 135, 1, 5, 135, 1, 6, 135, 1, 7, 135, 1, 8, 135, 1, 9,
|
|
135, 1, 11, 135, 1, 12, 135, 1, 13, 135, 1, 14, 135, 1, 15, 135, 1, 16,
|
|
135, 1, 17, 135, 1, 18, 135, 1, 19, 135, 1, 20, 135, 1, 21, 135, 1, 22,
|
|
135, 1, 23, 135, 1, 24, 135, 1, 25, 135, 1, 26, 135, 1, 27, 135, 1, 28,
|
|
135, 1, 29, 135, 1, 30, 135, 1, 31, 135, 1, 33, 135, 1, 36, 135, 1, 38,
|
|
135, 1, 39, 135, 1, 59, 135, 1, 60, 135, 1, 62, 135, 1, 64, 135, 1, 70,
|
|
135, 1, 75, 135, 1, 81, 135, 1, 86, 135, 1, 87, 135, 1, 94, 135, 1, 95,
|
|
135, 1, 96, 135, 1, 113, 135, 1, 120, 135, 1, 123, 135, 1, 124, 135, 1,
|
|
125, 135, 1, 126, 135, 1, 127, 135, 1, 128, 135, 1, 129, 135, 1, 130, 135,
|
|
1, 131, 135, 1, 132, 135, 1, 133, 135, 1, 134, 135, 1, 135, 135, 1, 136,
|
|
135, 1, 137, 135, 1, 138, 135, 1, 139, 135, 1, 140, 135, 1, 141, 135, 1,
|
|
142, 135, 1, 143, 135, 1, 144, 135, 1, 145, 135, 1, 146, 135, 1, 147, 135,
|
|
1, 148, 135, 1, 149, 135, 1, 150, 135, 1, 151, 135, 1, 152, 135, 1, 153,
|
|
135, 1, 154, 135, 1, 155, 135, 1, 156, 135, 1, 157, 135, 1, 158, 135, 1,
|
|
159, 135, 1, 160, 135, 1, 255, 135, 2, 130, 11, 2, 129, 28, 2, 162, 40, 2,
|
|
204, 40, 2, 142, 41, 2, 169, 42, 2, 105, 43, 2, 106, 43, 2, 196, 43, 2,
|
|
198, 43, 2, 200, 43, 2, 233, 43, 2, 140, 44, 2, 144, 44, 2, 189, 44, 2, 66,
|
|
45, 2, 150, 45, 2, 164, 45, 2, 170, 45, 2, 181, 45, 2, 201, 45, 2, 205, 45,
|
|
2, 65, 46, 2, 149, 46, 2, 137, 47, 2, 143, 47, 2, 147, 47, 2, 193, 47, 2,
|
|
197, 47, 2, 224, 47, 2, 231, 47, 2, 240, 47, 2, 241, 47, 2, 145, 48, 2,
|
|
146, 48, 2, 151, 48, 2, 138, 49, 2, 139, 49, 2, 141, 49, 2, 173, 49, 2,
|
|
190, 49, 2, 234, 49, 2, 148, 50, 2, 160, 50, 2, 183, 50, 2, 118, 51, 2,
|
|
131, 51, 2, 136, 51, 2, 220, 51, 2, 232, 51, 2, 117, 53, 2, 177, 53, 2,
|
|
229, 53, 2, 230, 53, 2, 108, 54, 2, 179, 54, 2, 187, 54, 2, 171, 55, 2,
|
|
166, 56, 2, 225, 56, 2, 10, 57, 2, 182, 57, 2, 175, 58, 2, 191, 58, 2, 194,
|
|
58, 2, 78, 59, 2, 168, 59, 2, 199, 59, 2, 226, 59, 2, 93, 60, 2, 185, 60,
|
|
2, 206, 60, 2, 235, 60, 2, 237, 60, 2, 111, 61, 2, 212, 61, 2, 223, 61, 2,
|
|
227, 61, 2, 92, 62, 2, 202, 62, 2, 203, 62, 2, 214, 62, 2, 228, 62, 2, 152,
|
|
63, 2, 158, 63, 2, 67, 64, 2, 79, 64, 2, 184, 64, 2, 64, 65, 2, 178, 65, 2,
|
|
186, 65, 2, 99, 66, 2, 115, 66, 2, 192, 66, 2, 221, 66, 2, 83, 67, 2, 113,
|
|
67, 2, 161, 67, 2, 172, 67, 2, 188, 67, 2, 222, 67, 2, 251, 67, 2, 252, 67,
|
|
2, 109, 68, 2, 110, 68, 2, 121, 68, 2, 157, 68, 2, 174, 68, 2, 211, 68, 2,
|
|
215, 68, 2, 217, 68, 2, 88, 69, 2, 116, 69, 2, 134, 69, 2, 135, 69, 2, 176,
|
|
69, 2, 180, 69, 2, 209, 69, 2, 82, 70, 2, 86, 70, 2, 95, 70, 2, 218, 70, 2,
|
|
250, 70, 2, 72, 71, 2, 76, 71, 2, 123, 71, 2, 167, 71, 2, 208, 71, 2, 243,
|
|
71, 2, 91, 72, 2, 119, 72, 2, 207, 72, 2, 210, 72, 2, 216, 72, 2, 94, 73,
|
|
2, 103, 73, 2, 112, 73, 2, 120, 73, 2, 133, 73, 2, 159, 73, 2, 32, 74, 2,
|
|
69, 74, 2, 73, 74, 2, 122, 74, 2, 156, 74, 2, 195, 74, 2, 236, 74, 2, 239,
|
|
74, 2, 68, 75, 2, 90, 75, 2, 98, 75, 2, 101, 75, 2, 132, 75, 2, 154, 75, 2,
|
|
219, 75, 2, 75, 76, 2, 96, 76, 2, 153, 76, 2, 242, 76, 2, 100, 77, 2, 104,
|
|
77, 2, 124, 77, 2, 126, 77, 2, 128, 77, 2, 246, 77, 2, 71, 78, 2, 81, 78,
|
|
2, 102, 78, 2, 244, 78, 2, 70, 79, 2, 74, 79, 2, 77, 79, 2, 97, 79, 2, 107,
|
|
79, 2, 155, 79, 2, 165, 79, 2, 84, 80, 2, 114, 80, 2, 125, 80, 2, 163, 80,
|
|
2, 213, 80, 2, 248, 80, 2, 80, 81, 2, 85, 81, 2, 89, 81, 2, 249, 81, 2, 87,
|
|
82, 2, 245, 82, 2, 238, 83, 2, 247, 83, 2, 45, 92, 2, 49, 92, 2, 51, 95, 2,
|
|
40, 96, 2, 41, 96, 2, 48, 97, 2, 56, 97, 2, 52, 98, 2, 50, 99, 2, 37, 100,
|
|
2, 57, 101, 2, 55, 103, 2, 43, 104, 2, 58, 105, 2, 44, 106, 2, 46, 106, 2,
|
|
53, 106, 2, 47, 107, 2, 54, 107, 2, 61, 111, 2, 42, 112, 2, 35, 119, 2, 63,
|
|
119, 2, 34, 128, 2, 0, 135, 2, 1, 135, 2, 2, 135, 2, 3, 135, 2, 4, 135, 2,
|
|
5, 135, 2, 6, 135, 2, 7, 135, 2, 8, 135, 2, 9, 135, 2, 11, 135, 2, 12, 135,
|
|
2, 13, 135, 2, 14, 135, 2, 15, 135, 2, 16, 135, 2, 17, 135, 2, 18, 135, 2,
|
|
19, 135, 2, 20, 135, 2, 21, 135, 2, 22, 135, 2, 23, 135, 2, 24, 135, 2, 25,
|
|
135, 2, 26, 135, 2, 27, 135, 2, 28, 135, 2, 29, 135, 2, 30, 135, 2, 31,
|
|
135, 2, 33, 135, 2, 36, 135, 2, 38, 135, 2, 39, 135, 2, 59, 135, 2, 60,
|
|
135, 2, 62, 135, 2, 127, 135, 2, 253, 135, 2, 254, 135, 2, 255, 135, 3,
|
|
227, 14, 3, 129, 17, 3, 130, 27, 3, 128, 36, 3, 229, 36, 3, 139, 38, 3,
|
|
188, 39, 3, 137, 40, 3, 230, 40, 3, 239, 40, 3, 136, 41, 3, 132, 42, 3,
|
|
140, 42, 3, 174, 42, 3, 228, 42, 3, 166, 44, 3, 231, 44, 3, 232, 44, 3,
|
|
147, 45, 3, 168, 45, 3, 170, 45, 3, 186, 45, 3, 151, 46, 3, 159, 46, 3,
|
|
171, 46, 3, 134, 47, 3, 141, 47, 3, 175, 47, 3, 233, 47, 3, 143, 48, 3,
|
|
163, 48, 3, 167, 48, 3, 184, 48, 3, 138, 49, 3, 146, 49, 3, 190, 49, 3,
|
|
153, 50, 3, 131, 51, 3, 149, 51, 3, 157, 51, 3, 160, 51, 3, 145, 52, 3,
|
|
155, 52, 3, 144, 53, 3, 161, 53, 3, 173, 53, 3, 176, 53, 3, 187, 53, 3,
|
|
135, 54, 3, 164, 54, 3, 165, 54, 3, 169, 54, 3, 133, 55, 3, 148, 56, 3,
|
|
150, 56, 3, 156, 57, 3, 179, 57, 3, 189, 57, 3, 191, 57, 3, 152, 58, 3,
|
|
154, 58, 3, 185, 59, 3, 10, 61, 3, 172, 61, 3, 177, 61, 3, 180, 61, 3, 182,
|
|
62, 3, 183, 62, 3, 162, 63, 3, 178, 63, 3, 181, 63, 3, 142, 64, 3, 158, 65,
|
|
3, 226, 68, 3, 32, 78, 3, 111, 94, 3, 105, 95, 3, 45, 96, 3, 49, 96, 3,
|
|
114, 97, 3, 97, 98, 3, 116, 98, 3, 51, 99, 3, 101, 99, 3, 110, 99, 3, 40,
|
|
100, 3, 41, 100, 3, 48, 101, 3, 56, 101, 3, 103, 101, 3, 52, 102, 3, 50,
|
|
103, 3, 108, 103, 3, 115, 103, 3, 37, 104, 3, 67, 104, 3, 80, 104, 3, 57,
|
|
105, 3, 109, 105, 3, 55, 107, 3, 69, 107, 3, 99, 107, 3, 43, 108, 3, 100,
|
|
108, 3, 58, 109, 3, 112, 109, 3, 44, 110, 3, 46, 110, 3, 53, 110, 3, 77,
|
|
110, 3, 47, 111, 3, 54, 111, 3, 68, 112, 3, 104, 112, 3, 117, 112, 3, 83,
|
|
113, 3, 73, 114, 3, 61, 115, 3, 76, 115, 3, 78, 115, 3, 79, 115, 3, 42,
|
|
116, 3, 65, 116, 3, 84, 116, 3, 71, 117, 3, 102, 117, 3, 119, 117, 3, 66,
|
|
118, 3, 82, 118, 3, 206, 118, 3, 122, 121, 3, 35, 123, 3, 89, 123, 3, 72,
|
|
125, 3, 92, 125, 3, 74, 128, 3, 85, 128, 3, 88, 128, 3, 106, 128, 3, 107,
|
|
128, 3, 121, 128, 3, 34, 132, 3, 90, 132, 3, 91, 132, 3, 93, 132, 3, 98,
|
|
132, 3, 118, 132, 3, 195, 132, 3, 0, 139, 3, 1, 139, 3, 2, 139, 3, 3, 139,
|
|
3, 4, 139, 3, 5, 139, 3, 6, 139, 3, 7, 139, 3, 8, 139, 3, 9, 139, 3, 11,
|
|
139, 3, 12, 139, 3, 13, 139, 3, 14, 139, 3, 15, 139, 3, 16, 139, 3, 17,
|
|
139, 3, 18, 139, 3, 19, 139, 3, 20, 139, 3, 21, 139, 3, 22, 139, 3, 23,
|
|
139, 3, 24, 139, 3, 25, 139, 3, 26, 139, 3, 27, 139, 3, 28, 139, 3, 29,
|
|
139, 3, 30, 139, 3, 31, 139, 3, 33, 139, 3, 36, 139, 3, 38, 139, 3, 39,
|
|
139, 3, 59, 139, 3, 60, 139, 3, 62, 139, 3, 63, 139, 3, 64, 139, 3, 70,
|
|
139, 3, 75, 139, 3, 81, 139, 3, 86, 139, 3, 87, 139, 3, 94, 139, 3, 95,
|
|
139, 3, 96, 139, 3, 113, 139, 3, 120, 139, 3, 123, 139, 3, 124, 139, 3,
|
|
125, 139, 3, 126, 139, 3, 127, 139, 3, 192, 139, 3, 193, 139, 3, 194, 139,
|
|
3, 196, 139, 3, 197, 139, 3, 198, 139, 3, 199, 139, 3, 200, 139, 3, 201,
|
|
139, 3, 202, 139, 3, 203, 139, 3, 204, 139, 3, 205, 139, 3, 207, 139, 3,
|
|
208, 139, 3, 209, 139, 3, 210, 139, 3, 211, 139, 3, 212, 139, 3, 213, 139,
|
|
3, 214, 139, 3, 215, 139, 3, 216, 139, 3, 217, 139, 3, 218, 139, 3, 219,
|
|
139, 3, 220, 139, 3, 221, 139, 3, 222, 139, 3, 223, 139, 3, 224, 139, 3,
|
|
225, 139, 3, 234, 139, 3, 235, 139, 3, 236, 139, 3, 237, 139, 3, 238, 139,
|
|
3, 240, 139, 3, 241, 139, 3, 242, 139, 3, 243, 139, 3, 244, 139, 3, 245,
|
|
139, 3, 246, 139, 3, 247, 139, 3, 248, 139, 3, 249, 139, 3, 250, 139, 3,
|
|
251, 139, 3, 252, 139, 3, 253, 139, 3, 254, 139, 3, 255, 139, 4, 0, 1000,
|
|
4, 1, 1000, 4, 2, 1000, 4, 3, 1000, 4, 4, 1000, 4, 5, 1000, 4, 6, 1000, 4,
|
|
7, 1000, 4, 8, 1000, 4, 9, 1000, 4, 10, 1000, 4, 11, 1000, 4, 12, 1000, 4,
|
|
13, 1000, 4, 14, 1000, 4, 15, 1000, 4, 16, 1000, 4, 17, 1000, 4, 18, 1000,
|
|
4, 19, 1000, 4, 20, 1000, 4, 21, 1000, 4, 22, 1000, 4, 23, 1000, 4, 24,
|
|
1000, 4, 25, 1000, 4, 26, 1000, 4, 27, 1000, 4, 28, 1000, 4, 29, 1000, 4,
|
|
30, 1000, 4, 31, 1000, 4, 32, 1000, 4, 33, 1000, 4, 34, 1000, 4, 35, 1000,
|
|
4, 36, 1000, 4, 37, 1000, 4, 38, 1000, 4, 39, 1000, 4, 40, 1000, 4, 41,
|
|
1000, 4, 42, 1000, 4, 43, 1000, 4, 44, 1000, 4, 45, 1000, 4, 46, 1000, 4,
|
|
47, 1000, 4, 48, 1000, 4, 49, 1000, 4, 50, 1000, 4, 51, 1000, 4, 52, 1000,
|
|
4, 53, 1000, 4, 54, 1000, 4, 55, 1000, 4, 56, 1000, 4, 57, 1000, 4, 58,
|
|
1000, 4, 59, 1000, 4, 60, 1000, 4, 61, 1000, 4, 62, 1000, 4, 63, 1000, 4,
|
|
64, 1000, 4, 65, 1000, 4, 66, 1000, 4, 67, 1000, 4, 68, 1000, 4, 69, 1000,
|
|
4, 70, 1000, 4, 71, 1000, 4, 72, 1000, 4, 73, 1000, 4, 74, 1000, 4, 75,
|
|
1000, 4, 76, 1000, 4, 77, 1000, 4, 78, 1000, 4, 79, 1000, 4, 80, 1000, 4,
|
|
81, 1000, 4, 82, 1000, 4, 83, 1000, 4, 84, 1000, 4, 85, 1000, 4, 86, 1000,
|
|
4, 87, 1000, 4, 88, 1000, 4, 89, 1000, 4, 90, 1000, 4, 91, 1000, 4, 92,
|
|
1000, 4, 93, 1000, 4, 94, 1000, 4, 95, 1000, 4, 96, 1000, 4, 97, 1000, 4,
|
|
98, 1000, 4, 99, 1000, 4, 100, 1000, 4, 101, 1000, 4, 102, 1000, 4, 103,
|
|
1000, 4, 104, 1000, 4, 105, 1000, 4, 106, 1000, 4, 107, 1000, 4, 108, 1000,
|
|
4, 109, 1000, 4, 110, 1000, 4, 111, 1000, 4, 112, 1000, 4, 113, 1000, 4,
|
|
114, 1000, 4, 115, 1000, 4, 116, 1000, 4, 117, 1000, 4, 118, 1000, 4, 119,
|
|
1000, 4, 120, 1000, 4, 121, 1000, 4, 122, 1000, 4, 123, 1000, 4, 124, 1000,
|
|
4, 125, 1000, 4, 126, 1000, 4, 127, 1000, 4, 128, 1000, 4, 129, 1000, 4,
|
|
130, 1000, 4, 131, 1000, 4, 132, 1000, 4, 133, 1000, 4, 134, 1000, 4, 135,
|
|
1000, 4, 136, 1000, 4, 137, 1000, 4, 138, 1000, 4, 139, 1000, 4, 140, 1000,
|
|
4, 141, 1000, 4, 142, 1000, 4, 143, 1000, 4, 144, 1000, 4, 145, 1000, 4,
|
|
146, 1000, 4, 147, 1000, 4, 148, 1000, 4, 149, 1000, 4, 150, 1000, 4, 151,
|
|
1000, 4, 152, 1000, 4, 153, 1000, 4, 154, 1000, 4, 155, 1000, 4, 156, 1000,
|
|
4, 157, 1000, 4, 158, 1000, 4, 159, 1000, 4, 160, 1000, 4, 161, 1000, 4,
|
|
162, 1000, 4, 163, 1000, 4, 164, 1000, 4, 165, 1000, 4, 166, 1000, 4, 167,
|
|
1000, 4, 168, 1000, 4, 169, 1000, 4, 170, 1000, 4, 171, 1000, 4, 172, 1000,
|
|
4, 173, 1000, 4, 174, 1000, 4, 175, 1000, 4, 176, 1000, 4, 177, 1000, 4,
|
|
178, 1000, 4, 179, 1000, 4, 180, 1000, 4, 181, 1000, 4, 182, 1000, 4, 183,
|
|
1000, 4, 184, 1000, 4, 185, 1000, 4, 186, 1000, 4, 187, 1000, 4, 188, 1000,
|
|
4, 189, 1000, 4, 190, 1000, 4, 191, 1000, 4, 192, 1000, 4, 193, 1000, 4,
|
|
194, 1000, 4, 195, 1000, 4, 196, 1000, 4, 197, 1000, 4, 198, 1000, 4, 199,
|
|
1000, 4, 200, 1000, 4, 201, 1000, 4, 202, 1000, 4, 203, 1000, 4, 204, 1000,
|
|
4, 205, 1000, 4, 206, 1000, 4, 207, 1000, 4, 208, 1000, 4, 209, 1000, 4,
|
|
210, 1000, 4, 211, 1000, 4, 212, 1000, 4, 213, 1000, 4, 214, 1000, 4, 215,
|
|
1000, 4, 216, 1000, 4, 217, 1000, 4, 218, 1000, 4, 219, 1000, 4, 220, 1000,
|
|
4, 221, 1000, 4, 222, 1000, 4, 223, 1000, 4, 224, 1000, 4, 225, 1000, 4,
|
|
226, 1000, 4, 227, 1000, 4, 228, 1000, 4, 229, 1000, 4, 230, 1000, 4, 231,
|
|
1000, 4, 232, 1000, 4, 233, 1000, 4, 234, 1000, 4, 235, 1000, 4, 236, 1000,
|
|
4, 237, 1000, 4, 238, 1000, 4, 239, 1000, 4, 240, 1000, 4, 241, 1000, 4,
|
|
242, 1000, 4, 243, 1000, 4, 244, 1000, 4, 245, 1000, 4, 246, 1000, 4, 247,
|
|
1000, 4, 248, 1000, 4, 249, 1000, 4, 250, 1000, 4, 251, 1000, 4, 252, 1000,
|
|
4, 253, 1000, 4, 254, 1000, 4, 255, 1000]));
|
|
|
|
predicate link_vars(var int: encoding_i, var int: byte_status_i,
|
|
var int: char_start_i) =
|
|
table_int([encoding_i, byte_status_i, char_start_i], array2d(1..16,
|
|
index_set([encoding_i, byte_status_i, char_start_i]), [0, 0, 1, 1, 1, 1, 1,
|
|
2, 0, 2, 3, 1, 2, 4, 1, 2, 5, 0, 3, 6, 1, 3, 7, 0, 3, 8, 1, 3, 9, 0, 3, 10,
|
|
0, 3, 11, 1, 3, 12, 0, 3, 13, 0, 3, 14, 0, 4, 15, 1]));
|
|
|
|
predicate link_statuses(var int: byte_status_i, var int: byte_status_im1) =
|
|
table_int([byte_status_i, byte_status_im1], array2d(1..72,
|
|
index_set([byte_status_i, byte_status_im1]), [0, 0, 1, 0, 3, 0, 4, 0, 6, 0,
|
|
8, 0, 11, 0, 15, 0, 2, 1, 0, 2, 1, 2, 3, 2, 4, 2, 6, 2, 8, 2, 11, 2, 15, 2,
|
|
0, 3, 1, 3, 3, 3, 4, 3, 6, 3, 8, 3, 11, 3, 15, 3, 5, 4, 0, 5, 1, 5, 3, 5,
|
|
4, 5, 6, 5, 8, 5, 11, 5, 15, 5, 7, 6, 0, 7, 1, 7, 3, 7, 4, 7, 6, 7, 8, 7,
|
|
11, 7, 15, 7, 9, 8, 10, 9, 0, 10, 1, 10, 3, 10, 4, 10, 6, 10, 8, 10, 11,
|
|
10, 15, 10, 12, 11, 13, 12, 14, 13, 0, 14, 1, 14, 3, 14, 4, 14, 6, 14, 8,
|
|
14, 11, 14, 15, 14, 0, 15, 1, 15, 3, 15, 4, 15, 6, 15, 8, 15, 11, 15, 15,
|
|
15]));
|
|
|