include "alldifferent.mzn";
include "cumulative.mzn";
%uint128_t x50 = x20 + x49;
%uint128_t x51 = x46 * x18;
%uint128_t x52 = x50 + x51;
%uint128_t x53 = x47 * x19;
%uint128_t x54 = x52 + x53;
%uint128_t x55 = x48 * x17;
%uint128_t x56 = x54 + x55;
%uint128_t x57 = x45 * x17;
%uint128_t x58 = x23 + x57;
%uint128_t x59 = x47 * x18;
%uint128_t x60 = x58 + x59;
%uint128_t x61 = x48 * x19;
%uint128_t x62 = x60 + x61;
%uint128_t x63 = x45 * x19;
%uint128_t x64 = x28 + x63;
%uint128_t x65 = x48 * x18;
%uint128_t x66 = x64 + x65;
%uint128_t x67 = x45 * x18;
%uint128_t x68 = x35 + x67;
%uint64_t x69 = x56 >> 0x33;
%uint64_t x70 = x56 & 0x7ffffffffffff;
%uint128_t x71 = x69 + x62;
%uint64_t x72 = x71 >> 0x33;
%uint64_t x73 = x71 & 0x7ffffffffffff;
%uint128_t x74 = x72 + x66;
%uint64_t x75 = x74 >> 0x33;
%uint64_t x76 = x74 & 0x7ffffffffffff;
%uint128_t x77 = x75 + x68;
%uint64_t x78 = x77 >> 0x33;
%uint64_t x79 = x77 & 0x7ffffffffffff;
set of int: INSTRUCTIONS = 1..40;
INSTRUCTIONS: x10 = 1; INSTRUCTIONS: x11 = 2; INSTRUCTIONS: x9 = 3; INSTRUCTIONS: x7 = 4; INSTRUCTIONS: x5 = 5; INSTRUCTIONS: x18 = 6; INSTRUCTIONS: x19 = 7; INSTRUCTIONS: x17 = 8; INSTRUCTIONS: x15 = 9; INSTRUCTIONS: x13 = 10; INSTRUCTIONS: x50 = 11; INSTRUCTIONS: x51 = 12; INSTRUCTIONS: x52 = 13; INSTRUCTIONS: x53 = 14; INSTRUCTIONS: x54 = 15; INSTRUCTIONS: x55 = 16; INSTRUCTIONS: x56 = 17; INSTRUCTIONS: x57 = 18; INSTRUCTIONS: x58 = 19; INSTRUCTIONS: x59 = 20; INSTRUCTIONS: x60 = 21; INSTRUCTIONS: x61 = 22; INSTRUCTIONS: x62 = 23; INSTRUCTIONS: x63 = 24; INSTRUCTIONS: x64 = 25; INSTRUCTIONS: x65 = 26; INSTRUCTIONS: x66 = 27; INSTRUCTIONS: x67 = 28; INSTRUCTIONS: x68 = 29; INSTRUCTIONS: x69 = 30; INSTRUCTIONS: x70 = 31; INSTRUCTIONS: x71 = 32; INSTRUCTIONS: x72 = 33; INSTRUCTIONS: x73 = 34; INSTRUCTIONS: x74 = 35; INSTRUCTIONS: x75 = 36; INSTRUCTIONS: x76 = 37; INSTRUCTIONS: x77 = 38; INSTRUCTIONS: x78 = 39; INSTRUCTIONS: x79 = 40; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x10", "x11", "x9", "x7", "x5", "x18", "x19", "x17", "x15", "x13", "x50", "x51", "x52", "x53", "x54", "x55", "x56", "x57", "x58", "x59", "x60", "x61", "x62", "x63", "x64", "x65", "x66", "x67", "x68", "x69", "x70", "x71", "x72", "x73", "x74", "x75", "x76", "x77", "x78", "x79"];

int: MAX_LOC = 144;

