diff options
Diffstat (limited to 'etc/compile-by-zinc/femulDisplayReg_1.mzn')
| -rw-r--r-- | etc/compile-by-zinc/femulDisplayReg_1.mzn | 147 |
1 files changed, 147 insertions, 0 deletions
diff --git a/etc/compile-by-zinc/femulDisplayReg_1.mzn b/etc/compile-by-zinc/femulDisplayReg_1.mzn new file mode 100644 index 000000000..222156642 --- /dev/null +++ b/etc/compile-by-zinc/femulDisplayReg_1.mzn @@ -0,0 +1,147 @@ +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) ]; |