149 lines
10 KiB
MiniZinc
149 lines
10 KiB
MiniZinc
predicate fzn_all_different_int(array [int] of var int: x);
|
|
predicate count(array [int] of var int: x, var int: y, var int: c);
|
|
predicate global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);
|
|
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 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);
|
|
array [1..9] of set of int: nums = [{}, 495..495, 6174..6174, {}, {549945, 631764}, {}, {63317664, 97508421}, {554999445, 864197532}, {6333176664, 9753086421, 9975084201}];
|
|
var bool: BOOL____00067 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00068 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00072 :: is_defined_var :: var_is_introduced;
|
|
var bool: BOOL____00073 :: is_defined_var :: var_is_introduced;
|
|
var 0..9: INT____00069 :: is_defined_var :: var_is_introduced;
|
|
var 1..10: INT____00070 :: is_defined_var :: var_is_introduced;
|
|
var 0..999: INT____00071 :: is_defined_var :: var_is_introduced;
|
|
var 1..10: i____00065;
|
|
var 0..999: ord_num____00004;
|
|
var 0..999: ord_num____00011;
|
|
var 0..999: ord_num____00018;
|
|
var 0..999: ord_num____00025;
|
|
var 0..999: ord_num____00032;
|
|
var 0..999: ord_num____00039;
|
|
var 0..999: ord_num____00046;
|
|
var 0..999: ord_num____00053;
|
|
var 0..999: ord_num____00060;
|
|
var 1..10: pos :: output_var = i____00065;
|
|
var 0..999: rev_num____00005;
|
|
var 0..999: rev_num____00012;
|
|
var 0..999: rev_num____00019;
|
|
var 0..999: rev_num____00026;
|
|
var 0..999: rev_num____00033;
|
|
var 0..999: rev_num____00040;
|
|
var 0..999: rev_num____00047;
|
|
var 0..999: rev_num____00054;
|
|
var 0..999: rev_num____00061;
|
|
array [1..3] of var 0..9: s_num____00001;
|
|
array [1..3] of var 0..9: s_num____00008;
|
|
array [1..3] of var 0..9: s_num____00015;
|
|
array [1..3] of var 0..9: s_num____00022;
|
|
array [1..3] of var 0..9: s_num____00029;
|
|
array [1..3] of var 0..9: s_num____00036;
|
|
array [1..3] of var 0..9: s_num____00043;
|
|
array [1..3] of var 0..9: s_num____00050;
|
|
array [1..3] of var 0..9: s_num____00057;
|
|
array [1..3] of var 0..9: s_ordered____00002;
|
|
array [1..3] of var 0..9: s_ordered____00009;
|
|
array [1..3] of var 0..9: s_ordered____00016;
|
|
array [1..3] of var 0..9: s_ordered____00023;
|
|
array [1..3] of var 0..9: s_ordered____00030;
|
|
array [1..3] of var 0..9: s_ordered____00037;
|
|
array [1..3] of var 0..9: s_ordered____00044;
|
|
array [1..3] of var 0..9: s_ordered____00051;
|
|
array [1..3] of var 0..9: s_ordered____00058;
|
|
array [1..3] of var 0..9: s_reverse____00003;
|
|
array [1..3] of var 0..9: s_reverse____00010;
|
|
array [1..3] of var 0..9: s_reverse____00017;
|
|
array [1..3] of var 0..9: s_reverse____00024;
|
|
array [1..3] of var 0..9: s_reverse____00031;
|
|
array [1..3] of var 0..9: s_reverse____00038;
|
|
array [1..3] of var 0..9: s_reverse____00045;
|
|
array [1..3] of var 0..9: s_reverse____00052;
|
|
array [1..3] of var 0..9: s_reverse____00059;
|
|
array [1..10] of var 0..999: x :: output_array([1..10]);
|
|
constraint array_bool_and([BOOL____00072, BOOL____00068, BOOL____00068], BOOL____00073) :: defines_var(BOOL____00073);
|
|
constraint array_var_int_element(INT____00070, x, INT____00071) :: defines_var(INT____00071);
|
|
constraint array_var_int_element(i____00065, x, 495);
|
|
constraint bool_le(BOOL____00067, BOOL____00073);
|
|
constraint int_eq(s_reverse____00003[1], s_ordered____00002[3]);
|
|
constraint int_eq(s_reverse____00003[2], s_ordered____00002[2]);
|
|
constraint int_eq(s_reverse____00003[3], s_ordered____00002[1]);
|
|
constraint int_eq(s_reverse____00010[1], s_ordered____00009[3]);
|
|
constraint int_eq(s_reverse____00010[2], s_ordered____00009[2]);
|
|
constraint int_eq(s_reverse____00010[3], s_ordered____00009[1]);
|
|
constraint int_eq(s_reverse____00017[1], s_ordered____00016[3]);
|
|
constraint int_eq(s_reverse____00017[2], s_ordered____00016[2]);
|
|
constraint int_eq(s_reverse____00017[3], s_ordered____00016[1]);
|
|
constraint int_eq(s_reverse____00024[1], s_ordered____00023[3]);
|
|
constraint int_eq(s_reverse____00024[2], s_ordered____00023[2]);
|
|
constraint int_eq(s_reverse____00024[3], s_ordered____00023[1]);
|
|
constraint int_eq(s_reverse____00031[1], s_ordered____00030[3]);
|
|
constraint int_eq(s_reverse____00031[2], s_ordered____00030[2]);
|
|
constraint int_eq(s_reverse____00031[3], s_ordered____00030[1]);
|
|
constraint int_eq(s_reverse____00038[1], s_ordered____00037[3]);
|
|
constraint int_eq(s_reverse____00038[2], s_ordered____00037[2]);
|
|
constraint int_eq(s_reverse____00038[3], s_ordered____00037[1]);
|
|
constraint int_eq(s_reverse____00045[1], s_ordered____00044[3]);
|
|
constraint int_eq(s_reverse____00045[2], s_ordered____00044[2]);
|
|
constraint int_eq(s_reverse____00045[3], s_ordered____00044[1]);
|
|
constraint int_eq(s_reverse____00052[1], s_ordered____00051[3]);
|
|
constraint int_eq(s_reverse____00052[2], s_ordered____00051[2]);
|
|
constraint int_eq(s_reverse____00052[3], s_ordered____00051[1]);
|
|
constraint int_eq(s_reverse____00059[1], s_ordered____00058[3]);
|
|
constraint int_eq(s_reverse____00059[2], s_ordered____00058[2]);
|
|
constraint int_eq(s_reverse____00059[3], s_ordered____00058[1]);
|
|
constraint int_eq_reif(INT____00069, INT____00070, BOOL____00068);
|
|
constraint int_eq_reif(x[1], 495, false);
|
|
constraint int_le_reif(2, i____00065, BOOL____00067) :: defines_var(BOOL____00067);
|
|
constraint int_lin_eq([-1, 1], [INT____00069, i____00065], 1) :: defines_var(INT____00069) :: domain;
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00004, rev_num____00005, x[2]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00011, rev_num____00012, x[3]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00018, rev_num____00019, x[4]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00025, rev_num____00026, x[5]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00032, rev_num____00033, x[6]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00039, rev_num____00040, x[7]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00046, rev_num____00047, x[8]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00053, rev_num____00054, x[9]], 0);
|
|
constraint int_lin_eq([1, -1, 1], [ord_num____00060, rev_num____00061, x[10]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00001[1], s_num____00001[2], s_num____00001[3], x[1]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00008[1], s_num____00008[2], s_num____00008[3], x[2]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00015[1], s_num____00015[2], s_num____00015[3], x[3]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00022[1], s_num____00022[2], s_num____00022[3], x[4]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00029[1], s_num____00029[2], s_num____00029[3], x[5]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00036[1], s_num____00036[2], s_num____00036[3], x[6]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00043[1], s_num____00043[2], s_num____00043[3], x[7]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00050[1], s_num____00050[2], s_num____00050[3], x[8]], 0);
|
|
constraint int_lin_eq([-100, -10, -1, 1], [s_num____00057[1], s_num____00057[2], s_num____00057[3], x[9]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00004, s_ordered____00002[1], s_ordered____00002[2], s_ordered____00002[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00011, s_ordered____00009[1], s_ordered____00009[2], s_ordered____00009[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00018, s_ordered____00016[1], s_ordered____00016[2], s_ordered____00016[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00025, s_ordered____00023[1], s_ordered____00023[2], s_ordered____00023[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00032, s_ordered____00030[1], s_ordered____00030[2], s_ordered____00030[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00039, s_ordered____00037[1], s_ordered____00037[2], s_ordered____00037[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00046, s_ordered____00044[1], s_ordered____00044[2], s_ordered____00044[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00053, s_ordered____00051[1], s_ordered____00051[2], s_ordered____00051[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [ord_num____00060, s_ordered____00058[1], s_ordered____00058[2], s_ordered____00058[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00005, s_reverse____00003[1], s_reverse____00003[2], s_reverse____00003[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00012, s_reverse____00010[1], s_reverse____00010[2], s_reverse____00010[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00019, s_reverse____00017[1], s_reverse____00017[2], s_reverse____00017[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00026, s_reverse____00024[1], s_reverse____00024[2], s_reverse____00024[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00033, s_reverse____00031[1], s_reverse____00031[2], s_reverse____00031[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00040, s_reverse____00038[1], s_reverse____00038[2], s_reverse____00038[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00047, s_reverse____00045[1], s_reverse____00045[2], s_reverse____00045[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00054, s_reverse____00052[1], s_reverse____00052[2], s_reverse____00052[3]], 0);
|
|
constraint int_lin_eq([-1, 100, 10, 1], [rev_num____00061, s_reverse____00059[1], s_reverse____00059[2], s_reverse____00059[3]], 0);
|
|
constraint int_lin_le_reif([-1], [i____00065], -2, BOOL____00068) :: defines_var(BOOL____00068);
|
|
constraint int_ne_reif(INT____00071, 495, BOOL____00072) :: defines_var(BOOL____00072);
|
|
constraint sort(s_num____00001, s_ordered____00002);
|
|
constraint sort(s_num____00008, s_ordered____00009);
|
|
constraint sort(s_num____00015, s_ordered____00016);
|
|
constraint sort(s_num____00022, s_ordered____00023);
|
|
constraint sort(s_num____00029, s_ordered____00030);
|
|
constraint sort(s_num____00036, s_ordered____00037);
|
|
constraint sort(s_num____00043, s_ordered____00044);
|
|
constraint sort(s_num____00050, s_ordered____00051);
|
|
constraint sort(s_num____00057, s_ordered____00058);
|
|
constraint int_eq(x[1], 0);
|
|
solve :: int_search(x, input_order, indomain_min, complete) satisfy;
|