set of int: LOCATIONS = 1..MAX_LOC;
array[INSTRUCTIONS] of var LOCATIONS: output_locations;
array[INSTRUCTIONS] of var LOCATIONS: live_duration;
array[INSTRUCTIONS] of int: output_register_count = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 2, 1, 1, 2, 1, 1, 2, 1, 1];
var LOCATIONS: RET_loc;
constraint cumulative(output_locations, live_duration, output_register_count, 16);


constraint alldifferent(output_locations);

constraint output_locations[x75] + live_duration[x75] == max([output_locations[x77]]);
constraint output_locations[x72] + live_duration[x72] == max([output_locations[x74]]);
constraint output_locations[x67] + live_duration[x67] == max([output_locations[x68]]);
constraint output_locations[x66] + live_duration[x66] == max([output_locations[x74]]);
constraint output_locations[x47] + live_duration[x47] == max([output_locations[x53], output_locations[x59]]);
constraint output_locations[x46] + live_duration[x46] == max([output_locations[x51]]);
constraint output_locations[x45] + live_duration[x45] == max([output_locations[x57], output_locations[x63], output_locations[x67]]);
constraint output_locations[x61] + live_duration[x61] == max([output_locations[x62]]);
constraint output_locations[x60] + live_duration[x60] == max([output_locations[x62]]);
constraint output_locations[x63] + live_duration[x63] == max([output_locations[x64]]);
constraint output_locations[x62] + live_duration[x62] == max([output_locations[x71]]);
constraint output_locations[x65] + live_duration[x65] == max([output_locations[x66]]);
constraint output_locations[x64] + live_duration[x64] == max([output_locations[x66]]);
constraint output_locations[x49] + live_duration[x49] == max([output_locations[x50]]);
constraint output_locations[x48] + live_duration[x48] == max([output_locations[x55], output_locations[x61], output_locations[x65]]);
constraint output_locations[x28] + live_duration[x28] == max([output_locations[x64]]);
constraint output_locations[x20] + live_duration[x20] == max([output_locations[x50]]);
constraint output_locations[x23] + live_duration[x23] == max([output_locations[x58]]);
constraint output_locations[x69] + live_duration[x69] == max([output_locations[x71]]);
constraint output_locations[x68] + live_duration[x68] == max([output_locations[x77]]);
constraint output_locations[x54] + live_duration[x54] == max([output_locations[x56]]);
constraint output_locations[x55] + live_duration[x55] == max([output_locations[x56]]);
constraint output_locations[x56] + live_duration[x56] == max([output_locations[x69], output_locations[x70]]);
constraint output_locations[x57] + live_duration[x57] == max([output_locations[x58]]);
constraint output_locations[x50] + live_duration[x50] == max([output_locations[x52]]);
constraint output_locations[x51] + live_duration[x51] == max([output_locations[x52]]);
constraint output_locations[x52] + live_duration[x52] == max([output_locations[x54]]);
constraint output_locations[x53] + live_duration[x53] == max([output_locations[x54]]);
constraint output_locations[x77] + live_duration[x77] == max([output_locations[x78], output_locations[x79]]);
constraint output_locations[x74] + live_duration[x74] == max([output_locations[x75], output_locations[x76]]);
constraint output_locations[x35] + live_duration[x35] == max([output_locations[x68]]);
constraint output_locations[x58] + live_duration[x58] == max([output_locations[x60]]);
constraint output_locations[x59] + live_duration[x59] == max([output_locations[x60]]);
constraint output_locations[x71] + live_duration[x71] == max([output_locations[x72], output_locations[x73]]);
constraint output_locations[x18] + live_duration[x18] == max([output_locations[x51], output_locations[x59], output_locations[x65], output_locations[x67]]);
constraint output_locations[x19] + live_duration[x19] == max([output_locations[x53], output_locations[x61], output_locations[x63]]);
constraint output_locations[x17] + live_duration[x17] == max([output_locations[x55], output_locations[x57]]);


