diff options
Diffstat (limited to 'etc/compile-by-zinc/femulDisplayReg_0.mzn')
| -rw-r--r-- | etc/compile-by-zinc/femulDisplayReg_0.mzn | 145 |
1 files changed, 145 insertions, 0 deletions
diff --git a/etc/compile-by-zinc/femulDisplayReg_0.mzn b/etc/compile-by-zinc/femulDisplayReg_0.mzn new file mode 100644 index 000000000..dc5cb140e --- /dev/null +++ b/etc/compile-by-zinc/femulDisplayReg_0.mzn @@ -0,0 +1,145 @@ +include "alldifferent.mzn"; +include "cumulative.mzn"; +%uint128_t x20 = x5 * x13; +%uint128_t x21 = x5 * x15; +%uint128_t x22 = x7 * x13; +%uint128_t x23 = x21 + x22; +%uint128_t x24 = x5 * x17; +%uint128_t x25 = x9 * x13; +%uint128_t x26 = x24 + x25; +%uint128_t x27 = x7 * x15; +%uint128_t x28 = x26 + x27; +%uint128_t x29 = x5 * x19; +%uint128_t x30 = x11 * x13; +%uint128_t x31 = x29 + x30; +%uint128_t x32 = x7 * x17; +%uint128_t x33 = x31 + x32; +%uint128_t x34 = x9 * x15; +%uint128_t x35 = x33 + x34; +%uint128_t x36 = x5 * x18; +%uint128_t x37 = x10 * x13; +%uint128_t x38 = x36 + x37; +%uint128_t x39 = x11 * x15; +%uint128_t x40 = x38 + x39; +%uint128_t x41 = x7 * x19; +%uint128_t x42 = x40 + x41; +%uint128_t x43 = x9 * x17; +%uint128_t x44 = x42 + x43; +%uint64_t x45 = x10 * 0x13; +%uint64_t x46 = x7 * 0x13; +%uint64_t x47 = x9 * 0x13; +%uint64_t x48 = x11 * 0x13; +%uint128_t x49 = x45 * x15; +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: x20 = 11; INSTRUCTIONS: x21 = 12; INSTRUCTIONS: x22 = 13; INSTRUCTIONS: x23 = 14; INSTRUCTIONS: x24 = 15; INSTRUCTIONS: x25 = 16; INSTRUCTIONS: x26 = 17; INSTRUCTIONS: x27 = 18; INSTRUCTIONS: x28 = 19; INSTRUCTIONS: x29 = 20; INSTRUCTIONS: x30 = 21; INSTRUCTIONS: x31 = 22; INSTRUCTIONS: x32 = 23; INSTRUCTIONS: x33 = 24; INSTRUCTIONS: x34 = 25; INSTRUCTIONS: x35 = 26; INSTRUCTIONS: x36 = 27; INSTRUCTIONS: x37 = 28; INSTRUCTIONS: x38 = 29; INSTRUCTIONS: x39 = 30; INSTRUCTIONS: x40 = 31; INSTRUCTIONS: x41 = 32; INSTRUCTIONS: x42 = 33; INSTRUCTIONS: x43 = 34; INSTRUCTIONS: x44 = 35; INSTRUCTIONS: x45 = 36; INSTRUCTIONS: x46 = 37; INSTRUCTIONS: x47 = 38; INSTRUCTIONS: x48 = 39; INSTRUCTIONS: x49 = 40; array[INSTRUCTIONS] of string: INSTRUCTIONS_NAMES = ["x10", "x11", "x9", "x7", "x5", "x18", "x19", "x17", "x15", "x13", "x20", "x21", "x22", "x23", "x24", "x25", "x26", "x27", "x28", "x29", "x30", "x31", "x32", "x33", "x34", "x35", "x36", "x37", "x38", "x39", "x40", "x41", "x42", "x43", "x44", "x45", "x46", "x47", "x48", "x49"]; + +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, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 2]; +var LOCATIONS: RET_loc; +constraint cumulative(output_locations, live_duration, output_register_count, 16); + + +constraint alldifferent(output_locations); + +constraint output_locations[x45] + live_duration[x45] == max([output_locations[x49]]); +constraint output_locations[x43] + live_duration[x43] == max([output_locations[x44]]); +constraint output_locations[x42] + live_duration[x42] == max([output_locations[x44]]); +constraint output_locations[x41] + live_duration[x41] == max([output_locations[x42]]); +constraint output_locations[x40] + live_duration[x40] == max([output_locations[x42]]); +constraint output_locations[x29] + live_duration[x29] == max([output_locations[x31]]); +constraint output_locations[x25] + live_duration[x25] == max([output_locations[x26]]); +constraint output_locations[x24] + live_duration[x24] == max([output_locations[x26]]); +constraint output_locations[x27] + live_duration[x27] == max([output_locations[x28]]); +constraint output_locations[x26] + live_duration[x26] == max([output_locations[x28]]); +constraint output_locations[x21] + live_duration[x21] == max([output_locations[x23]]); +constraint output_locations[x22] + live_duration[x22] == max([output_locations[x23]]); +constraint output_locations[x9] + live_duration[x9] == max([output_locations[x25], output_locations[x34], output_locations[x43], output_locations[x47]]); +constraint output_locations[x7] + live_duration[x7] == max([output_locations[x22], output_locations[x27], output_locations[x32], output_locations[x41], output_locations[x46]]); +constraint output_locations[x5] + live_duration[x5] == max([output_locations[x20], output_locations[x21], output_locations[x24], output_locations[x29], output_locations[x36]]); +constraint output_locations[x32] + live_duration[x32] == max([output_locations[x33]]); +constraint output_locations[x33] + live_duration[x33] == max([output_locations[x35]]); +constraint output_locations[x30] + live_duration[x30] == max([output_locations[x31]]); +constraint output_locations[x31] + live_duration[x31] == max([output_locations[x33]]); +constraint output_locations[x36] + live_duration[x36] == max([output_locations[x38]]); +constraint output_locations[x37] + live_duration[x37] == max([output_locations[x38]]); +constraint output_locations[x34] + live_duration[x34] == max([output_locations[x35]]); +constraint output_locations[x38] + live_duration[x38] == max([output_locations[x40]]); +constraint output_locations[x39] + live_duration[x39] == max([output_locations[x40]]); +constraint output_locations[x18] + live_duration[x18] == max([output_locations[x36]]); +constraint output_locations[x19] + live_duration[x19] == max([output_locations[x29], output_locations[x41]]); +constraint output_locations[x10] + live_duration[x10] == max([output_locations[x37], output_locations[x45]]); +constraint output_locations[x11] + live_duration[x11] == max([output_locations[x30], output_locations[x39], output_locations[x48]]); +constraint output_locations[x13] + live_duration[x13] == max([output_locations[x20], output_locations[x22], output_locations[x25], output_locations[x30], output_locations[x37]]); +constraint output_locations[x15] + live_duration[x15] == max([output_locations[x21], output_locations[x27], output_locations[x34], output_locations[x39], output_locations[x49]]); +constraint output_locations[x17] + live_duration[x17] == max([output_locations[x24], output_locations[x32], output_locations[x43]]); + + +constraint output_locations[x5] + 1 <= output_locations[x20]; +constraint output_locations[x13] + 1 <= output_locations[x20]; +constraint output_locations[x5] + 1 <= output_locations[x21]; +constraint output_locations[x15] + 1 <= output_locations[x21]; +constraint output_locations[x7] + 1 <= output_locations[x22]; +constraint output_locations[x13] + 1 <= output_locations[x22]; +constraint output_locations[x21] + 1 <= output_locations[x23]; +constraint output_locations[x22] + 1 <= output_locations[x23]; +constraint output_locations[x5] + 1 <= output_locations[x24]; +constraint output_locations[x17] + 1 <= output_locations[x24]; +constraint output_locations[x9] + 1 <= output_locations[x25]; +constraint output_locations[x13] + 1 <= output_locations[x25]; +constraint output_locations[x24] + 1 <= output_locations[x26]; +constraint output_locations[x25] + 1 <= output_locations[x26]; +constraint output_locations[x7] + 1 <= output_locations[x27]; +constraint output_locations[x15] + 1 <= output_locations[x27]; +constraint output_locations[x26] + 1 <= output_locations[x28]; +constraint output_locations[x27] + 1 <= output_locations[x28]; +constraint output_locations[x5] + 1 <= output_locations[x29]; +constraint output_locations[x19] + 1 <= output_locations[x29]; +constraint output_locations[x11] + 1 <= output_locations[x30]; +constraint output_locations[x13] + 1 <= output_locations[x30]; +constraint output_locations[x29] + 1 <= output_locations[x31]; +constraint output_locations[x30] + 1 <= output_locations[x31]; +constraint output_locations[x7] + 1 <= output_locations[x32]; +constraint output_locations[x17] + 1 <= output_locations[x32]; +constraint output_locations[x31] + 1 <= output_locations[x33]; +constraint output_locations[x32] + 1 <= output_locations[x33]; +constraint output_locations[x9] + 1 <= output_locations[x34]; +constraint output_locations[x15] + 1 <= output_locations[x34]; +constraint output_locations[x33] + 1 <= output_locations[x35]; +constraint output_locations[x34] + 1 <= output_locations[x35]; +constraint output_locations[x5] + 1 <= output_locations[x36]; +constraint output_locations[x18] + 1 <= output_locations[x36]; +constraint output_locations[x10] + 1 <= output_locations[x37]; +constraint output_locations[x13] + 1 <= output_locations[x37]; +constraint output_locations[x36] + 1 <= output_locations[x38]; +constraint output_locations[x37] + 1 <= output_locations[x38]; +constraint output_locations[x11] + 1 <= output_locations[x39]; +constraint output_locations[x15] + 1 <= output_locations[x39]; +constraint output_locations[x38] + 1 <= output_locations[x40]; +constraint output_locations[x39] + 1 <= output_locations[x40]; +constraint output_locations[x7] + 1 <= output_locations[x41]; +constraint output_locations[x19] + 1 <= output_locations[x41]; +constraint output_locations[x40] + 1 <= output_locations[x42]; +constraint output_locations[x41] + 1 <= output_locations[x42]; +constraint output_locations[x9] + 1 <= output_locations[x43]; +constraint output_locations[x17] + 1 <= output_locations[x43]; +constraint output_locations[x42] + 1 <= output_locations[x44]; +constraint output_locations[x43] + 1 <= output_locations[x44]; +constraint output_locations[x10] + 1 <= output_locations[x45]; +constraint output_locations[x7] + 1 <= output_locations[x46]; +constraint output_locations[x9] + 1 <= output_locations[x47]; +constraint output_locations[x11] + 1 <= output_locations[x48]; +constraint output_locations[x45] + 1 <= output_locations[x49]; +constraint output_locations[x15] + 1 <= output_locations[x49]; + +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) ]; |