another example

This commit is contained in:
lperron@google.com
2012-06-16 07:30:29 +00:00
parent 1bdbc0281f
commit d6cc60fcf6
6 changed files with 9894 additions and 11753 deletions

File diff suppressed because it is too large Load Diff

View File

@@ -0,0 +1,123 @@
array [1..11] of var 0..1000: C :: output_array([0..10]);
var 0..1000000: INT____00001 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00002 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00003 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00004 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00005 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00006 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00007 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00008 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00009 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00010 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00011 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00012 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00013 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00014 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00015 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00016 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00017 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00018 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00019 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00020 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00021 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00022 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00023 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00024 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00025 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00026 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00027 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00028 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00029 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00030 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00031 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00032 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00033 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00034 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00035 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00036 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00037 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00038 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00039 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00040 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00041 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00042 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00043 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00044 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00045 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00046 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00047 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00048 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00049 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00050 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00051 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00052 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00053 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00054 :: is_defined_var :: var_is_introduced;
var 0..1000000: INT____00055 :: is_defined_var :: var_is_introduced;
constraint int_eq(C[1], 1);
constraint int_lin_eq([-1, 1], [INT____00001, C[2]], 0);
constraint int_lin_eq([-1, -1, 1], [INT____00002, INT____00003, C[3]], 0);
constraint int_lin_eq([-1, -1, -1, 1], [INT____00004, INT____00005, INT____00006, C[4]], 0);
constraint int_lin_eq([-1, -1, -1, -1, 1], [INT____00007, INT____00008, INT____00009, INT____00010, C[5]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, 1], [INT____00011, INT____00012, INT____00013, INT____00014, INT____00015, C[6]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, 1], [INT____00016, INT____00017, INT____00018, INT____00019, INT____00020, INT____00021, C[7]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, 1], [INT____00022, INT____00023, INT____00024, INT____00025, INT____00026, INT____00027, INT____00028, C[8]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00029, INT____00030, INT____00031, INT____00032, INT____00033, INT____00034, INT____00035, INT____00036, C[9]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00037, INT____00038, INT____00039, INT____00040, INT____00041, INT____00042, INT____00043, INT____00044, INT____00045, C[10]], 0);
constraint int_lin_eq([-1, -1, -1, -1, -1, -1, -1, -1, -1, -1, 1], [INT____00046, INT____00047, INT____00048, INT____00049, INT____00050, INT____00051, INT____00052, INT____00053, INT____00054, INT____00055, C[11]], 0);
constraint int_times(C[1], C[1], INT____00001) :: defines_var(INT____00001);
constraint int_times(C[1], C[2], INT____00002) :: defines_var(INT____00002);
constraint int_times(C[1], C[3], INT____00004) :: defines_var(INT____00004);
constraint int_times(C[1], C[4], INT____00007) :: defines_var(INT____00007);
constraint int_times(C[1], C[5], INT____00011) :: defines_var(INT____00011);
constraint int_times(C[1], C[6], INT____00016) :: defines_var(INT____00016);
constraint int_times(C[1], C[7], INT____00022) :: defines_var(INT____00022);
constraint int_times(C[1], C[8], INT____00029) :: defines_var(INT____00029);
constraint int_times(C[1], C[9], INT____00037) :: defines_var(INT____00037);
constraint int_times(C[1], C[10], INT____00046) :: defines_var(INT____00046);
constraint int_times(C[2], C[1], INT____00003) :: defines_var(INT____00003);
constraint int_times(C[2], C[2], INT____00005) :: defines_var(INT____00005);
constraint int_times(C[2], C[3], INT____00008) :: defines_var(INT____00008);
constraint int_times(C[2], C[4], INT____00012) :: defines_var(INT____00012);
constraint int_times(C[2], C[5], INT____00017) :: defines_var(INT____00017);
constraint int_times(C[2], C[6], INT____00023) :: defines_var(INT____00023);
constraint int_times(C[2], C[7], INT____00030) :: defines_var(INT____00030);
constraint int_times(C[2], C[8], INT____00038) :: defines_var(INT____00038);
constraint int_times(C[2], C[9], INT____00047) :: defines_var(INT____00047);
constraint int_times(C[3], C[1], INT____00006) :: defines_var(INT____00006);
constraint int_times(C[3], C[2], INT____00009) :: defines_var(INT____00009);
constraint int_times(C[3], C[3], INT____00013) :: defines_var(INT____00013);
constraint int_times(C[3], C[4], INT____00018) :: defines_var(INT____00018);
constraint int_times(C[3], C[5], INT____00024) :: defines_var(INT____00024);
constraint int_times(C[3], C[6], INT____00031) :: defines_var(INT____00031);
constraint int_times(C[3], C[7], INT____00039) :: defines_var(INT____00039);
constraint int_times(C[3], C[8], INT____00048) :: defines_var(INT____00048);
constraint int_times(C[4], C[1], INT____00010) :: defines_var(INT____00010);
constraint int_times(C[4], C[2], INT____00014) :: defines_var(INT____00014);
constraint int_times(C[4], C[3], INT____00019) :: defines_var(INT____00019);
constraint int_times(C[4], C[4], INT____00025) :: defines_var(INT____00025);
constraint int_times(C[4], C[5], INT____00032) :: defines_var(INT____00032);
constraint int_times(C[4], C[6], INT____00040) :: defines_var(INT____00040);
constraint int_times(C[4], C[7], INT____00049) :: defines_var(INT____00049);
constraint int_times(C[5], C[1], INT____00015) :: defines_var(INT____00015);
constraint int_times(C[5], C[2], INT____00020) :: defines_var(INT____00020);
constraint int_times(C[5], C[3], INT____00026) :: defines_var(INT____00026);
constraint int_times(C[5], C[4], INT____00033) :: defines_var(INT____00033);
constraint int_times(C[5], C[5], INT____00041) :: defines_var(INT____00041);
constraint int_times(C[5], C[6], INT____00050) :: defines_var(INT____00050);
constraint int_times(C[6], C[1], INT____00021) :: defines_var(INT____00021);
constraint int_times(C[6], C[2], INT____00027) :: defines_var(INT____00027);
constraint int_times(C[6], C[3], INT____00034) :: defines_var(INT____00034);
constraint int_times(C[6], C[4], INT____00042) :: defines_var(INT____00042);
constraint int_times(C[6], C[5], INT____00051) :: defines_var(INT____00051);
constraint int_times(C[7], C[1], INT____00028) :: defines_var(INT____00028);
constraint int_times(C[7], C[2], INT____00035) :: defines_var(INT____00035);
constraint int_times(C[7], C[3], INT____00043) :: defines_var(INT____00043);
constraint int_times(C[7], C[4], INT____00052) :: defines_var(INT____00052);
constraint int_times(C[8], C[1], INT____00036) :: defines_var(INT____00036);
constraint int_times(C[8], C[2], INT____00044) :: defines_var(INT____00044);
constraint int_times(C[8], C[3], INT____00053) :: defines_var(INT____00053);
constraint int_times(C[9], C[1], INT____00045) :: defines_var(INT____00045);
constraint int_times(C[9], C[2], INT____00054) :: defines_var(INT____00054);
constraint int_times(C[10], C[1], INT____00055) :: defines_var(INT____00055);
solve :: int_search(C, first_fail, indomain, complete) satisfy;

