516 lines
31 KiB
MiniZinc
516 lines
31 KiB
MiniZinc
predicate fzn_all_different_int(array [int] of var int: x);
|
|
predicate count_eq(array [int] of var int: x, var int: y, var int: c);
|
|
predicate count_reif(array [int] of var int: x, var int: y, var int: c, var bool: b);
|
|
predicate fixed_fzn_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, int: b);
|
|
predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
predicate global_cardinality_closed(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
predicate global_cardinality_low_up(array [int] of var int: x, array [int] of int: cover, array [int] of int: lbound, array [int] of int: ubound);
|
|
predicate global_cardinality_low_up_closed(array [int] of var int: x, array [int] of int: cover, array [int] of int: lbound, array [int] of int: ubound);
|
|
predicate maximum_int(var int: m, array [int] of var int: x);
|
|
predicate minimum_int(var int: m, array [int] of var int: x);
|
|
predicate sliding_sum(int: low, int: up, int: seq, array [int] of var int: vs);
|
|
predicate sort(array [int] of var int: x, array [int] of var int: y);
|
|
predicate table_bool(array [int] of var bool: x, array [int, int] of bool: t);
|
|
predicate table_int(array [int] of var int: x, array [int, int] of int: t);
|
|
predicate var_fzn_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, var int: b);
|
|
var bool: BOOL____00029 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00031 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00033 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00035 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00037 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00039 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00041 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00043 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00045 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00047 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00049 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00051 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00053 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00055 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00057 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00059 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00061 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00063 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00065 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00067 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00069 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00071 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00073 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00075 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00077 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00079 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00081 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00083 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00085 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00087 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00089 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00091 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00093 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00095 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00097 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00099 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00101 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00103 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00105 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00107 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00109 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00111 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00113 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00115 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00117 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00119 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00121 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00123 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00125 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00127 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00129 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00131 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00133 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00135 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00137 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00139 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00141 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00143 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00145 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00147 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00149 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00151 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00153 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00155 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00157 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00159 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00161 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00163 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00165 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00167 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00169 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00171 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00173 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00175 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00177 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00179 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00181 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00183 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00185 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00187 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00189 :: is_defined_var :: var_is_introduced;
|
|
var -54..3: INT____00190 :: is_defined_var :: var_is_introduced;
|
|
array [1..27] of var 0..2: bin_code;
|
|
array [1..81] of var 0..2: binary;
|
|
var -54..54: max_val :: output_var;
|
|
var -54..54: min_max_diff :: output_var = INT____00190;
|
|
var -54..54: min_val :: output_var;
|
|
array [1..3] of var 0..2: t____00001;
|
|
array [1..3] of var 0..2: t____00002;
|
|
array [1..3] of var 0..2: t____00003;
|
|
array [1..3] of var 0..2: t____00004;
|
|
array [1..3] of var 0..2: t____00005;
|
|
array [1..3] of var 0..2: t____00006;
|
|
array [1..3] of var 0..2: t____00007;
|
|
array [1..3] of var 0..2: t____00008;
|
|
array [1..3] of var 0..2: t____00009;
|
|
array [1..3] of var 0..2: t____00010;
|
|
array [1..3] of var 0..2: t____00011;
|
|
array [1..3] of var 0..2: t____00012;
|
|
array [1..3] of var 0..2: t____00013;
|
|
array [1..3] of var 0..2: t____00014;
|
|
array [1..3] of var 0..2: t____00015;
|
|
array [1..3] of var 0..2: t____00016;
|
|
array [1..3] of var 0..2: t____00017;
|
|
array [1..3] of var 0..2: t____00018;
|
|
array [1..3] of var 0..2: t____00019;
|
|
array [1..3] of var 0..2: t____00020;
|
|
array [1..3] of var 0..2: t____00021;
|
|
array [1..3] of var 0..2: t____00022;
|
|
array [1..3] of var 0..2: t____00023;
|
|
array [1..3] of var 0..2: t____00024;
|
|
array [1..3] of var 0..2: t____00025;
|
|
array [1..3] of var 0..2: t____00026;
|
|
array [1..3] of var 0..2: t____00027;
|
|
array [1..27] of var -1..1: winter :: output_array([1..27]);
|
|
array [1..27] of var int: winter_sum :: output_array([1..27]);
|
|
array [1..27] of var 0..26: x;
|
|
constraint fzn_all_different_int(x);
|
|
constraint int_eq(bin_code[1], binary[1]);
|
|
constraint int_eq(bin_code[2], binary[4]);
|
|
constraint int_eq(bin_code[3], binary[7]);
|
|
constraint int_eq(bin_code[4], binary[10]);
|
|
constraint int_eq(bin_code[5], binary[13]);
|
|
constraint int_eq(bin_code[6], binary[16]);
|
|
constraint int_eq(bin_code[7], binary[19]);
|
|
constraint int_eq(bin_code[8], binary[22]);
|
|
constraint int_eq(bin_code[9], binary[25]);
|
|
constraint int_eq(bin_code[10], binary[28]);
|
|
constraint int_eq(bin_code[11], binary[31]);
|
|
constraint int_eq(bin_code[12], binary[34]);
|
|
constraint int_eq(bin_code[13], binary[37]);
|
|
constraint int_eq(bin_code[14], binary[40]);
|
|
constraint int_eq(bin_code[15], binary[43]);
|
|
constraint int_eq(bin_code[16], binary[46]);
|
|
constraint int_eq(bin_code[17], binary[49]);
|
|
constraint int_eq(bin_code[18], binary[52]);
|
|
constraint int_eq(bin_code[19], binary[55]);
|
|
constraint int_eq(bin_code[20], binary[58]);
|
|
constraint int_eq(bin_code[21], binary[61]);
|
|
constraint int_eq(bin_code[22], binary[64]);
|
|
constraint int_eq(bin_code[23], binary[67]);
|
|
constraint int_eq(bin_code[24], binary[70]);
|
|
constraint int_eq(bin_code[25], binary[73]);
|
|
constraint int_eq(bin_code[26], binary[76]);
|
|
constraint int_eq(bin_code[27], binary[79]);
|
|
constraint int_eq(binary[1], t____00001[1]);
|
|
constraint int_eq(binary[2], binary[4]);
|
|
constraint int_eq(binary[2], t____00001[2]);
|
|
constraint int_eq(binary[3], binary[5]);
|
|
constraint int_eq(binary[3], t____00001[3]);
|
|
constraint int_eq(binary[4], t____00002[1]);
|
|
constraint int_eq(binary[5], binary[7]);
|
|
constraint int_eq(binary[5], t____00002[2]);
|
|
constraint int_eq(binary[6], binary[8]);
|
|
constraint int_eq(binary[6], t____00002[3]);
|
|
constraint int_eq(binary[7], t____00003[1]);
|
|
constraint int_eq(binary[8], binary[10]);
|
|
constraint int_eq(binary[8], t____00003[2]);
|
|
constraint int_eq(binary[9], binary[11]);
|
|
constraint int_eq(binary[9], t____00003[3]);
|
|
constraint int_eq(binary[10], t____00004[1]);
|
|
constraint int_eq(binary[11], binary[13]);
|
|
constraint int_eq(binary[11], t____00004[2]);
|
|
constraint int_eq(binary[12], binary[14]);
|
|
constraint int_eq(binary[12], t____00004[3]);
|
|
constraint int_eq(binary[13], t____00005[1]);
|
|
constraint int_eq(binary[14], binary[16]);
|
|
constraint int_eq(binary[14], t____00005[2]);
|
|
constraint int_eq(binary[15], binary[17]);
|
|
constraint int_eq(binary[15], t____00005[3]);
|
|
constraint int_eq(binary[16], t____00006[1]);
|
|
constraint int_eq(binary[17], binary[19]);
|
|
constraint int_eq(binary[17], t____00006[2]);
|
|
constraint int_eq(binary[18], binary[20]);
|
|
constraint int_eq(binary[18], t____00006[3]);
|
|
constraint int_eq(binary[19], t____00007[1]);
|
|
constraint int_eq(binary[20], binary[22]);
|
|
constraint int_eq(binary[20], t____00007[2]);
|
|
constraint int_eq(binary[21], binary[23]);
|
|
constraint int_eq(binary[21], t____00007[3]);
|
|
constraint int_eq(binary[22], t____00008[1]);
|
|
constraint int_eq(binary[23], binary[25]);
|
|
constraint int_eq(binary[23], t____00008[2]);
|
|
constraint int_eq(binary[24], binary[26]);
|
|
constraint int_eq(binary[24], t____00008[3]);
|
|
constraint int_eq(binary[25], t____00009[1]);
|
|
constraint int_eq(binary[26], binary[28]);
|
|
constraint int_eq(binary[26], t____00009[2]);
|
|
constraint int_eq(binary[27], binary[29]);
|
|
constraint int_eq(binary[27], t____00009[3]);
|
|
constraint int_eq(binary[28], t____00010[1]);
|
|
constraint int_eq(binary[29], binary[31]);
|
|
constraint int_eq(binary[29], t____00010[2]);
|
|
constraint int_eq(binary[30], binary[32]);
|
|
constraint int_eq(binary[30], t____00010[3]);
|
|
constraint int_eq(binary[31], t____00011[1]);
|
|
constraint int_eq(binary[32], binary[34]);
|
|
constraint int_eq(binary[32], t____00011[2]);
|
|
constraint int_eq(binary[33], binary[35]);
|
|
constraint int_eq(binary[33], t____00011[3]);
|
|
constraint int_eq(binary[34], t____00012[1]);
|
|
constraint int_eq(binary[35], binary[37]);
|
|
constraint int_eq(binary[35], t____00012[2]);
|
|
constraint int_eq(binary[36], binary[38]);
|
|
constraint int_eq(binary[36], t____00012[3]);
|
|
constraint int_eq(binary[37], t____00013[1]);
|
|
constraint int_eq(binary[38], binary[40]);
|
|
constraint int_eq(binary[38], t____00013[2]);
|
|
constraint int_eq(binary[39], binary[41]);
|
|
constraint int_eq(binary[39], t____00013[3]);
|
|
constraint int_eq(binary[40], t____00014[1]);
|
|
constraint int_eq(binary[41], binary[43]);
|
|
constraint int_eq(binary[41], t____00014[2]);
|
|
constraint int_eq(binary[42], binary[44]);
|
|
constraint int_eq(binary[42], t____00014[3]);
|
|
constraint int_eq(binary[43], t____00015[1]);
|
|
constraint int_eq(binary[44], binary[46]);
|
|
constraint int_eq(binary[44], t____00015[2]);
|
|
constraint int_eq(binary[45], binary[47]);
|
|
constraint int_eq(binary[45], t____00015[3]);
|
|
constraint int_eq(binary[46], t____00016[1]);
|
|
constraint int_eq(binary[47], binary[49]);
|
|
constraint int_eq(binary[47], t____00016[2]);
|
|
constraint int_eq(binary[48], binary[50]);
|
|
constraint int_eq(binary[48], t____00016[3]);
|
|
constraint int_eq(binary[49], t____00017[1]);
|
|
constraint int_eq(binary[50], binary[52]);
|
|
constraint int_eq(binary[50], t____00017[2]);
|
|
constraint int_eq(binary[51], binary[53]);
|
|
constraint int_eq(binary[51], t____00017[3]);
|
|
constraint int_eq(binary[52], t____00018[1]);
|
|
constraint int_eq(binary[53], binary[55]);
|
|
constraint int_eq(binary[53], t____00018[2]);
|
|
constraint int_eq(binary[54], binary[56]);
|
|
constraint int_eq(binary[54], t____00018[3]);
|
|
constraint int_eq(binary[55], t____00019[1]);
|
|
constraint int_eq(binary[56], binary[58]);
|
|
constraint int_eq(binary[56], t____00019[2]);
|
|
constraint int_eq(binary[57], binary[59]);
|
|
constraint int_eq(binary[57], t____00019[3]);
|
|
constraint int_eq(binary[58], t____00020[1]);
|
|
constraint int_eq(binary[59], binary[61]);
|
|
constraint int_eq(binary[59], t____00020[2]);
|
|
constraint int_eq(binary[60], binary[62]);
|
|
constraint int_eq(binary[60], t____00020[3]);
|
|
constraint int_eq(binary[61], t____00021[1]);
|
|
constraint int_eq(binary[62], binary[64]);
|
|
constraint int_eq(binary[62], t____00021[2]);
|
|
constraint int_eq(binary[63], binary[65]);
|
|
constraint int_eq(binary[63], t____00021[3]);
|
|
constraint int_eq(binary[64], t____00022[1]);
|
|
constraint int_eq(binary[65], binary[67]);
|
|
constraint int_eq(binary[65], t____00022[2]);
|
|
constraint int_eq(binary[66], binary[68]);
|
|
constraint int_eq(binary[66], t____00022[3]);
|
|
constraint int_eq(binary[67], t____00023[1]);
|
|
constraint int_eq(binary[68], binary[70]);
|
|
constraint int_eq(binary[68], t____00023[2]);
|
|
constraint int_eq(binary[69], binary[71]);
|
|
constraint int_eq(binary[69], t____00023[3]);
|
|
constraint int_eq(binary[70], t____00024[1]);
|
|
constraint int_eq(binary[71], binary[73]);
|
|
constraint int_eq(binary[71], t____00024[2]);
|
|
constraint int_eq(binary[72], binary[74]);
|
|
constraint int_eq(binary[72], t____00024[3]);
|
|
constraint int_eq(binary[73], t____00025[1]);
|
|
constraint int_eq(binary[74], binary[76]);
|
|
constraint int_eq(binary[74], t____00025[2]);
|
|
constraint int_eq(binary[75], binary[77]);
|
|
constraint int_eq(binary[75], t____00025[3]);
|
|
constraint int_eq(binary[76], t____00026[1]);
|
|
constraint int_eq(binary[77], binary[79]);
|
|
constraint int_eq(binary[77], t____00026[2]);
|
|
constraint int_eq(binary[78], binary[80]);
|
|
constraint int_eq(binary[78], t____00026[3]);
|
|
constraint int_eq(binary[79], t____00027[1]);
|
|
constraint int_eq(binary[80], binary[1]);
|
|
constraint int_eq(binary[80], t____00027[2]);
|
|
constraint int_eq(binary[81], binary[2]);
|
|
constraint int_eq(binary[81], t____00027[3]);
|
|
constraint int_eq(winter_sum[1], winter[1]);
|
|
constraint int_eq_reif(bin_code[1], 0, BOOL____00029);
|
|
constraint int_eq_reif(bin_code[1], 1, BOOL____00031);
|
|
constraint int_eq_reif(bin_code[1], 2, BOOL____00033);
|
|
constraint int_eq_reif(bin_code[2], 0, BOOL____00035);
|
|
constraint int_eq_reif(bin_code[2], 1, BOOL____00037);
|
|
constraint int_eq_reif(bin_code[2], 2, BOOL____00039);
|
|
constraint int_eq_reif(bin_code[3], 0, BOOL____00041);
|
|
constraint int_eq_reif(bin_code[3], 1, BOOL____00043);
|
|
constraint int_eq_reif(bin_code[3], 2, BOOL____00045);
|
|
constraint int_eq_reif(bin_code[4], 0, BOOL____00047);
|
|
constraint int_eq_reif(bin_code[4], 1, BOOL____00049);
|
|
constraint int_eq_reif(bin_code[4], 2, BOOL____00051);
|
|
constraint int_eq_reif(bin_code[5], 0, BOOL____00053);
|
|
constraint int_eq_reif(bin_code[5], 1, BOOL____00055);
|
|
constraint int_eq_reif(bin_code[5], 2, BOOL____00057);
|
|
constraint int_eq_reif(bin_code[6], 0, BOOL____00059);
|
|
constraint int_eq_reif(bin_code[6], 1, BOOL____00061);
|
|
constraint int_eq_reif(bin_code[6], 2, BOOL____00063);
|
|
constraint int_eq_reif(bin_code[7], 0, BOOL____00065);
|
|
constraint int_eq_reif(bin_code[7], 1, BOOL____00067);
|
|
constraint int_eq_reif(bin_code[7], 2, BOOL____00069);
|
|
constraint int_eq_reif(bin_code[8], 0, BOOL____00071);
|
|
constraint int_eq_reif(bin_code[8], 1, BOOL____00073);
|
|
constraint int_eq_reif(bin_code[8], 2, BOOL____00075);
|
|
constraint int_eq_reif(bin_code[9], 0, BOOL____00077);
|
|
constraint int_eq_reif(bin_code[9], 1, BOOL____00079);
|
|
constraint int_eq_reif(bin_code[9], 2, BOOL____00081);
|
|
constraint int_eq_reif(bin_code[10], 0, BOOL____00083);
|
|
constraint int_eq_reif(bin_code[10], 1, BOOL____00085);
|
|
constraint int_eq_reif(bin_code[10], 2, BOOL____00087);
|
|
constraint int_eq_reif(bin_code[11], 0, BOOL____00089);
|
|
constraint int_eq_reif(bin_code[11], 1, BOOL____00091);
|
|
constraint int_eq_reif(bin_code[11], 2, BOOL____00093);
|
|
constraint int_eq_reif(bin_code[12], 0, BOOL____00095);
|
|
constraint int_eq_reif(bin_code[12], 1, BOOL____00097);
|
|
constraint int_eq_reif(bin_code[12], 2, BOOL____00099);
|
|
constraint int_eq_reif(bin_code[13], 0, BOOL____00101);
|
|
constraint int_eq_reif(bin_code[13], 1, BOOL____00103);
|
|
constraint int_eq_reif(bin_code[13], 2, BOOL____00105);
|
|
constraint int_eq_reif(bin_code[14], 0, BOOL____00107);
|
|
constraint int_eq_reif(bin_code[14], 1, BOOL____00109);
|
|
constraint int_eq_reif(bin_code[14], 2, BOOL____00111);
|
|
constraint int_eq_reif(bin_code[15], 0, BOOL____00113);
|
|
constraint int_eq_reif(bin_code[15], 1, BOOL____00115);
|
|
constraint int_eq_reif(bin_code[15], 2, BOOL____00117);
|
|
constraint int_eq_reif(bin_code[16], 0, BOOL____00119);
|
|
constraint int_eq_reif(bin_code[16], 1, BOOL____00121);
|
|
constraint int_eq_reif(bin_code[16], 2, BOOL____00123);
|
|
constraint int_eq_reif(bin_code[17], 0, BOOL____00125);
|
|
constraint int_eq_reif(bin_code[17], 1, BOOL____00127);
|
|
constraint int_eq_reif(bin_code[17], 2, BOOL____00129);
|
|
constraint int_eq_reif(bin_code[18], 0, BOOL____00131);
|
|
constraint int_eq_reif(bin_code[18], 1, BOOL____00133);
|
|
constraint int_eq_reif(bin_code[18], 2, BOOL____00135);
|
|
constraint int_eq_reif(bin_code[19], 0, BOOL____00137);
|
|
constraint int_eq_reif(bin_code[19], 1, BOOL____00139);
|
|
constraint int_eq_reif(bin_code[19], 2, BOOL____00141);
|
|
constraint int_eq_reif(bin_code[20], 0, BOOL____00143);
|
|
constraint int_eq_reif(bin_code[20], 1, BOOL____00145);
|
|
constraint int_eq_reif(bin_code[20], 2, BOOL____00147);
|
|
constraint int_eq_reif(bin_code[21], 0, BOOL____00149);
|
|
constraint int_eq_reif(bin_code[21], 1, BOOL____00151);
|
|
constraint int_eq_reif(bin_code[21], 2, BOOL____00153);
|
|
constraint int_eq_reif(bin_code[22], 0, BOOL____00155);
|
|
constraint int_eq_reif(bin_code[22], 1, BOOL____00157);
|
|
constraint int_eq_reif(bin_code[22], 2, BOOL____00159);
|
|
constraint int_eq_reif(bin_code[23], 0, BOOL____00161);
|
|
constraint int_eq_reif(bin_code[23], 1, BOOL____00163);
|
|
constraint int_eq_reif(bin_code[23], 2, BOOL____00165);
|
|
constraint int_eq_reif(bin_code[24], 0, BOOL____00167);
|
|
constraint int_eq_reif(bin_code[24], 1, BOOL____00169);
|
|
constraint int_eq_reif(bin_code[24], 2, BOOL____00171);
|
|
constraint int_eq_reif(bin_code[25], 0, BOOL____00173);
|
|
constraint int_eq_reif(bin_code[25], 1, BOOL____00175);
|
|
constraint int_eq_reif(bin_code[25], 2, BOOL____00177);
|
|
constraint int_eq_reif(bin_code[26], 0, BOOL____00179);
|
|
constraint int_eq_reif(bin_code[26], 1, BOOL____00181);
|
|
constraint int_eq_reif(bin_code[26], 2, BOOL____00183);
|
|
constraint int_eq_reif(bin_code[27], 0, BOOL____00185);
|
|
constraint int_eq_reif(bin_code[27], 1, BOOL____00187);
|
|
constraint int_eq_reif(bin_code[27], 2, BOOL____00189);
|
|
constraint int_eq_reif(winter[1], -1, BOOL____00029) :: defines_var(BOOL____00029);
|
|
constraint int_eq_reif(winter[1], 0, BOOL____00031) :: defines_var(BOOL____00031);
|
|
constraint int_eq_reif(winter[1], 1, BOOL____00033) :: defines_var(BOOL____00033);
|
|
constraint int_eq_reif(winter[2], -1, BOOL____00035) :: defines_var(BOOL____00035);
|
|
constraint int_eq_reif(winter[2], 0, BOOL____00037) :: defines_var(BOOL____00037);
|
|
constraint int_eq_reif(winter[2], 1, BOOL____00039) :: defines_var(BOOL____00039);
|
|
constraint int_eq_reif(winter[3], -1, BOOL____00041) :: defines_var(BOOL____00041);
|
|
constraint int_eq_reif(winter[3], 0, BOOL____00043) :: defines_var(BOOL____00043);
|
|
constraint int_eq_reif(winter[3], 1, BOOL____00045) :: defines_var(BOOL____00045);
|
|
constraint int_eq_reif(winter[4], -1, BOOL____00047) :: defines_var(BOOL____00047);
|
|
constraint int_eq_reif(winter[4], 0, BOOL____00049) :: defines_var(BOOL____00049);
|
|
constraint int_eq_reif(winter[4], 1, BOOL____00051) :: defines_var(BOOL____00051);
|
|
constraint int_eq_reif(winter[5], -1, BOOL____00053) :: defines_var(BOOL____00053);
|
|
constraint int_eq_reif(winter[5], 0, BOOL____00055) :: defines_var(BOOL____00055);
|
|
constraint int_eq_reif(winter[5], 1, BOOL____00057) :: defines_var(BOOL____00057);
|
|
constraint int_eq_reif(winter[6], -1, BOOL____00059) :: defines_var(BOOL____00059);
|
|
constraint int_eq_reif(winter[6], 0, BOOL____00061) :: defines_var(BOOL____00061);
|
|
constraint int_eq_reif(winter[6], 1, BOOL____00063) :: defines_var(BOOL____00063);
|
|
constraint int_eq_reif(winter[7], -1, BOOL____00065) :: defines_var(BOOL____00065);
|
|
constraint int_eq_reif(winter[7], 0, BOOL____00067) :: defines_var(BOOL____00067);
|
|
constraint int_eq_reif(winter[7], 1, BOOL____00069) :: defines_var(BOOL____00069);
|
|
constraint int_eq_reif(winter[8], -1, BOOL____00071) :: defines_var(BOOL____00071);
|
|
constraint int_eq_reif(winter[8], 0, BOOL____00073) :: defines_var(BOOL____00073);
|
|
constraint int_eq_reif(winter[8], 1, BOOL____00075) :: defines_var(BOOL____00075);
|
|
constraint int_eq_reif(winter[9], -1, BOOL____00077) :: defines_var(BOOL____00077);
|
|
constraint int_eq_reif(winter[9], 0, BOOL____00079) :: defines_var(BOOL____00079);
|
|
constraint int_eq_reif(winter[9], 1, BOOL____00081) :: defines_var(BOOL____00081);
|
|
constraint int_eq_reif(winter[10], -1, BOOL____00083) :: defines_var(BOOL____00083);
|
|
constraint int_eq_reif(winter[10], 0, BOOL____00085) :: defines_var(BOOL____00085);
|
|
constraint int_eq_reif(winter[10], 1, BOOL____00087) :: defines_var(BOOL____00087);
|
|
constraint int_eq_reif(winter[11], -1, BOOL____00089) :: defines_var(BOOL____00089);
|
|
constraint int_eq_reif(winter[11], 0, BOOL____00091) :: defines_var(BOOL____00091);
|
|
constraint int_eq_reif(winter[11], 1, BOOL____00093) :: defines_var(BOOL____00093);
|
|
constraint int_eq_reif(winter[12], -1, BOOL____00095) :: defines_var(BOOL____00095);
|
|
constraint int_eq_reif(winter[12], 0, BOOL____00097) :: defines_var(BOOL____00097);
|
|
constraint int_eq_reif(winter[12], 1, BOOL____00099) :: defines_var(BOOL____00099);
|
|
constraint int_eq_reif(winter[13], -1, BOOL____00101) :: defines_var(BOOL____00101);
|
|
constraint int_eq_reif(winter[13], 0, BOOL____00103) :: defines_var(BOOL____00103);
|
|
constraint int_eq_reif(winter[13], 1, BOOL____00105) :: defines_var(BOOL____00105);
|
|
constraint int_eq_reif(winter[14], -1, BOOL____00107) :: defines_var(BOOL____00107);
|
|
constraint int_eq_reif(winter[14], 0, BOOL____00109) :: defines_var(BOOL____00109);
|
|
constraint int_eq_reif(winter[14], 1, BOOL____00111) :: defines_var(BOOL____00111);
|
|
constraint int_eq_reif(winter[15], -1, BOOL____00113) :: defines_var(BOOL____00113);
|
|
constraint int_eq_reif(winter[15], 0, BOOL____00115) :: defines_var(BOOL____00115);
|
|
constraint int_eq_reif(winter[15], 1, BOOL____00117) :: defines_var(BOOL____00117);
|
|
constraint int_eq_reif(winter[16], -1, BOOL____00119) :: defines_var(BOOL____00119);
|
|
constraint int_eq_reif(winter[16], 0, BOOL____00121) :: defines_var(BOOL____00121);
|
|
constraint int_eq_reif(winter[16], 1, BOOL____00123) :: defines_var(BOOL____00123);
|
|
constraint int_eq_reif(winter[17], -1, BOOL____00125) :: defines_var(BOOL____00125);
|
|
constraint int_eq_reif(winter[17], 0, BOOL____00127) :: defines_var(BOOL____00127);
|
|
constraint int_eq_reif(winter[17], 1, BOOL____00129) :: defines_var(BOOL____00129);
|
|
constraint int_eq_reif(winter[18], -1, BOOL____00131) :: defines_var(BOOL____00131);
|
|
constraint int_eq_reif(winter[18], 0, BOOL____00133) :: defines_var(BOOL____00133);
|
|
constraint int_eq_reif(winter[18], 1, BOOL____00135) :: defines_var(BOOL____00135);
|
|
constraint int_eq_reif(winter[19], -1, BOOL____00137) :: defines_var(BOOL____00137);
|
|
constraint int_eq_reif(winter[19], 0, BOOL____00139) :: defines_var(BOOL____00139);
|
|
constraint int_eq_reif(winter[19], 1, BOOL____00141) :: defines_var(BOOL____00141);
|
|
constraint int_eq_reif(winter[20], -1, BOOL____00143) :: defines_var(BOOL____00143);
|
|
constraint int_eq_reif(winter[20], 0, BOOL____00145) :: defines_var(BOOL____00145);
|
|
constraint int_eq_reif(winter[20], 1, BOOL____00147) :: defines_var(BOOL____00147);
|
|
constraint int_eq_reif(winter[21], -1, BOOL____00149) :: defines_var(BOOL____00149);
|
|
constraint int_eq_reif(winter[21], 0, BOOL____00151) :: defines_var(BOOL____00151);
|
|
constraint int_eq_reif(winter[21], 1, BOOL____00153) :: defines_var(BOOL____00153);
|
|
constraint int_eq_reif(winter[22], -1, BOOL____00155) :: defines_var(BOOL____00155);
|
|
constraint int_eq_reif(winter[22], 0, BOOL____00157) :: defines_var(BOOL____00157);
|
|
constraint int_eq_reif(winter[22], 1, BOOL____00159) :: defines_var(BOOL____00159);
|
|
constraint int_eq_reif(winter[23], -1, BOOL____00161) :: defines_var(BOOL____00161);
|
|
constraint int_eq_reif(winter[23], 0, BOOL____00163) :: defines_var(BOOL____00163);
|
|
constraint int_eq_reif(winter[23], 1, BOOL____00165) :: defines_var(BOOL____00165);
|
|
constraint int_eq_reif(winter[24], -1, BOOL____00167) :: defines_var(BOOL____00167);
|
|
constraint int_eq_reif(winter[24], 0, BOOL____00169) :: defines_var(BOOL____00169);
|
|
constraint int_eq_reif(winter[24], 1, BOOL____00171) :: defines_var(BOOL____00171);
|
|
constraint int_eq_reif(winter[25], -1, BOOL____00173) :: defines_var(BOOL____00173);
|
|
constraint int_eq_reif(winter[25], 0, BOOL____00175) :: defines_var(BOOL____00175);
|
|
constraint int_eq_reif(winter[25], 1, BOOL____00177) :: defines_var(BOOL____00177);
|
|
constraint int_eq_reif(winter[26], -1, BOOL____00179) :: defines_var(BOOL____00179);
|
|
constraint int_eq_reif(winter[26], 0, BOOL____00181) :: defines_var(BOOL____00181);
|
|
constraint int_eq_reif(winter[26], 1, BOOL____00183) :: defines_var(BOOL____00183);
|
|
constraint int_eq_reif(winter[27], -1, BOOL____00185) :: defines_var(BOOL____00185);
|
|
constraint int_eq_reif(winter[27], 0, BOOL____00187) :: defines_var(BOOL____00187);
|
|
constraint int_eq_reif(winter[27], 1, BOOL____00189) :: defines_var(BOOL____00189);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[2], winter_sum[1], winter_sum[2]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[3], winter_sum[2], winter_sum[3]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[4], winter_sum[3], winter_sum[4]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[5], winter_sum[4], winter_sum[5]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[6], winter_sum[5], winter_sum[6]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[7], winter_sum[6], winter_sum[7]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[8], winter_sum[7], winter_sum[8]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[9], winter_sum[8], winter_sum[9]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[10], winter_sum[9], winter_sum[10]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[11], winter_sum[10], winter_sum[11]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[12], winter_sum[11], winter_sum[12]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[13], winter_sum[12], winter_sum[13]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[14], winter_sum[13], winter_sum[14]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[15], winter_sum[14], winter_sum[15]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[16], winter_sum[15], winter_sum[16]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[17], winter_sum[16], winter_sum[17]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[18], winter_sum[17], winter_sum[18]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[19], winter_sum[18], winter_sum[19]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[20], winter_sum[19], winter_sum[20]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[21], winter_sum[20], winter_sum[21]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[22], winter_sum[21], winter_sum[22]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[23], winter_sum[22], winter_sum[23]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[24], winter_sum[23], winter_sum[24]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[25], winter_sum[24], winter_sum[25]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[26], winter_sum[25], winter_sum[26]], 0);
|
|
constraint int_lin_eq([-1, -1, 1], [winter[27], winter_sum[26], winter_sum[27]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00001[1], t____00001[2], t____00001[3], x[1]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00002[1], t____00002[2], t____00002[3], x[2]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00003[1], t____00003[2], t____00003[3], x[3]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00004[1], t____00004[2], t____00004[3], x[4]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00005[1], t____00005[2], t____00005[3], x[5]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00006[1], t____00006[2], t____00006[3], x[6]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00007[1], t____00007[2], t____00007[3], x[7]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00008[1], t____00008[2], t____00008[3], x[8]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00009[1], t____00009[2], t____00009[3], x[9]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00010[1], t____00010[2], t____00010[3], x[10]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00011[1], t____00011[2], t____00011[3], x[11]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00012[1], t____00012[2], t____00012[3], x[12]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00013[1], t____00013[2], t____00013[3], x[13]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00014[1], t____00014[2], t____00014[3], x[14]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00015[1], t____00015[2], t____00015[3], x[15]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00016[1], t____00016[2], t____00016[3], x[16]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00017[1], t____00017[2], t____00017[3], x[17]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00018[1], t____00018[2], t____00018[3], x[18]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00019[1], t____00019[2], t____00019[3], x[19]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00020[1], t____00020[2], t____00020[3], x[20]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00021[1], t____00021[2], t____00021[3], x[21]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00022[1], t____00022[2], t____00022[3], x[22]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00023[1], t____00023[2], t____00023[3], x[23]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00024[1], t____00024[2], t____00024[3], x[24]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00025[1], t____00025[2], t____00025[3], x[25]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00026[1], t____00026[2], t____00026[3], x[26]], 0);
|
|
constraint int_lin_eq([-9, -3, -1, 1], [t____00027[1], t____00027[2], t____00027[3], x[27]], 0);
|
|
constraint int_plus(INT____00190, min_val, max_val) :: defines_var(INT____00190);
|
|
constraint maximum_int(max_val, winter_sum);
|
|
constraint minimum_int(min_val, winter_sum);
|
|
solve satisfy;
|