constraint output_locations[x20] + 1 <= output_locations[x50];
constraint output_locations[x49] + 1 <= output_locations[x50];
constraint output_locations[x46] + 1 <= output_locations[x51];
constraint output_locations[x18] + 1 <= output_locations[x51];
constraint output_locations[x50] + 1 <= output_locations[x52];
constraint output_locations[x51] + 1 <= output_locations[x52];
constraint output_locations[x47] + 1 <= output_locations[x53];
constraint output_locations[x19] + 1 <= output_locations[x53];
constraint output_locations[x52] + 1 <= output_locations[x54];
constraint output_locations[x53] + 1 <= output_locations[x54];
constraint output_locations[x48] + 1 <= output_locations[x55];
constraint output_locations[x17] + 1 <= output_locations[x55];
constraint output_locations[x54] + 1 <= output_locations[x56];
constraint output_locations[x55] + 1 <= output_locations[x56];
constraint output_locations[x45] + 1 <= output_locations[x57];
constraint output_locations[x17] + 1 <= output_locations[x57];
constraint output_locations[x23] + 1 <= output_locations[x58];
constraint output_locations[x57] + 1 <= output_locations[x58];
constraint output_locations[x47] + 1 <= output_locations[x59];
constraint output_locations[x18] + 1 <= output_locations[x59];
constraint output_locations[x58] + 1 <= output_locations[x60];
constraint output_locations[x59] + 1 <= output_locations[x60];
constraint output_locations[x48] + 1 <= output_locations[x61];
constraint output_locations[x19] + 1 <= output_locations[x61];
constraint output_locations[x60] + 1 <= output_locations[x62];
constraint output_locations[x61] + 1 <= output_locations[x62];
constraint output_locations[x45] + 1 <= output_locations[x63];
constraint output_locations[x19] + 1 <= output_locations[x63];
constraint output_locations[x28] + 1 <= output_locations[x64];
constraint output_locations[x63] + 1 <= output_locations[x64];
constraint output_locations[x48] + 1 <= output_locations[x65];
constraint output_locations[x18] + 1 <= output_locations[x65];
constraint output_locations[x64] + 1 <= output_locations[x66];
constraint output_locations[x65] + 1 <= output_locations[x66];
constraint output_locations[x45] + 1 <= output_locations[x67];
constraint output_locations[x18] + 1 <= output_locations[x67];
constraint output_locations[x35] + 1 <= output_locations[x68];
constraint output_locations[x67] + 1 <= output_locations[x68];
constraint output_locations[x56] + 1 <= output_locations[x69];
constraint output_locations[x56] + 1 <= output_locations[x70];
constraint output_locations[x69] + 1 <= output_locations[x71];
constraint output_locations[x62] + 1 <= output_locations[x71];
constraint output_locations[x71] + 1 <= output_locations[x72];
constraint output_locations[x71] + 1 <= output_locations[x73];
constraint output_locations[x72] + 1 <= output_locations[x74];
constraint output_locations[x66] + 1 <= output_locations[x74];
constraint output_locations[x74] + 1 <= output_locations[x75];
constraint output_locations[x74] + 1 <= output_locations[x76];
constraint output_locations[x75] + 1 <= output_locations[x77];
constraint output_locations[x68] + 1 <= output_locations[x77];
constraint output_locations[x77] + 1 <= output_locations[x78];
constraint output_locations[x77] + 1 <= output_locations[x79];

constraint max([ output_locations[i] + 1 | i in INSTRUCTIONS ]) <= RET_loc;


solve minimize RET_loc;

output [ "(" ++ show(INSTRUCTIONS_NAMES[i]) ++ ", " ++ show(output_locations[i]) ++ ", " ++ show(live_duration[i]) ++ ") ,\n"
       | i in INSTRUCTIONS ];
output [ "RET_loc: " ++ show(RET_loc) ];