dekker.one
The models, scripts, and results of the benchmarks performed for a Half Reification Journal paper
1%
2% Main authors:
3% Mats Carlsson <mats.carlsson@ri.se>
4%
5% This file is part of Unison, see http://unison-code.github.io
6%
7% Copyright (c) 2016, RISE SICS AB
8% All rights reserved.
9%
10% Redistribution and use in source and binary forms, with or without
11% modification, are permitted provided that the following conditions are met:
12% 1. Redistributions of source code must retain the above copyright notice,
13% this list of conditions and the following disclaimer.
14% 2. Redistributions in binary form must reproduce the above copyright notice,
15% this list of conditions and the following disclaimer in the documentation
16% and/or other materials provided with the distribution.
17% 3. Neither the name of the copyright holder nor the names of its contributors
18% may be used to endorse or promote products derived from this software
19% without specific prior written permission.
20%
21% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
22% AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
23% IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
24% ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
25% LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
26% CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
27% SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
28% INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
29% CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
30% ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
31% POSSIBILITY OF SUCH DAMAGE.
32
33include "globals.mzn";
34
35%% solver parameters
36
37bool: optimize_cycles;
38
39%% some constants
40%% N.B. keep in sync with modeler! see also isreal()!
41
42int: TYPE_LINEAR = 0;
43int: TYPE_BRANCH = 1;
44int: TYPE_CALL = 2;
45int: TYPE_TAIL = 3;
46int: TYPE_IN = 4;
47int: TYPE_OUT = 5;
48int: TYPE_KILL = 6;
49int: TYPE_DEFINE = 7;
50int: TYPE_COMBINE = 8;
51int: TYPE_LOW = 9;
52int: TYPE_HIGH = 10;
53int: TYPE_SPLIT2 = 11;
54int: TYPE_SPLIT4 = 12;
55int: TYPE_FUN = 13;
56int: TYPE_COPY = 14;
57
58%% problem parameters
59
60int: MAXF;
61int: MAXO;
62int: MAXP;
63int: MAXT;
64int: MAXC;
65int: MAXI;
66int: MAXR;
67int: MAXB = max(index_set(bb_ops));
68int: MINL;
69int: MAXL;
70int: MAXINSNS = max(o in 0..MAXO)(card(op_instructions[o]));
71int: MAXTEMPS = max(p in 0..MAXP)(card(operand_temps[p]));
72
73set of int: expr = index_set(expr_op);
74
75%% see JSON freq, maxc, ins, tmp, operands, optional_min
76array[int] of int: bb_order;
77array[int] of set of int: bb_ops;
78array[int] of set of int: bb_operands;
79array[int] of set of int: bb_temps;
80array[int] of set of int: bb_subsumed;
81array[int] of int: bb_frequency;
82array[int] of int: bb_maxcycle;
83array[int] of int: bb_optional_min;
84
85%% see JSON operands, instructions, type
86array[int] of set of int: op_operands;
87array[int] of set of int: op_instructions;
88array[int] of int: op_type;
89array[int] of bool: op_mand;
90
91%% see JSON atoms
92array[int] of set of int: atom_regs; % atom -> registers
93
94%% see JSON calleesaved, callersaved, infinite, bounded, range
95set of int: calleesaved;
96set of int: callersaved;
97set of int: infinite;
98array[int] of bool: bounded;
99array[int] of set of int: range;
100
101%% see JSON cap, con, dur, off
102array[int] of int: res_cap;
103array[int,int] of int: res_con;
104array[int,int] of int: res_dur;
105array[int,int] of int: res_off;
106
107%% see JSON congr
108array[int] of set of int: congr;
109
110%% see JSON strictly_congr
111array[int] of set of int: strictly_congr;
112
113%% see JSON preassign
114array[int] of int: preassign_operand;
115array[int] of int: preassign_reg;
116
117%% see JSON aligned/adist
118array[int] of int: aligned_use;
119array[int] of int: aligned_def;
120array[int] of int: aligned_usei;
121array[int] of int: aligned_defi;
122array[int] of int: aligned_dist;
123
124%% see JSON adjacent
125array[int] of int: adj_from;
126array[int] of int: adj_to;
127
128%% see JSON quasi_adjacent
129array[int] of int: quasi_adj_from;
130array[int] of int: quasi_adj_to;
131
132%% see JSON long_latency
133array[int,int] of set of int: long_latency_index;
134array[int] of int: long_latency_def;
135array[int] of int: long_latency_use;
136
137%% see JSON operands
138array[int] of int: operand_definer; % operand -> defining op
139
140%% see JSON use
141array[int] of bool: operand_use;
142
143%% see JSON last_use
144array[int] of bool: operand_lastuse;
145
146%% see JSON temps
147array[int] of set of int: operand_temps;
148
149%% see JSON class, operands, instructions
150array[int,int] of int: operand_atom; % operand x operation -> atom
151
152%% see JSON temps
153array[int] of set of int: related_temps;
154
155%% see JSON definer, temps, width, minlive
156array[int] of int: temp_definer; % temp -> defining op
157array[int] of int: temp_def; % temp -> defining operand
158array[int] of int: temp_width; % temp -> width
159array[int] of int: temp_minlive; % temp -> minlive
160array[int] of set of int: temp_uses; % temp -> set of use operands
161array[int] of set of int: temp_domain; % temp -> domain of regs
162
163%% see JSON packed, pinstrs
164array[int,int] of int: packed_pq;
165
166%% see JSON before
167array[int] of int: before_pred;
168array[int] of int: before_succ;
169array[int] of expr: before_cond;
170
171%% see JSON E
172array[int] of int: adhoc;
173
174%% see JSON nogoods
175array[int] of expr: nogood;
176
177%% see JSON across
178array[int] of int: across_op;
179array[int] of set of int: across_regs;
180array[int] of set of int: across_items;
181array[int] of int: across_item_temp;
182array[int] of expr: across_item_cond;
183
184%% see JSON set_across
185array[int] of int: setacross_op;
186array[int] of set of int: setacross_regs;
187array[int] of set of int: setacross_tempsets;
188
189%% see JSON difftemps
190array[int] of set of int: difftemp;
191
192%% see JSON diffregs
193array[int] of set of int: diffreg;
194
195%% see JSON domops
196array[int] of set of int: domop_operands;
197array[int] of set of int: domop_temps;
198
199%% see JSON domuse
200array[int] of int: domuse_p;
201array[int] of int: domuse_q;
202array[int] of int: domuse_r;
203
204%% see JSON infassign
205array[int,int] of int: infassign;
206
207%% see JSON space
208array[int] of int: space;
209
210%% see JSON dominates
211array[int] of int: dominate_ing;
212array[int] of int: dominate_ed;
213array[int] of set of int: dominate_instructions;
214array[int] of set of int: dominate_temps;
215
216%% see JSON precedences
217array[int] of expr: precedence;
218
219%% see JSON active_tables, tmp_tables
220array[int] of set of int: table_exists_ops;
221array[int] of set of int: table_iffall_ops;
222array[int] of set of int: relation_ops;
223array[int] of set of int: relation_temps;
224array[int] of int: relation_ntuples;
225array[int] of set of int: relation_range;
226
227%% see JSON calleesaved_spill
228array[int] of set of int: calleesaved_spill;
229array[int,int] of int: cs_spill_transpose;
230
231%% see JSON activators
232array[int] of set of int: activator_insns;
233array[int] of set of int: activator_ops;
234
235%% see JSON value_precede_chain
236array[int] of int: value_precede_min;
237array[int] of int: value_precede_max;
238array[int] of set of int: value_precede_regs;
239array[int] of int: value_precede_temps;
240
241%% see JSON lat
242array[int,int] of int: lat_table;
243
244%% see JSON preschedule
245array[int] of int: preschedule_op;
246array[int] of int: preschedule_cycle;
247
248%% see JSON bypass
249array[int,int] of int: bypass_table;
250
251%% see JSON exrelated, table
252array[int] of int: exrelated_p;
253array[int] of int: exrelated_q;
254array[int] of set of int: exrelated_rows;
255array[int,int] of int: exrelated_ext;
256
257%% see JSON wcet
258array[int,int] of int: wcet;
259
260%% extra storage for constraint expressions
261array[int] of int: expr_op;
262array[int] of int: expr_arg1;
263array[int] of int: expr_arg2;
264array[int] of int: expr_arg3;
265array[int] of set of int: expr_children;
266
267%% extra store for relations in table constraints
268array[int] of int: ints;
269
270%% extra storage: each set is a set of temporaries
271array[int] of set of int: sets;
272
273%% problem variables
274
275var 0..MAXF: objective;
276array[0..MAXO] of var bool: a;
277array[0..MAXO] of var 1..MAXINSNS: ii; % same as in gecode-solver
278array[0..MAXO] of var -1..MAXC: c;
279array[0..MAXP] of var -1..MAXR: rt;
280array[0..MAXP] of var MINL..MAXL: lt; % operand latency
281array[0..MAXP] of var -MAXL..MAXL: s; % global operand slack
282array[0..MAXP] of var 1..MAXTEMPS: y; % same as in gecode-solver
283array[-1..MAXT] of var -1..MAXR: r;
284array[-1..MAXT] of var -1..MAXC: ls;
285array[-1..MAXT] of var 0..MAXC: ld;
286array[-1..MAXT] of var -1..MAXC: le;
287array[1..MAXB] of var 0..MAXC: copysum;
288
289%% PREDICATES AND TESTS
290
291test isreal(int: o) = (op_type[o] in
292 {TYPE_LINEAR, TYPE_BRANCH, TYPE_CALL, TYPE_TAIL, TYPE_FUN, TYPE_COPY});
293
294test fixedop(int: o) = (
295 op_instructions[o] != {0} /\ card(op_instructions[o]) = 1
296);
297
298test all_equal_ints(array[int] of int: x) =
299 forall(i, j in index_set(x) where i < j) ( x[i] = x[j] );
300
301var int: res_con_of_op(int: res, int: o) =
302 let {array[int] of int: I = op_instructions[o]} in
303 let {array[int] of int: ints = [res_con[res,I[i]] | i in index_set(I)]} in
304 if all_equal_ints(ints) then ints[1] else ints[ii[o]] endif;
305
306var int: res_dur_of_op(int: res, int: o) =
307 let {array[int] of int: I = op_instructions[o]} in
308 let {array[int] of int: ints = [res_dur[res,I[i]] | i in index_set(I)]} in
309 if all_equal_ints(ints) then ints[1] else ints[ii[o]] endif;
310
311var int: res_off_of_op(int: res, int: o) =
312 let {array[int] of int: I = op_instructions[o]} in
313 let {array[int] of int: ints = [res_off[res,I[i]] | i in index_set(I)]} in
314 if all_equal_ints(ints) then ints[1] else ints[ii[o]] endif;
315
316predicate insn_eq(int: o, int: x) =
317 let {array[int] of int: I = op_instructions[o]} in
318 exists(j in index_set(I) where I[j]=x)(ii[o]=j);
319
320predicate insn_in(int: o, set of int: X) =
321 if card(X)=0 then
322 false
323 else if card(X)=1 then
324 insn_eq(o, min(X))
325 else
326 let {array[int] of int: I = op_instructions[o]} in
327 ii[o] in {j | j in index_set(I) where I[j] in X}
328 endif endif;
329
330predicate smart_alldiff(array[int] of var int: X) =
331 if length(X)<2 then
332 true
333 else if length(X)=2 then
334 let {set of int: S = index_set(X)} in
335 X[min(S)] != X[max(S)]
336 else
337 all_different(X)
338 endif endif;
339
340predicate ra_diffn(array[int] of var int: R,
341 array[int] of int: W,
342 array[int] of set of int: D,
343 array[int] of var int: LS,
344 array[int] of var int: LD,
345 array[int] of var int: LE) =
346 diffn_nonstrict(R, LS, W, LD);
347
348predicate disjoint1(array[int] of var int: x,
349 array[int] of var int: w) =
350 diffn(x, [1 | i in index_set(x)], w, [1 | i in index_set(x)]) ;
351
352predicate noverlap(array[int] of var int: x,
353 array[int] of var int: w) = (
354 if min([lb(z) | z in w]) < max([ub(z) | z in w]) then
355 disjoint1(x, w)
356 else if length(x) = 2 then
357 x[1] != x[2]
358 else
359 smart_alldiff(x)
360 endif endif
361 );
362
363predicate live_overlap(int: k, int: j) = (ls[k] < le[j] /\ ls[j] < le[k]);
364
365predicate operand_live_overlap(int: p, int: q) = (ls_t(p) < le_t(q) /\ ls_t(q) < le_t(p));
366
367predicate operand_live_before(int: p, int: q) = (le_t(p) <= ls_t(q));
368
369test operand_related(int: p, int: q) =
370 operand_temps[p] subset operand_temps[q] \/ operand_temps[q] subset operand_temps[p];
371
372predicate same_temp(int: p, int: q) =
373 assert(operand_related(p,q), "same_temp[\(p),\(q)] with unrelated operands") /\
374 y[p] = y[q];
375
376predicate temp_eq(int: p, int: t) =
377 let {array[int] of int: ts = operand_temps[p]} in
378 exists(j in index_set(ts) where ts[j]=t)(y[p]=j);
379
380predicate temp_in(int: p, set of int: T) =
381 if card(T)=0 then
382 false
383 else if card(T)=1 then
384 temp_eq(p, min(T))
385 else
386 let {array[int] of int: ts = operand_temps[p]} in
387 y[p] in {j | j in index_set(ts) where ts[j] in T}
388 endif endif;
389
390test temp_is_unsafe(int: t) =
391 if op_type[temp_definer[t]] in {TYPE_IN,TYPE_DEFINE,TYPE_FUN} then
392 false
393 else
394 let {array[int] of int: dlats = [lat_table[j,4] | j in index_set_1of2(lat_table)
395 where
396 lat_table[j,2] != 0 /\
397 lat_table[j,3] = temp_def[t]
398 ],
399 array[int] of int: ulats = [lat_table[j,4] | j in index_set_1of2(lat_table)
400 where
401 lat_table[j,2] != 0 /\
402 lat_table[j,3] in temp_uses[t]
403 ]} in
404 temp_minlive[t] > min(dlats) + min(ulats)
405 endif;
406
407test temp_must_be_real(int: p) =
408 min(operand_temps[p])>=0;
409
410predicate temp_is_real(int: p) =
411 if min(operand_temps[p])>=0 then
412 true
413 else
414 y[p]!=1
415 endif;
416
417predicate temp_is_real_reif(int: p, var bool: re) =
418 if min(operand_temps[p])>=0 then
419 re
420 else
421 re <-> y[p]!=1
422 endif;
423
424predicate insn_is_real_reif(int: o, var bool: re) =
425 if min(op_instructions[o])>=1 then
426 re
427 else
428 re <-> ii[o]!=1
429 endif;
430
431predicate temp_member_reif(set of int: P, int: t, var bool: re) =
432 (re <-> exists(p in P)(temp_eq(p,t)));
433
434var int: t(int: p) =
435 if card(operand_temps[p])=1 then min(operand_temps[p])
436 else if card(operand_temps[p])=2 then
437 let {int: a = min(operand_temps[p]),
438 int: b = max(operand_temps[p])}
439 in (b-a)*y[p] -b+a+a
440 else
441 operand_temps[p][y[p]]
442 endif endif;
443
444var int: ls_t(int: p) = [ls[t] | t in operand_temps[p]][y[p]];
445
446var int: le_t(int: p) = [le[t] | t in operand_temps[p]][y[p]];
447
448%% conditions
449predicate eval_expr(int: l) = (
450 let {int: tag = expr_op[l],
451 int: arg1 = expr_arg1[l],
452 int: arg2 = expr_arg2[l],
453 int: arg3 = expr_arg3[l],
454 } in (
455 if tag=0 then exists(j in expr_children[l])(eval_expr(j))
456 else if tag=1 then forall(j in expr_children[l])(eval_expr(j))
457 else if tag=2 then eval_expr(arg1) xor eval_expr(arg2)
458 else if tag=3 then eval_expr(arg1) -> eval_expr(arg2)
459 else if tag=4 then not eval_expr(arg1)
460 else if tag=5 then a[arg1]
461 else if tag=6 then temp_eq(arg1,arg2)
462 else if tag=7 then insn_eq(arg1,arg2)
463 else if tag=8 then c[arg2] >= c[arg1] + arg3
464 else if tag=9 then same_temp(arg1,arg2)
465 else if tag=10 then operand_live_overlap(arg1,arg2)
466 else if tag=11 then live_overlap(arg1,arg2)
467 else if tag=12 then r[arg1] in callersaved
468 else if tag=13 then rt[arg1] in atom_regs[arg2]
469 else false endif endif endif endif endif endif endif endif endif endif endif endif endif endif
470 )
471);
472
473var int: ite(var bool: cond, var int: thenval, var int: elseval) = (
474 let {array[1..2] of var int: ar = [elseval,thenval]} in
475 ar[cond+1]
476);
477
4780..MAXT: single_temp(int: p) = max(operand_temps[p]);
479
480set of 0..MAXT: real_temps(int: p) = operand_temps[p] intersect 0..MAXT;
481
482%% (mostly) ESSENTIAL CONSTRAINT
483
484%% basic invariants, null instructions
485
486test opt_in_temporary(int: v) =
487 let {int: p = temp_def[v]} in
488 op_type[temp_definer[v]] = TYPE_IN /\ card(operand_temps[p])>1;
489
490constraint
491 r[-1] = -1 /\
492 ls[-1] = -1 /\
493 ld[-1] = 0 /\
494 le[-1] = -1 /\
495 forall(o in 0..MAXO where op_mand[o]) (a[o]) /\
496 forall(o in 0..MAXO where not op_mand[o]) (insn_is_real_reif(o,a[o])) /\
497 forall(o in 0..MAXO) (a[o] <-> c[o] >= 0) /\
498 forall(p in 0..MAXP where card(operand_temps[p])>1) (rt[p] = [r[v] | v in operand_temps[p]][y[p]]) /\
499 forall(p in 0..MAXP where card(operand_temps[p])=1) (rt[p] = r[single_temp(p)]) /\
500 forall(p in 0..MAXP where not op_mand[operand_definer[p]]) % rematerialization
501 (temp_is_real_reif(p,a[operand_definer[p]])) /\
502 forall(v in 0..MAXT) (ls[v]+ld[v] = le[v]) /\
503 forall(v in 0..MAXT where not opt_in_temporary(v)) % rematerialization
504 (ls[v] = c[temp_definer[v]] /\
505 (a[temp_definer[v]] <-> r[v] >= 0)) /\
506 forall(v in 0..MAXT where opt_in_temporary(v)) % rematerialization
507 (ls[v] in -1 .. 0 /\
508 (r[v] >= 0 <-> ls[v]=0) /\
509 (r[v] >= 0 <-> temp_eq(temp_def[v],v))) /\
510 forall(v in 0..MAXT) (
511 let {bool: unsafe = temp_is_unsafe(v),
512 set of int: pset = temp_uses[v],
513 set of int: prange = 1..card(pset),
514 array[prange] of int: parr = [p | p in pset],
515 array[prange] of var -1..MAXC: carr} in (
516 forall(p in prange) (carr[p] = ite(temp_eq(parr[p],v), c[operand_definer[parr[p]]], -1)) /\
517 if card(pset)=1 /\ not unsafe then
518 le[v] = carr[1]
519 else if not unsafe then
520 maximum(le[v], carr)
521 else
522 maximum(le[v], carr++[ls[v]+ % 20130930: live range can extend past last use
523 temp_minlive[v]*bool2int(a[temp_definer[v]])])
524 endif endif
525 )
526 );
527
528%% objective, bounds on (out) cycle
529
530constraint
531 forall(b in 1..MAXB) (
532 forall(o in bb_ops[b])(c[o] in -1..bb_maxcycle[b]) /\
533 c[min(bb_ops[b])] = 0 /\
534 copysum[b] = sum(o in bb_ops[b] where not op_mand[o])(bool2int(a[o])) /\
535 copysum[b] >= bb_optional_min[b]
536 ) /\
537 if optimize_cycles then
538 objective = sum(b in 1..MAXB) (bb_frequency[b] * c[max(bb_ops[b])])
539 else
540 objective = sum(o in 0..MAXO)(res_con_of_op(1,o))
541 endif;
542
543%% domains
544constraint
545 forall(o in 0..MAXO) (ii[o] in 1..card(op_instructions[o]));
546
547constraint
548 forall(q in 0..MAXP) (y[q] in 1..card(operand_temps[q]));
549
550set of int: temp_insn_regs(int: v, int: j) =
551 let {int: p = temp_def[v],
552 int: w = temp_width[v],
553 int: oa = operand_atom[p,j],
554 set of int: ks = {k | k in index_set_1of2(infassign) where infassign[k,1]=v /\ infassign[k,2]=space[oa]},
555 set of int: unaligned =
556 if card(ks)>0 then
557 {r | r in atom_regs[oa]} intersect (infassign[min(ks),3]..infassign[min(ks),4])
558 else
559 {r | r in atom_regs[oa]}
560 endif}
561 in {r | r in unaligned /*where r mod w = 0*/}; % currently, that would over-constrain
562
563set of int: generic_temp_domain(int: t1) =
564 if card(temp_domain[t1]) > 0 then
565 temp_domain[t1]
566 else
567 let {int: p = temp_def[t1],
568 set of int: rdom = array_union([temp_insn_regs(t1,j) | j in 1..MAXI]),
569 set of int: joker = if min(operand_temps[p])>=0 then {} else {-1} endif, % rematerialization
570 } in rdom union joker
571 endif;
572
573constraint
574 forall(t1 in 0..MAXT) (r[t1] in generic_temp_domain(t1));
575
576%% operation selection (register set depending on operation)
577constraint
578 forall(p in 0..MAXP)(
579 let {int: o = operand_definer[p],
580 set of int: joker = if min(operand_temps[p])>=0 then {} else {-1} endif} in
581 if fixedop(o) then
582 rt[p] in atom_regs[operand_atom[p,min(op_instructions[o])]] union joker % rematerialization
583 else
584 let {array[int] of set of int: doms = [ if insn=0 then {-1} else atom_regs[operand_atom[p,insn]] endif
585 | insn in op_instructions[o]
586 ],
587 array[int] of int: extension = [ if k=1 then j else r endif
588 | j in index_set(op_instructions[o]),
589 r in doms[j],
590 k in 1..2
591 ],
592 int: nt = length(extension) div 2} in
593 if forall(i in index_set(doms))(doms[i] = doms[1]) then
594 rt[p] in doms[1]
595 else
596 table([ii[o],rt[p]], array2d(1..nt, 1..2, extension))
597 endif
598 endif
599 );
600
601%% preassignments
602constraint
603 forall(j in index_set(preassign_reg))
604 (rt[preassign_operand[j]] = preassign_reg[j]);
605
606%% congruences
607constraint
608 forall(cgr in strictly_congr) (
609 let {int: junior = min(cgr)} in (
610 forall(j in cgr where j>junior) (rt[junior] = rt[j])
611 )
612 );
613
614%% adjacencies % rematerialization
615constraint
616 forall( j in index_set(adj_from)
617 where not({adj_from[j],adj_to[j]} subset array_union(strictly_congr))
618 ) (
619 let {int: p = adj_from[j],
620 int: q = adj_to[j]} in
621 (temp_is_real(q) -> temp_is_real(p)) /\
622 (temp_is_real(q) -> rt[p] = rt[q]) /\
623 (temp_is_real(p) -> exists(k in index_set(adj_from) where adj_from[k] = p)(temp_is_real(adj_to[k])))
624 );
625
626constraint
627 forall(j in index_set(quasi_adj_from)) (
628 let {int: p = quasi_adj_from[j],
629 int: q = quasi_adj_to[j]} in
630 temp_is_real(q) -> temp_is_real(p)
631 );
632
633%% aligned/adist
634constraint
635 forall(j in index_set(aligned_use)) (
636 let {int: p = aligned_use[j],
637 int: q = aligned_def[j],
638 int: pi = aligned_usei[j],
639 int: qi = aligned_defi[j],
640 int: offset = aligned_dist[j]} in (
641 insn_eq(operand_definer[p],pi) /\ insn_eq(operand_definer[q],qi) -> rt[p] + offset = rt[q]
642 )
643 );
644
645%% disjoint live ranges
646constraint
647 forall(T in bb_temps) (
648 ra_diffn([r[v] | v in T],
649 [temp_width[v] | v in T],
650 [generic_temp_domain(v) | v in T],
651 [ls[v] | v in T],
652 [ld[v] | v in T],
653 [le[v] | v in T])
654 );
655
656%% precedences (with conditions added by presolver)
657constraint
658 forall(P in precedence) (
659 eval_expr(P)
660 );
661
662%% slack and balancing
663
664%% Model::global_operand
665test global_operand(int: p) =
666 exists(j in index_set(adj_from))(adj_from[j]=p) \/
667 exists(j in index_set(adj_to))(adj_to[j]=p);
668
669%% Model::slack
670constraint
671 forall(p in 0..MAXP)(if not global_operand(p) then s[p]=0 else true endif);
672
673%% CompleteModel::post_slack_balancing_constraints
674constraint
675 forall(j in index_set(adj_from)) (
676 s[adj_from[j]] + s[adj_to[j]] = 0
677 );
678
679%% Model::post_operand_latency_definition
680constraint
681 forall(o in 0..MAXO, p in op_operands[o])(
682 let {array[int] of int: lcol = [ lat_table[j,4]
683 | j in index_set_1of2(lat_table)
684 where lat_table[j,1] = o /\ lat_table[j,3] = p
685 ],
686 int: n = length(lcol),
687 bool: simple = if not op_mand[o] then
688 forall(k in 2..n)(lcol[k]=lcol[2])
689 else
690 forall(k in 1..n)(lcol[k]=lcol[1])
691 endif} in
692 if simple then
693 lt[p] = lcol[n]
694 else
695 lt[p] = lcol[ii[o]]
696 endif
697 );
698
699%% Model::post_temporary_use_latency_definition
700var -MAXL..3*MAXL: lat(int: q, int: v) =
701 let {int: p = temp_def[v]} in
702 lt[p] + s[p] + lt[q] + s[q];
703
704%% data precedences with slack and everything
705
706array[int] of var int: opnd_lbs(int: q) =
707 [ if v = -1 then -1
708 else c[temp_definer[v]] + lat(q,v)
709 endif
710 | v in operand_temps[q]
711 ];
712
713predicate post_data_prec(int: q) =
714 let {int: u = operand_definer[q],
715 array[int] of var int: lbs = opnd_lbs(q)} in
716 c[u] >= lbs[1] /\
717 c[u] >= lbs[y[q]];
718
719%% Model::post_data_precedences_constraints
720%% redundant if op_type[operand_definer[q]]!=TYPE_KILL and implied constraints are being posted
721constraint
722 forall(q in 0..MAXP where operand_use[q])(post_data_prec(q));
723
724%% resources
725
726test unit_res_dur_cap(int: res, set of int: active) = (
727 forall(o in active, oi in op_instructions[o])(
728 res_con[res,oi]=res_cap[res] /\
729 res_dur[res,oi]=1 /\
730 res_off[res,oi]=0
731 )
732);
733
734test unit_res_dur(int: res, int: o) = (
735 forall(oi in op_instructions[o])(res_dur[res,oi]=1)
736);
737
738test zero_res_off(int: res, int: o) = (
739 forall(oi in op_instructions[o])(res_off[res,oi]=0)
740);
741
742constraint
743 forall(b in 1..MAXB, res in index_set(res_cap) diff bb_subsumed[b]) (
744 let {set of int: active = {o | o in bb_ops[b] where
745 exists(q in op_instructions[o])(res_con[res,q]>0)}} in (
746 if card(active)<=1 then true
747 else if unit_res_dur_cap(res,active) then
748 smart_alldiff([c[o] | o in active])
749 else
750 cumulative([ if zero_res_off(res,o) then c[o] else c[o]+res_off_of_op(res,o) endif
751 | o in active
752 ],
753 [ if unit_res_dur(res,o) then 1 else res_dur_of_op(res,o) endif
754 | o in active
755 ],
756 [ res_con_of_op(res,o)
757 | o in active
758 ],
759 res_cap[res])
760 endif endif
761 )
762 );
763
764
765%% packing constraints
766%% see Model::post_packing_constraints()
767constraint
768 forall(k in index_set_1of2(packed_pq)) (
769 let {int: p = packed_pq[k,1],
770 int: q = packed_pq[k,2],
771 int: w = temp_width[single_temp(p)],
772 array[int] of int: modtab = [-1,-1]++[ if k=1 then v else v + w - 2*(v mod 2*w) endif
773 | v in 0..MAXR, k in 1..2
774 where v mod w = 0
775 ],
776 int: nt = length(modtab) div 2,
777 } in
778 table([rt[p], rt[q]], array2d(1..nt, 1..2, modtab))
779 );
780
781%% activators
782constraint
783 forall(x in index_set(activator_insns))(
784 let {set of int: is = activator_insns[x],
785 set of int: os = activator_ops[x]} in (
786 (a[min(os)] <-> exists(o in 0..MAXO)(insn_in(o,op_instructions[o] intersect is))) /\
787 forall(i2 in os where i2>min(os))(a[i2] <-> a[min(os)])
788 )
789 );
790
791%% prescheduling
792constraint
793 forall(j in index_set(preschedule_op))(
794 let {int: oper = preschedule_op[j],
795 int: cycle = preschedule_cycle[j],
796 int: bb = min({k | k in index_set(bb_ops) where oper in bb_ops[k]}),
797 int: outop = max(bb_ops[bb])}
798 in (a[oper] -> c[oper] = cycle) /\
799 (a[oper] <-> c[outop] > cycle)
800 );
801
802%% bypass
803constraint
804 forall(j in index_set_1of2(bypass_table))(
805 let {int: o = bypass_table[j,1],
806 int: insn = bypass_table[j,2],
807 int: p = bypass_table[j,3]}
808 in insn_eq(o,insn) -> c[o] = ls_t(p)
809 );
810
811%% exrelated
812constraint
813 forall(j in index_set(exrelated_p))(
814 let {int: p = exrelated_p[j],
815 int: q = exrelated_q[j],
816 array[int] of int: ext = [exrelated_ext[r,k] | r in exrelated_rows[j], k in 1..2]}
817 in table([rt[p],rt[q]], array2d(1..(length(ext) div 2), 1..2, ext))
818 );
819
820%% ad-hoc
821constraint
822 forall(L in adhoc) (
823 eval_expr(L)
824 );
825
826%% IMPLIED CONSTRAINTS
827
828%% effective copy, handling multiple defs and/or uses
829constraint
830 symmetry_breaking_constraint(
831 forall(o in 0..MAXO where op_type[o] = TYPE_COPY)(
832 let {int: src = min([p | p in op_operands[o] where operand_use[p]]),
833 int: dst = min([p | p in op_operands[o] where not operand_use[p]])} in
834 a[o] -> rt[src] != rt[dst]
835 )
836 );
837
838%% dominating copies
839constraint
840 symmetry_breaking_constraint(
841 forall(k in index_set(dominate_ing)) (
842 let {int: ing = dominate_ing[k],
843 int: ed = dominate_ed[k],
844 int: edsrc = min(op_operands[ed]),
845 set of int: iset = dominate_instructions[k],
846 set of int: tset = dominate_temps[k]} in (
847 a[ing] \/ not a[ed] \/ insn_in(ed,iset) \/ temp_in(edsrc,tset)
848 )
849 )
850 );
851
852%% disjoint registers
853constraint
854 redundant_constraint(
855 forall(R in diffreg) (
856 noverlap([rt[j] | j in R],
857 [temp_width[min(operand_temps[j])] | j in R])
858 )
859 );
860
861%% different temporaries
862constraint
863 redundant_constraint(
864 forall(T in difftemp) (
865 let {array[int] of int: TA = T} in
866 forall(j in index_set(TA), k in index_set(TA) where j<k)(
867 assert(operand_related(TA[j],TA[k]), "difftemp(\(T)) with unrelated operands")
868 ) /\
869 smart_alldiff([y[p] | p in T])
870 )
871 );
872
873%% nogoods
874constraint
875 redundant_constraint(
876 forall(N in nogood) (
877 not eval_expr(N)
878 )
879 );
880
881%% Model::post_connected_users_constraints
882constraint
883 redundant_constraint(
884 forall(p in 0..MAXP where not operand_use[p])(
885 let {int: v = single_temp(p)} in (
886 if temp_must_be_real(p) then
887 temp_member_reif(temp_uses[v], v, true)
888 else if opt_in_temporary(v) then
889 let {var bool: rp}
890 in (temp_is_real_reif(p,rp)) /\
891 (temp_member_reif(temp_uses[v], v, rp))
892 else
893 temp_member_reif(temp_uses[v], v, a[operand_definer[p]])
894 endif endif
895 )
896 )
897 );
898
899%% Model::post_connected_users_constraints
900constraint
901 redundant_constraint(
902 forall(p in 0..MAXP where not operand_use[p])(
903 let {int: v = single_temp(p)} in (
904 if temp_must_be_real(p) then
905 member([rt[p] | p in temp_uses[v]], r[v])
906 else
907 member([rt[p] | p in temp_uses[v]]++[-1], r[v])
908 endif
909 )
910 )
911 );
912
913%% disjoint live ranges projected on callee-saved regs
914constraint
915 redundant_constraint(
916 forall(T in bb_temps) (
917 cumulative([ls[v] | v in T],
918 [ld[v] | v in T],
919 [temp_width[v]*bool2int(r[v] in calleesaved) | v in T],
920 card(calleesaved))
921 )
922 );
923
924%% temp symmetry breaking among interchangeable temporaries in their potential use operands
925constraint
926 symmetry_breaking_constraint(
927 forall(j in index_set(domop_operands)) (
928 value_precede_chain(domop_temps[j], [t(o) | o in domop_operands[j]])
929 )
930 );
931
932%% before
933constraint
934 redundant_constraint(
935 forall(j in index_set(before_pred)) (
936 let {int: p = before_pred[j],
937 int: q = before_succ[j],
938 expr: bc = before_cond[j]} in (
939 eval_expr(bc) -> operand_live_before(p,q)
940 )
941 )
942 );
943
944%% active_table, tmp_table
945constraint
946 redundant_constraint(
947 forall(E in table_exists_ops) (
948 exists(j in E)(a[j])
949 )
950 );
951
952constraint
953 redundant_constraint(
954 forall(XOR in table_iffall_ops) (
955 let {int: j = min(XOR),
956 int: k = max(XOR)} in (
957 a[j] <-> a[k]
958 )
959 )
960 );
961
962constraint
963 redundant_constraint(
964 forall(j in index_set(relation_ops)) (
965 let{set of int: ops = relation_ops[j],
966 set of int: temps = relation_temps[j],
967 int: nt = relation_ntuples[j],
968 set of int: range = relation_range[j],
969 set of int: irange = 1..(card(ops)+card(temps)),
970 array[irange] of var int: vars = [bool2int(a[j]) | j in ops]++
971 [t(j) | j in temps]} in (
972 table(vars, array2d(1..nt,irange,[ints[j] | j in range]))
973 )
974 )
975 );
976
977%% combine
978constraint
979 redundant_constraint(
980 forall(o in 0..MAXO where op_type[o] = TYPE_COMBINE)(
981 let {array[int] of int: opnds = [x | x in op_operands[o]],
982 int: src1 = opnds[1],
983 int: src2 = opnds[2],
984 int: def = opnds[3]} in (
985 minimum(ls_t(def), [le_t(src1), le_t(def)]) /\
986 minimum(ls_t(def), [le_t(src2), le_t(def)])
987 )
988 )
989 );
990
991%% low/high
992constraint
993 redundant_constraint(
994 forall(o in 0..MAXO where op_type[o] in {TYPE_HIGH, TYPE_LOW})(
995 let {int: src = min(op_operands[o]),
996 int: def = max(op_operands[o])} in (
997 minimum(ls_t(def), [le_t(src), le_t(def)])
998 )
999 )
1000 );
1001
1002%% useless memory stores
1003constraint
1004 symmetry_breaking_constraint(
1005 forall(T in related_temps) (
1006 sum([bool2int(r[v] in infinite) | v in T]) <= 1
1007 )
1008 );
1009
1010%% across
1011constraint
1012 redundant_constraint(
1013 forall(j in index_set(across_op)) (
1014 let {int: opi = across_op[j],
1015 int: maxwidth = max(temp_width),
1016 set of int: regs = across_regs[j],
1017 set of int: items = across_items[j],
1018 array[items] of int: cand =
1019 array1d(items, [across_item_temp[k] | k in items]),
1020 array[items] of var bool: active,
1021 array[items] of var -maxwidth*(MAXT+1)..MAXR: selected,
1022 array[int] of var int: allreg =
1023 [x | x in callersaved] ++ [x | x in regs] ++ selected,
1024 array[int] of int: allwidth =
1025 [1 | x in callersaved] ++
1026 [1 | x in regs] ++
1027 [temp_width[cand[k]] | k in items]} in (
1028 forall(k in items)(
1029 let {int: ck = cand[k]} in (
1030 ( active[k] <->
1031 eval_expr(across_item_cond[k]) \/
1032 (ls[ck] <= c[opi] /\ c[opi] < le[ck])) /\
1033 selected[k] = ite(active[k], r[ck], -maxwidth*(ck+1))
1034 )
1035 ) /\
1036 noverlap(allreg, allwidth)
1037 )
1038 )
1039 );
1040
1041%% set_across
1042constraint
1043 redundant_constraint(
1044 forall(j in index_set(setacross_op)) (
1045 let {int: opi = setacross_op[j],
1046 set of int: regs = setacross_regs[j],
1047 set of int: itemsset = setacross_tempsets[j],
1048 set of int: items = 1..card(itemsset),
1049 array[items] of set of int: cands = [sets[it] | it in itemsset],
1050 array[items] of var 0..MAXR: selected,
1051 array[items] of var 0..max(temp_width): width,
1052 array[int] of var int: allreg =
1053 [x | x in callersaved] ++ [x | x in regs] ++ selected,
1054 array[int] of var int: allwidth =
1055 [1 | x in callersaved] ++ [1 | x in regs] ++ width} in (
1056 forall(it in items)(
1057 let {set of int: cit = cands[it],
1058 array[int] of int: ws = [temp_width[k] | k in cit],
1059 array[int] of var int: rs = [r[k] | k in cit],
1060 array[int] of var int: lss = [ls[k] | k in cit],
1061 array[int] of var int: les = [le[k] | k in cit],
1062 var 1..card(cit): k} in (
1063 width[it] = if min(ws) < max(ws) then ws[k] else min(ws) endif /\
1064 selected[it] = rs[k] /\
1065 lss[k] <= c[opi] /\ c[opi] < les[k]
1066 )
1067 ) /\
1068 noverlap(allreg, allwidth)
1069 )
1070 )
1071 );
1072
1073%% spill callee-saved if and only if some temp interfers with it
1074constraint
1075 symmetry_breaking_constraint(
1076 if card(index_set(calleesaved_spill))>0 then
1077 let {int: nrows = card(index_set_1of2(cs_spill_transpose)),
1078 int: ncols = card(index_set_2of2(cs_spill_transpose)),
1079 set of int: css_ops = {cs_spill_transpose[j,k] | j in 1..nrows, k in 1..ncols},
1080 set of int: preass_ops = {o | o in 0..MAXO where op_type[o] in {TYPE_IN,TYPE_CALL,TYPE_TAIL,TYPE_FUN}},
1081 set of int: tcands = {o | o in 0..MAXT where not (temp_definer[o] in css_ops union preass_ops)}} in (
1082 forall(j in 1..ncols) (
1083 let {int: theop = cs_spill_transpose[1,j],
1084 int: thepu = min(op_operands[theop]),
1085 int: thetu = single_temp(thepu),
1086 int: thepd = temp_def[thetu],
1087 int: thea = min(k in index_set(preassign_reg) where preassign_operand[k]=thepd)(preassign_reg[k]),
1088 int: thew = temp_width[thetu]} in (
1089 a[theop] <-> exists(ti in tcands)(r[ti]+temp_width[ti] > thea /\ r[ti] in 0..thea+thew-1)
1090 )
1091 )
1092 )
1093 else true endif
1094 );
1095
1096%% break symmetries among which callee-saved to spill
1097constraint
1098 symmetry_breaking_constraint(
1099 if card(index_set(calleesaved_spill))>0 then
1100 forall(j in index_set(calleesaved_spill)) (
1101 let {set of int: cgr = calleesaved_spill[j],
1102 int: cur = min(cgr)} in (
1103 forall(x in cgr where x>cur) (a[cur] <-> a[x])
1104 )
1105 ) /\
1106 let {int: nrows = card(index_set_1of2(cs_spill_transpose)),
1107 int: ncols = card(index_set_2of2(cs_spill_transpose)),
1108 set of int: spill = if nrows>=1 then {cs_spill_transpose[1,j] | j in 1..ncols}
1109 else {} endif,
1110 set of int: unspill = if nrows>=2 then {cs_spill_transpose[2,j] | j in 1..ncols}
1111 else {} endif} in (
1112 decreasing([a[cs_spill_transpose[1,k]] | k in 1..ncols]) /\
1113 forall(k in 2..ncols)(
1114 a[cs_spill_transpose[1,k]] -> c[cs_spill_transpose[1,k-1]] <= c[cs_spill_transpose[1,k]]
1115 ) /\
1116 if spill subset bb_ops[1] /\ unspill subset bb_ops[1] then
1117 forall(k in 1..ncols)(
1118 let {int: u = cs_spill_transpose[2,k],
1119 int: v = cs_spill_transpose[1,k]} in (
1120 a[u] -> c[v] < c[u]
1121 )
1122 )
1123 else true endif
1124 )
1125 else true endif
1126 );
1127
1128%% IMPORTED FROM Model::
1129
1130%% Model::post_minimum_temporary_duration_constraints
1131constraint
1132 redundant_constraint(
1133 forall(o in 0..MAXO, dp in op_operands[o] where not operand_use[dp])(
1134 let {int: v = single_temp(dp)} in
1135 (temp_eq(dp,v) -> ld[v] >= temp_minlive[v]) /\
1136 forall(up in temp_uses[v])(temp_eq(up,v) -> ld[v] >= lat(up,v))
1137 )
1138 );
1139
1140%% Model::post_define_issue_cycle_constraints
1141constraint
1142 symmetry_breaking_constraint(
1143 forall(o in 0..MAXO where op_type[o]=TYPE_DEFINE)(
1144 let {set of int: js = {operand_definer[q] | p in op_operands[o],
1145 v in {single_temp(p)},
1146 q in temp_uses[v]},
1147 array[int] of var int: lats = [lat(q,v) | p in op_operands[o],
1148 v in {single_temp(p)},
1149 q in temp_uses[v]]} in
1150 if card(js) = 1 then
1151 c[min(js)] = c[o] + max(lats)
1152 else true endif
1153 )
1154 );
1155
1156%% DOMINATION: live range of temp occurring in (kill)
1157predicate kill_live_range(int: v) =
1158 (ld[v] = lt[temp_def[v]]);
1159
1160%% Model::post_kill_issue_cycle_constraints
1161constraint
1162 symmetry_breaking_constraint(
1163 forall(o2 in 0..MAXO where op_type[o2] = TYPE_KILL)(
1164 if op_mand[o2] then % e.g. after function call, multiple operands
1165 let {array[int] of var int: lats = [lat(q,v) | q in op_operands[o2],
1166 v in {single_temp(q)}],
1167 array[int] of int: ts = [v | q in op_operands[o2],
1168 v in {single_temp(q)}],
1169 set of int: o1s = {temp_definer[v] | q in op_operands[o2],
1170 v in {single_temp(q)}},
1171 } in
1172 forall(v in ts)(kill_live_range(v)) /\
1173 c[o2] = c[min(o1s)] + max(lats)
1174 else % e.g. after move subject to pack, one operand, multiple temps
1175 let {int: q1 = min(op_operands[o2]),
1176 int: p1 = temp_def[single_temp(q1)],
1177 set of int: o1s = {temp_definer[v] | v in real_temps(q1)},
1178 array[int] of var int: issue = [-1] ++ [c[temp_definer[v]] + lat(q1,v) | v in real_temps(q1)],
1179 } in
1180 card(op_operands[o2]) = 1 /\ % sanity check
1181 forall(v in real_temps(q1))(kill_live_range(v)) /\
1182 c[o2] = issue[y[q1]] /\
1183 if card(real_temps(q1))=1 then
1184 same_temp(p1,q1) /\ rt[p1] = rt[q1]
1185 else
1186 sum(o in o1s)(a[o]) <= 1
1187 endif
1188 endif
1189 )
1190 );
1191
1192%% domination constraint for slack, in fact make it a functional dependency
1193constraint
1194 symmetry_breaking_constraint(
1195 forall(j in index_set_1of2(long_latency_index))(
1196 let {set of int: inps = long_latency_index[j,1],
1197 set of int: inix = long_latency_index[j,2],
1198 set of int: outps = long_latency_index[j,3],
1199 set of int: outix = long_latency_index[j,4],
1200 array[int] of var int: inubs = [ if temp_eq(q,single_temp(p)) then
1201 c[operand_definer[q]] - lt[q] - s[q] - lt[p]
1202 else MAXL endif
1203 | i in inix,
1204 p in [long_latency_def[i]],
1205 q in [long_latency_use[i]]
1206 ],
1207 array[int] of var int: outubs = [ if temp_eq(q,single_temp(p)) then
1208 ld[single_temp(p)] - lt[q] - lt[p] - s[p]
1209 else MAXL endif
1210 | i in outix,
1211 p in [long_latency_def[i]],
1212 q in [long_latency_use[i]]
1213 ]} in
1214 assert((card(inps)>0 /\ card(outps)>0), "invalid long_latency item") /\
1215 let {var int: outlb = if length( inubs)>0 then -min( inubs) else -MAXL endif,
1216 var int: outub = if length(outubs)>0 then min(outubs) else MAXL endif} in
1217 outlb <= outub /\
1218 forall(p in outps)(s[p] = min(outub,max(outlb,0)))
1219 )
1220 );
1221
1222%% domination constraint: sequential schedule as a makespan UB
1223%% Model::post_sequential_upper_bound_constraints
1224constraint
1225 symmetry_breaking_constraint(
1226 forall(bb in index_set(bb_ops))(
1227 let {set of int: os = bb_ops[bb],
1228 array[os] of var 0..MAXC: wc = array1d(os, [o_wcet(o) | o in os])}
1229 in c[max(os)] <= sum(o in os)(wc[o])
1230 )
1231 );
1232
1233var 0..MAXC: o_wcet(0..MAXO: o) =
1234 let {array[int] of var int: wcs = [wcet[jj,3] | jj in index_set_1of2(wcet) where wcet[jj,1] = o],
1235 int: nwcs = length(wcs)}
1236 in if forall(jj in 1..nwcs)(wcs[jj] = 1)
1237 then a[o]
1238 else if not op_mand[o] /\ forall(jj in 2..nwcs)(wcs[jj] = 1)
1239 then a[o]
1240 else
1241 wcs[ii[o]]
1242 endif endif;
1243
1244%% output
1245
1246%------------------------------------------------------------------------------
1247% Solve item
1248
1249solve
1250 :: seq_search([
1251 seq_search([
1252 int_search(
1253 [y[p] | p in bb_operands[b] where operand_use[p] /\ op_mand[operand_definer[p]]],
1254 first_fail, indomain_min, complete
1255 )
1256 ] ++ [
1257 int_search(
1258 [0] ++ [y[p] | p in bb_operands[b] where operand_use[p] /\ not op_mand[operand_definer[p]]],
1259 first_fail, indomain_min, complete
1260 )
1261 ])
1262 | b in bb_order
1263 ] ++ [
1264 int_search([ii[o] | o in bb_ops[b]], input_order, indomain_min, complete)
1265 | b in bb_order
1266 ] ++ [
1267 seq_search([
1268 int_search([c[max(bb_ops[b])]], input_order, indomain_min, complete),
1269 int_search([c[o] | o in bb_ops[b]], smallest, indomain_min, complete)
1270 ])
1271 | b in bb_order
1272 ] ++ [
1273 int_search(
1274 [r[t] | t in bb_temps[b] where op_type[temp_definer[t]] != TYPE_IN]++[0],
1275 first_fail, indomain_min, complete
1276 )
1277 | b in bb_order
1278 ])
1279 minimize objective;
1280
1281%------------------------------------------------------------------------------
1282% Output item
1283
1284output [
1285 "c = array1d(0..\(MAXO), \(c));\n",
1286 "ii = array1d(0..\(MAXO), \(ii));\n",
1287 "y = array1d(0..\(MAXP), \(y));\n",
1288 "r = array1d(-1..\(MAXT), \(r));\n",
1289 "objective = \(objective);\n"
1290];
1291%++
1292% ["\"cost\": "] ++ [show(objective)] ++ ["\n"] ++
1293% ["\"cycles\": "] ++ [show(c)] ++ ["\n"] ++
1294% ["\"instructions\": "] ++ [show([op_instructions[o][fix(ii[o])] | o in 0..MAXO])] ++ ["\n"] ++
1295% ["\"temporaries\": "] ++ [show([operand_temps[p][fix(y[p])] | p in 0..MAXP])] ++ ["\n"] ++
1296% ["\"registers\": "] ++ [show([r[v] | v in 0..MAXT])] ++ ["\n"] ++
1297% ["\"live start\": "] ++ [show([ls[v] | v in 0..MAXT])] ++ ["\n"] ++
1298% ["\"live duration\": "] ++ [show([ld[v] | v in 0..MAXT])] ++ ["\n"] ++
1299% ["\"live end\": "] ++ [show([le[v] | v in 0..MAXT])] ++ ["\n"];
1300