File diff suppressed because one or more lines are too long

View File

@@ -0,0 +1,25 @@
predicate 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 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);
var 0..9: A :: output_var;
var 0..9: B :: output_var;
var 0..9: C :: output_var;
var 0..9: D :: output_var;
var 0..9: E :: output_var;
var 0..9: F :: output_var;
var 0..9: G :: output_var;
var 0..9: H :: output_var;
var 0..9: I :: output_var;
var 1..99999: INT____00003 :: is_defined_var :: var_is_introduced;
var 0..9: J :: output_var;
array [1..10] of var 0..9: FD :: output_array([1..10]) = [A, B, C, D, E, F, G, H, I, J];
var 0..99999: X;
var 0..99999: Y;
var -99999..99999: difference :: output_var = INT____00003;
constraint all_different_int(FD);
constraint int_lin_eq([-1, 10000, 1000, 100, 10, 1], [X, A, B, C, D, E], 0);
constraint int_lin_eq([-1, 10000, 1000, 100, 10, 1], [Y, F, G, H, I, J], 0);
constraint int_plus(INT____00003, Y, X) :: defines_var(INT____00003);
solve :: int_search(FD, first_fail, indomain, complete) minimize INT____00003;

View File

@@ -0,0 +1,251 @@
predicate all_different_int(array [int] of var int: x);
predicate count(array [int] of var int: x, var int: y, var int: c);
predicate fixed_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 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);
predicate var_cumulative(array [int] of var int: s, array [int] of int: d, array [int] of int: r, var int: b);
var bool: BOOL____00003 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00005 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00011 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00013 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00019 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00021 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00027 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00029 :: 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____00043 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00045 :: 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____00059 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00061 :: 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____00075 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00077 :: 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____00091 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00093 :: 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____00107 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00109 :: 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____00123 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00125 :: 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____00139 :: is_defined_var :: var_is_introduced;
var bool: BOOL____00141 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00006 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00008 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00014 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00016 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00022 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00024 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00030 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00032 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00038 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00040 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00046 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00048 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00054 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00056 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00062 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00064 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00070 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00072 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00078 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00080 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00086 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00088 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00094 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00096 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00102 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00104 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00110 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00112 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00118 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00120 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00126 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00128 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00134 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00136 :: is_defined_var :: var_is_introduced;
var 1..90000: INT____00142 :: is_defined_var :: var_is_introduced;
var 0..300: INT____00144 :: is_defined_var :: var_is_introduced;
array [1..18] of var 1..2: ops :: output_array([1..18]);
array [1..18] of var int: s____00001;
var 666..666: total :: output_var = 666;
array [1..19] of var 1..300: x :: output_array([1..19]);
constraint int_div(x[1], x[2], INT____00008) :: defines_var(INT____00008);
constraint int_div(x[2], x[3], INT____00016) :: defines_var(INT____00016);
constraint int_div(x[3], x[4], INT____00024) :: defines_var(INT____00024);
constraint int_div(x[4], x[5], INT____00032) :: defines_var(INT____00032);
constraint int_div(x[5], x[6], INT____00040) :: defines_var(INT____00040);
constraint int_div(x[6], x[7], INT____00048) :: defines_var(INT____00048);
constraint int_div(x[7], x[8], INT____00056) :: defines_var(INT____00056);
constraint int_div(x[8], x[9], INT____00064) :: defines_var(INT____00064);
constraint int_div(x[9], x[10], INT____00072) :: defines_var(INT____00072);
constraint int_div(x[10], x[11], INT____00080) :: defines_var(INT____00080);
constraint int_div(x[11], x[12], INT____00088) :: defines_var(INT____00088);
constraint int_div(x[12], x[13], INT____00096) :: defines_var(INT____00096);
constraint int_div(x[13], x[14], INT____00104) :: defines_var(INT____00104);
constraint int_div(x[14], x[15], INT____00112) :: defines_var(INT____00112);
constraint int_div(x[15], x[16], INT____00120) :: defines_var(INT____00120);
constraint int_div(x[16], x[17], INT____00128) :: defines_var(INT____00128);
constraint int_div(x[17], x[18], INT____00136) :: defines_var(INT____00136);
constraint int_div(x[18], x[19], INT____00144) :: defines_var(INT____00144);
constraint int_eq(x[1], 72);
constraint int_eq(x[2], 229);
constraint int_eq(x[3], 107);
constraint int_eq(x[4], 97);
constraint int_eq(x[5], 110);
constraint int_eq(x[6], 32);
constraint int_eq(x[7], 75);
constraint int_eq(x[8], 106);
constraint int_eq(x[9], 101);
constraint int_eq(x[10], 108);
constraint int_eq(x[11], 108);
constraint int_eq(x[12], 101);
constraint int_eq(x[13], 114);
constraint int_eq(x[14], 115);
constraint int_eq(x[15], 116);
constraint int_eq(x[16], 114);
constraint int_eq(x[17], 97);
constraint int_eq(x[18], 110);
constraint int_eq(x[19], 100);
constraint int_eq_reif(ops[1], 1, BOOL____00003);
constraint int_eq_reif(ops[1], 2, BOOL____00005);
constraint int_eq_reif(ops[2], 1, BOOL____00011);
constraint int_eq_reif(ops[2], 2, BOOL____00013);
constraint int_eq_reif(ops[3], 1, BOOL____00019);
constraint int_eq_reif(ops[3], 2, BOOL____00021);
constraint int_eq_reif(ops[4], 1, BOOL____00027);
constraint int_eq_reif(ops[4], 2, BOOL____00029);
constraint int_eq_reif(ops[5], 1, BOOL____00035);
constraint int_eq_reif(ops[5], 2, BOOL____00037);
constraint int_eq_reif(ops[6], 1, BOOL____00043);
constraint int_eq_reif(ops[6], 2, BOOL____00045);
constraint int_eq_reif(ops[7], 1, BOOL____00051);
constraint int_eq_reif(ops[7], 2, BOOL____00053);
constraint int_eq_reif(ops[8], 1, BOOL____00059);
constraint int_eq_reif(ops[8], 2, BOOL____00061);
constraint int_eq_reif(ops[9], 1, BOOL____00067);
constraint int_eq_reif(ops[9], 2, BOOL____00069);
constraint int_eq_reif(ops[10], 1, BOOL____00075);
constraint int_eq_reif(ops[10], 2, BOOL____00077);
constraint int_eq_reif(ops[11], 1, BOOL____00083);
constraint int_eq_reif(ops[11], 2, BOOL____00085);
constraint int_eq_reif(ops[12], 1, BOOL____00091);
constraint int_eq_reif(ops[12], 2, BOOL____00093);
constraint int_eq_reif(ops[13], 1, BOOL____00099);
constraint int_eq_reif(ops[13], 2, BOOL____00101);
constraint int_eq_reif(ops[14], 1, BOOL____00107);
constraint int_eq_reif(ops[14], 2, BOOL____00109);
constraint int_eq_reif(ops[15], 1, BOOL____00115);
constraint int_eq_reif(ops[15], 2, BOOL____00117);
constraint int_eq_reif(ops[16], 1, BOOL____00123);
constraint int_eq_reif(ops[16], 2, BOOL____00125);
constraint int_eq_reif(ops[17], 1, BOOL____00131);
constraint int_eq_reif(ops[17], 2, BOOL____00133);
constraint int_eq_reif(ops[18], 1, BOOL____00139);
constraint int_eq_reif(ops[18], 2, BOOL____00141);
constraint int_eq_reif(s____00001[1], INT____00006, false);
constraint int_eq_reif(s____00001[1], INT____00008, false);
constraint int_eq_reif(s____00001[2], INT____00014, false);
constraint int_eq_reif(s____00001[2], INT____00016, false);
constraint int_eq_reif(s____00001[3], INT____00022, false);
constraint int_eq_reif(s____00001[3], INT____00024, false);
constraint int_eq_reif(s____00001[4], INT____00030, false);
constraint int_eq_reif(s____00001[4], INT____00032, false);
constraint int_eq_reif(s____00001[5], INT____00038, false);
constraint int_eq_reif(s____00001[5], INT____00040, false);
constraint int_eq_reif(s____00001[6], INT____00046, false);
constraint int_eq_reif(s____00001[6], INT____00048, false);
constraint int_eq_reif(s____00001[7], INT____00054, false);
constraint int_eq_reif(s____00001[7], INT____00056, false);
constraint int_eq_reif(s____00001[8], INT____00062, false);
constraint int_eq_reif(s____00001[8], INT____00064, false);
constraint int_eq_reif(s____00001[9], INT____00070, false);
constraint int_eq_reif(s____00001[9], INT____00072, false);
constraint int_eq_reif(s____00001[10], INT____00078, false);
constraint int_eq_reif(s____00001[10], INT____00080, false);
constraint int_eq_reif(s____00001[11], INT____00086, false);
constraint int_eq_reif(s____00001[11], INT____00088, false);
constraint int_eq_reif(s____00001[12], INT____00094, false);
constraint int_eq_reif(s____00001[12], INT____00096, false);
constraint int_eq_reif(s____00001[13], INT____00102, false);
constraint int_eq_reif(s____00001[13], INT____00104, false);
constraint int_eq_reif(s____00001[14], INT____00110, false);
constraint int_eq_reif(s____00001[14], INT____00112, false);
constraint int_eq_reif(s____00001[15], INT____00118, false);
constraint int_eq_reif(s____00001[15], INT____00120, false);
constraint int_eq_reif(s____00001[16], INT____00126, false);
constraint int_eq_reif(s____00001[16], INT____00128, false);
constraint int_eq_reif(s____00001[17], INT____00134, false);
constraint int_eq_reif(s____00001[17], INT____00136, false);
constraint int_eq_reif(s____00001[18], INT____00142, false);
constraint int_eq_reif(s____00001[18], INT____00144, false);
constraint int_lin_eq([-1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [666, s____00001[1], s____00001[2], s____00001[3], s____00001[4], s____00001[5], s____00001[6], s____00001[7], s____00001[8], s____00001[9], s____00001[10], s____00001[11], s____00001[12], s____00001[13], s____00001[14], s____00001[15], s____00001[16], s____00001[17], s____00001[18]], 0);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[1], x[1], x[2]], 0, BOOL____00003) :: defines_var(BOOL____00003);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[2], x[2], x[3]], 0, BOOL____00011) :: defines_var(BOOL____00011);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[3], x[3], x[4]], 0, BOOL____00019) :: defines_var(BOOL____00019);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[4], x[4], x[5]], 0, BOOL____00027) :: defines_var(BOOL____00027);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[5], x[5], x[6]], 0, BOOL____00035) :: defines_var(BOOL____00035);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[6], x[6], x[7]], 0, BOOL____00043) :: defines_var(BOOL____00043);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[7], x[7], x[8]], 0, BOOL____00051) :: defines_var(BOOL____00051);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[8], x[8], x[9]], 0, BOOL____00059) :: defines_var(BOOL____00059);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[9], x[9], x[10]], 0, BOOL____00067) :: defines_var(BOOL____00067);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[10], x[10], x[11]], 0, BOOL____00075) :: defines_var(BOOL____00075);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[11], x[11], x[12]], 0, BOOL____00083) :: defines_var(BOOL____00083);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[12], x[12], x[13]], 0, BOOL____00091) :: defines_var(BOOL____00091);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[13], x[13], x[14]], 0, BOOL____00099) :: defines_var(BOOL____00099);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[14], x[14], x[15]], 0, BOOL____00107) :: defines_var(BOOL____00107);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[15], x[15], x[16]], 0, BOOL____00115) :: defines_var(BOOL____00115);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[16], x[16], x[17]], 0, BOOL____00123) :: defines_var(BOOL____00123);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[17], x[17], x[18]], 0, BOOL____00131) :: defines_var(BOOL____00131);
constraint int_lin_eq_reif([1, -1, -1], [s____00001[18], x[18], x[19]], 0, BOOL____00139) :: defines_var(BOOL____00139);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[1], x[1], x[2]], 0, BOOL____00005) :: defines_var(BOOL____00005);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[2], x[2], x[3]], 0, BOOL____00013) :: defines_var(BOOL____00013);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[3], x[3], x[4]], 0, BOOL____00021) :: defines_var(BOOL____00021);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[4], x[4], x[5]], 0, BOOL____00029) :: defines_var(BOOL____00029);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[5], x[5], x[6]], 0, BOOL____00037) :: defines_var(BOOL____00037);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[6], x[6], x[7]], 0, BOOL____00045) :: defines_var(BOOL____00045);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[7], x[7], x[8]], 0, BOOL____00053) :: defines_var(BOOL____00053);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[8], x[8], x[9]], 0, BOOL____00061) :: defines_var(BOOL____00061);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[9], x[9], x[10]], 0, BOOL____00069) :: defines_var(BOOL____00069);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[10], x[10], x[11]], 0, BOOL____00077) :: defines_var(BOOL____00077);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[11], x[11], x[12]], 0, BOOL____00085) :: defines_var(BOOL____00085);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[12], x[12], x[13]], 0, BOOL____00093) :: defines_var(BOOL____00093);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[13], x[13], x[14]], 0, BOOL____00101) :: defines_var(BOOL____00101);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[14], x[14], x[15]], 0, BOOL____00109) :: defines_var(BOOL____00109);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[15], x[15], x[16]], 0, BOOL____00117) :: defines_var(BOOL____00117);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[16], x[16], x[17]], 0, BOOL____00125) :: defines_var(BOOL____00125);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[17], x[17], x[18]], 0, BOOL____00133) :: defines_var(BOOL____00133);
constraint int_lin_eq_reif([1, -1, 1], [s____00001[18], x[18], x[19]], 0, BOOL____00141) :: defines_var(BOOL____00141);
constraint int_times(x[1], x[2], INT____00006) :: defines_var(INT____00006);
constraint int_times(x[2], x[3], INT____00014) :: defines_var(INT____00014);
constraint int_times(x[3], x[4], INT____00022) :: defines_var(INT____00022);
constraint int_times(x[4], x[5], INT____00030) :: defines_var(INT____00030);
constraint int_times(x[5], x[6], INT____00038) :: defines_var(INT____00038);
constraint int_times(x[6], x[7], INT____00046) :: defines_var(INT____00046);
constraint int_times(x[7], x[8], INT____00054) :: defines_var(INT____00054);
constraint int_times(x[8], x[9], INT____00062) :: defines_var(INT____00062);
constraint int_times(x[9], x[10], INT____00070) :: defines_var(INT____00070);
constraint int_times(x[10], x[11], INT____00078) :: defines_var(INT____00078);
constraint int_times(x[11], x[12], INT____00086) :: defines_var(INT____00086);
constraint int_times(x[12], x[13], INT____00094) :: defines_var(INT____00094);
constraint int_times(x[13], x[14], INT____00102) :: defines_var(INT____00102);
constraint int_times(x[14], x[15], INT____00110) :: defines_var(INT____00110);
constraint int_times(x[15], x[16], INT____00118) :: defines_var(INT____00118);
constraint int_times(x[16], x[17], INT____00126) :: defines_var(INT____00126);
constraint int_times(x[17], x[18], INT____00134) :: defines_var(INT____00134);
constraint int_times(x[18], x[19], INT____00142) :: defines_var(INT____00142);
solve satisfy;

View File

@@ -0,0 +1,24 @@
predicate all_different_int(array [int] of var int: x);
predicate count(array [int] of var int: x, var int: y, var int: c);
predicate fixed_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 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..7] of int: LD = [16, 6, 13, 7, 5, 18, 4];
array [1..7] of int: LR = [2, 9, 3, 7, 10, 1, 11];
var int: End :: output_var;
array [1..7] of var 1..30: LE :: output_array([1..7]);
array [1..7] of var 1..30: LO :: output_array([1..7]);
constraint fixed_cumulative(LO, LD, LR, 13);
constraint int_lin_eq([-1, 1], [LE[1], LO[1]], -16);
constraint int_lin_eq([-1, 1], [LE[2], LO[2]], -6);
constraint int_lin_eq([-1, 1], [LE[3], LO[3]], -13);
constraint int_lin_eq([-1, 1], [LE[4], LO[4]], -7);
constraint int_lin_eq([-1, 1], [LE[5], LO[5]], -5);
constraint int_lin_eq([-1, 1], [LE[6], LO[6]], -18);
constraint int_lin_eq([-1, 1], [LE[7], LO[7]], -4);
constraint maximum_int(End, LE);
solve :: int_search(LE, anti_first_fail, indomain_min, complete) minimize End;