1114 lines
19 KiB
Plaintext
1114 lines
19 KiB
Plaintext
int: n:: global_register(1);
|
|
int: m:: global_register(0);
|
|
array [int,int] of int: Intensity:: global_register(2);
|
|
predicate solve_this(int: mode,var int: objective,array [int] of var int: x,int: varsel,int: valsel);
|
|
predicate int_lin_le(array [int] of int: as,array [int] of var int: bs,int: c);
|
|
predicate int_plus(var int: a,var int: b,var int: c);
|
|
predicate int_max(var int: a,var int: b,var int: c);
|
|
predicate int_minus(var int: x,var int: y,var int: z);
|
|
predicate int_sum(array [int] of var int: xs,var int: x);
|
|
predicate int_times(var int: a,var int: b,var int: c);
|
|
predicate array_int_minimum(var int: m,array [int] of var int: x);
|
|
predicate int_min(var int: a,var int: b,var int: c);
|
|
predicate output_this(array [int] of var int: arr);
|
|
predicate array_int_maximum(var int: m,array [int] of var int: x);
|
|
predicate int_lin_eq(array [int] of int: as,array [int] of var int: bs,int: c);
|
|
predicate clause(array [$T] of var bool: x,array [$T] of var bool: y);
|
|
predicate clause(array [$T] of bool: x,array [$T] of bool: y);
|
|
predicate bool_clause(array [int] of var bool: as,array [int] of var bool: bs);
|
|
predicate bool_not(var bool: a,var bool: b);
|
|
@@@@@@@@@@
|
|
:mk_intvar: 1
|
|
:absent: 1
|
|
:infinity: 1
|
|
:boolean_domain: 0
|
|
:infinite_domain: 0
|
|
:uniform: 2
|
|
:sol: 1
|
|
:sort_by: 2
|
|
:floor: 1
|
|
:ceil: 1
|
|
:slice_Xd: 3
|
|
:array_Xd: 2
|
|
:index_set: 2
|
|
:internal_sort: 1
|
|
:f_op_not_b:FUN 1
|
|
NOT R0 R1
|
|
PUSH R1
|
|
RET
|
|
:f_op_not_vb:FUN 1
|
|
OPEN_AGGREGATION OTHER
|
|
BUILTIN boolean_domain
|
|
POP R1
|
|
CALL ROOT mk_intvar 0 R1
|
|
POP R2
|
|
CALL ROOT bool_not 1 R0 R2
|
|
PUSH R2
|
|
CLEAR R1 R2
|
|
CLOSE_AGGREGATION
|
|
POP R1
|
|
PUSH R1
|
|
RET
|
|
:d_op_not_b:FUN 1
|
|
ISPAR R0 R1
|
|
JMPIF R1 l0
|
|
JMP l1
|
|
l0: TCALL FUN f_op_not_b 0
|
|
l1: TCALL FUN f_op_not_vb 1
|
|
:bool_clause:ROOT 2
|
|
:bool_clause_reif:ROOT 3
|
|
CALL FUN d_op_not_b 0 R2
|
|
POP R3
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R3
|
|
CLOSE_AGGREGATION
|
|
POP R4
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R1 l178
|
|
l177: ITER_NEXT R6
|
|
PUSH R6
|
|
JMP l177
|
|
l178: ITER_ARRAY R4 l180
|
|
l179: ITER_NEXT R7
|
|
PUSH R7
|
|
JMP l179
|
|
l180: CLEAR R6 R7
|
|
CLOSE_AGGREGATION
|
|
POP R5
|
|
IMMI 1 R6
|
|
BUILTIN index_set R0 R6
|
|
POP R7
|
|
ITER_ARRAY R7 l182
|
|
l181: ITER_NEXT R8
|
|
ITER_NEXT R9
|
|
ITER_RANGE R8 R9 l184
|
|
l183: ITER_NEXT R10
|
|
GET_ARRAY 1 R0 R10 R11 R12
|
|
OPEN_AGGREGATION OR
|
|
IMMI 0 R14
|
|
JMPIFNOT R12 l185
|
|
MOV R11 R14
|
|
l185: PUSH R14
|
|
PUSH R3
|
|
CLEAR R14 R14
|
|
CLOSE_AGGREGATION
|
|
POP R13
|
|
POST R13
|
|
JMP l183
|
|
l184: JMP l181
|
|
l182: IMMI 1 R14
|
|
BUILTIN index_set R1 R14
|
|
POP R15
|
|
ITER_ARRAY R15 l187
|
|
l186: ITER_NEXT R16
|
|
ITER_NEXT R17
|
|
ITER_RANGE R16 R17 l189
|
|
l188: ITER_NEXT R18
|
|
GET_ARRAY 1 R1 R18 R19 R20
|
|
IMMI 1 R21
|
|
NOT R20 R22
|
|
JMPIF R22 l190
|
|
OPEN_AGGREGATION OR
|
|
CALL FUN d_op_not_b 0 R19
|
|
POP R23
|
|
PUSH R23
|
|
PUSH R3
|
|
CLEAR R23 R23
|
|
CLOSE_AGGREGATION
|
|
POP R21
|
|
l190: POST R21
|
|
JMP l188
|
|
l189: JMP l186
|
|
l187: CALL ROOT d_clause_d1b_d1b 1 R0 R5
|
|
RET
|
|
:int_lin_eq:ROOT 3
|
|
:f_max_dTi:FUN 1
|
|
IMMI 0 R2
|
|
BUILTIN array_Xd R0 R2
|
|
POP R1
|
|
BUILTIN infinity R2
|
|
POP R3
|
|
ITER_ARRAY R1 l176
|
|
l175: ITER_NEXT R5
|
|
LTI R3 R5 R4
|
|
JMPIFNOT R4 l174
|
|
MOV R5 R3
|
|
l174: JMP l175
|
|
l176: PUSH R3
|
|
RET
|
|
:f_max_dTvi:FUN 1
|
|
IMMI 0 R2
|
|
BUILTIN array_Xd R0 R2
|
|
POP R1
|
|
LENGTH R0 R3
|
|
IMMI 1 R4
|
|
LEI R4 R3 R5
|
|
CALL FUN f_max_t_d1vi 1 R1
|
|
POP R6
|
|
PUSH R6
|
|
RET
|
|
:d_max_d1i:FUN 1
|
|
ISPAR R0 R1
|
|
JMPIF R1 l20
|
|
JMP l21
|
|
l20: TCALL FUN f_max_dTi 0
|
|
l21: TCALL FUN f_max_dTvi 1
|
|
:output_this:ROOT 1
|
|
:f_lex_obj_i:ROOT 1
|
|
LOAD_GLOBAL 6 R1
|
|
LOAD_GLOBAL 7 R2
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R1
|
|
PUSH R2
|
|
CLOSE_AGGREGATION
|
|
POP R3
|
|
CALL ROOT f_lex_minimize_d1vi_i 1 R3 R0
|
|
RET
|
|
:f_op_times_i_i:FUN 2
|
|
MULI R0 R1 R2
|
|
PUSH R2
|
|
RET
|
|
:f_op_times_i_vi:FUN 2
|
|
IMMI 1 R2
|
|
IMMI 1 R4
|
|
EQI R0 R2 R5
|
|
JMPIFNOT R5 l138
|
|
IMMI 0 R4
|
|
MOV R1 R3
|
|
JMP l137
|
|
l138: OPEN_AGGREGATION OTHER
|
|
BUILTIN infinite_domain
|
|
POP R6
|
|
CALL ROOT mk_intvar 0 R6
|
|
POP R7
|
|
CALL ROOT int_times 1 R0 R1 R7
|
|
PUSH R7
|
|
CLEAR R6 R7
|
|
CLOSE_AGGREGATION
|
|
POP R6
|
|
IMMI 0 R4
|
|
MOV R6 R3
|
|
l137: PUSH R3
|
|
RET
|
|
:f_op_times_vi_i:FUN 2
|
|
CALL FUN d_op_times_i_i 0 R1 R0
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:f_op_times_vi_vi:FUN 2
|
|
OPEN_AGGREGATION OTHER
|
|
BUILTIN infinite_domain
|
|
POP R2
|
|
CALL ROOT mk_intvar 0 R2
|
|
POP R3
|
|
CALL ROOT int_times 1 R0 R1 R3
|
|
PUSH R3
|
|
CLEAR R2 R3
|
|
CLOSE_AGGREGATION
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:d_op_times_i_i:FUN 2
|
|
ISPAR R0 R2
|
|
JMPIF R2 l42
|
|
JMP l43
|
|
l42: ISPAR R1 R2
|
|
JMPIF R2 l44
|
|
JMP l45
|
|
l43: ISPAR R1 R2
|
|
JMPIF R2 l46
|
|
JMP l47
|
|
l44: TCALL FUN f_op_times_i_i 0
|
|
l45: TCALL FUN f_op_times_i_vi 1
|
|
l46: TCALL FUN f_op_times_vi_i 1
|
|
l47: TCALL FUN f_op_times_vi_vi 1
|
|
:f_sum_cc_dTvi:FUN 1
|
|
OPEN_AGGREGATION OTHER
|
|
IMMI 0 R2
|
|
BUILTIN array_Xd R0 R2
|
|
POP R1
|
|
BUILTIN infinite_domain
|
|
POP R3
|
|
CALL ROOT mk_intvar 0 R3
|
|
POP R4
|
|
CALL ROOT int_sum 1 R1 R4
|
|
PUSH R4
|
|
CLEAR R1 R4
|
|
CLOSE_AGGREGATION
|
|
POP R1
|
|
PUSH R1
|
|
RET
|
|
:f_pre_int_lin_eq_d1i_d1vi_i:ROOT 3
|
|
LENGTH R0 R4
|
|
IMMI 0 R5
|
|
EQI R4 R5 R6
|
|
JMPIFNOT R6 l136
|
|
EQI R2 R5 R7
|
|
MOV R7 R3
|
|
JMP l135
|
|
l136: CALL ROOT int_lin_eq 1 R0 R1 R2
|
|
IMMI 1 R8
|
|
MOV R8 R3
|
|
l135: POST R3
|
|
RET
|
|
:f_upper_bound_on_increments_vi_d1vi:ROOT 2
|
|
IMMI 1 R2
|
|
GET_ARRAY 1 R1 R2 R3 R4
|
|
IMMI 2 R5
|
|
LOAD_GLOBAL 1 R6
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R5
|
|
PUSH R6
|
|
CLOSE_AGGREGATION
|
|
POP R7
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R7 l106
|
|
l105: ITER_NEXT R8
|
|
ITER_NEXT R9
|
|
ITER_RANGE R8 R9 l108
|
|
l107: ITER_NEXT R10
|
|
GET_ARRAY 1 R1 R10 R11 R12
|
|
SUBI R10 R2 R13
|
|
GET_ARRAY 1 R1 R13 R14 R15
|
|
CALL FUN d_op_minus_i_i 1 R11 R14
|
|
POP R16
|
|
IMMI 0 R17
|
|
CALL FUN d_max_i_i 1 R16 R17
|
|
POP R18
|
|
PUSH R18
|
|
JMP l107
|
|
l108: JMP l105
|
|
l106: CLEAR R8 R18
|
|
CLOSE_AGGREGATION
|
|
POP R8
|
|
LENGTH R8 R9
|
|
JMPIFNOT R9 l118
|
|
EQI R2 R9 R10
|
|
JMPIF R10 l119
|
|
CALL FUN f_sum_cc_dTvi 1 R8
|
|
POP R10
|
|
JMP l120
|
|
l118: IMMI 0 R10
|
|
JMP l120
|
|
l119: GET_VEC R8 R2 R10
|
|
l120: CALL FUN d_op_plus_i_i 1 R3 R10
|
|
POP R11
|
|
LB R11 R12
|
|
UB R0 R13
|
|
LEI R12 R13 R12
|
|
SIMPLIFY_LIN R11 R0 0 R14 R15 R16
|
|
POST R4
|
|
POST R12
|
|
CALL ROOT f_pre_int_lin_le_d1i_d1vi_i 1 R14 R15 R16
|
|
RET
|
|
:solve_this:ROOT 5
|
|
:f_op_minus_i_i:FUN 2
|
|
SUBI R0 R1 R2
|
|
PUSH R2
|
|
RET
|
|
:f_op_minus_vi_i:FUN 2
|
|
IMMI 1 R2
|
|
IMMI 1 R4
|
|
IMMI 0 R5
|
|
EQI R1 R5 R6
|
|
JMPIFNOT R6 l134
|
|
IMMI 0 R4
|
|
MOV R0 R3
|
|
JMP l133
|
|
l134: OPEN_AGGREGATION OTHER
|
|
BUILTIN infinite_domain
|
|
POP R7
|
|
CALL ROOT mk_intvar 0 R7
|
|
POP R8
|
|
CALL ROOT int_minus 1 R0 R1 R8
|
|
PUSH R8
|
|
CLEAR R7 R8
|
|
CLOSE_AGGREGATION
|
|
POP R7
|
|
IMMI 0 R4
|
|
MOV R7 R3
|
|
l133: PUSH R3
|
|
RET
|
|
:f_op_minus_vi_vi:FUN 2
|
|
OPEN_AGGREGATION OTHER
|
|
BUILTIN infinite_domain
|
|
POP R2
|
|
CALL ROOT mk_intvar 0 R2
|
|
POP R3
|
|
CALL ROOT int_minus 1 R0 R1 R3
|
|
PUSH R3
|
|
CLEAR R2 R3
|
|
CLOSE_AGGREGATION
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:d_op_minus_i_i:FUN 2
|
|
ISPAR R0 R2
|
|
JMPIF R2 l109
|
|
JMP l110
|
|
l109: ISPAR R1 R2
|
|
JMPIF R2 l111
|
|
JMP l112
|
|
l110: ISPAR R1 R2
|
|
JMPIF R2 l113
|
|
JMP l112
|
|
l111: TCALL FUN f_op_minus_i_i 0
|
|
l112: TCALL FUN f_op_minus_vi_vi 1
|
|
l113: TCALL FUN f_op_minus_vi_i 1
|
|
:f_max_t_t:FUN 2
|
|
IMMI 1 R2
|
|
IMMI 1 R4
|
|
LTI R1 R0 R5
|
|
JMPIFNOT R5 l132
|
|
IMMI 0 R4
|
|
MOV R0 R3
|
|
JMP l131
|
|
l132: IMMI 0 R4
|
|
MOV R1 R3
|
|
l131: PUSH R3
|
|
RET
|
|
:f_max_vi_vi:FUN 2
|
|
OPEN_AGGREGATION OTHER
|
|
LB R0 R2
|
|
LB R1 R3
|
|
CALL FUN d_max_i_i 0 R2 R3
|
|
POP R4
|
|
UB R0 R5
|
|
UB R1 R6
|
|
CALL FUN d_max_i_i 0 R5 R6
|
|
POP R7
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R4
|
|
PUSH R7
|
|
CLOSE_AGGREGATION
|
|
POP R8
|
|
CALL ROOT mk_intvar 0 R8
|
|
POP R9
|
|
CALL ROOT int_max 1 R0 R1 R9
|
|
PUSH R9
|
|
CLEAR R2 R9
|
|
CLOSE_AGGREGATION
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:d_max_i_i:FUN 2
|
|
ISPAR R0 R2
|
|
JMPIF R2 l114
|
|
JMP l115
|
|
l114: ISPAR R1 R2
|
|
JMPIF R2 l116
|
|
JMP l117
|
|
l115: JMP l117
|
|
l116: TCALL FUN f_max_t_t 0
|
|
l117: TCALL FUN f_max_vi_vi 1
|
|
:f_op_plus_i_i:FUN 2
|
|
ADDI R0 R1 R2
|
|
PUSH R2
|
|
RET
|
|
:f_op_plus_i_vi:FUN 2
|
|
IMMI 1 R2
|
|
IMMI 1 R4
|
|
IMMI 0 R5
|
|
EQI R0 R5 R6
|
|
JMPIFNOT R6 l130
|
|
IMMI 0 R4
|
|
MOV R1 R3
|
|
JMP l129
|
|
l130: OPEN_AGGREGATION OTHER
|
|
BUILTIN infinite_domain
|
|
POP R7
|
|
CALL ROOT mk_intvar 0 R7
|
|
POP R8
|
|
CALL ROOT int_plus 1 R0 R1 R8
|
|
PUSH R8
|
|
CLEAR R7 R8
|
|
CLOSE_AGGREGATION
|
|
POP R7
|
|
IMMI 0 R4
|
|
MOV R7 R3
|
|
l129: PUSH R3
|
|
RET
|
|
:f_op_plus_vi_i:FUN 2
|
|
CALL FUN d_op_plus_i_i 0 R1 R0
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:f_op_plus_vi_vi:FUN 2
|
|
OPEN_AGGREGATION OTHER
|
|
BUILTIN infinite_domain
|
|
POP R2
|
|
CALL ROOT mk_intvar 0 R2
|
|
POP R3
|
|
CALL ROOT int_plus 1 R0 R1 R3
|
|
PUSH R3
|
|
CLEAR R2 R3
|
|
CLOSE_AGGREGATION
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:d_op_plus_i_i:FUN 2
|
|
ISPAR R0 R2
|
|
JMPIF R2 l121
|
|
JMP l122
|
|
l121: ISPAR R1 R2
|
|
JMPIF R2 l123
|
|
JMP l124
|
|
l122: ISPAR R1 R2
|
|
JMPIF R2 l125
|
|
JMP l126
|
|
l123: TCALL FUN f_op_plus_i_i 0
|
|
l124: TCALL FUN f_op_plus_i_vi 1
|
|
l125: TCALL FUN f_op_plus_vi_i 1
|
|
l126: TCALL FUN f_op_plus_vi_vi 1
|
|
:f_pre_int_lin_le_d1i_d1vi_i:ROOT 3
|
|
LENGTH R0 R4
|
|
IMMI 0 R5
|
|
EQI R4 R5 R6
|
|
JMPIFNOT R6 l128
|
|
LEI R5 R2 R7
|
|
MOV R7 R3
|
|
JMP l127
|
|
l128: CALL ROOT int_lin_le 1 R0 R1 R2
|
|
IMMI 1 R8
|
|
MOV R8 R3
|
|
l127: POST R3
|
|
RET
|
|
:int_lin_le:ROOT 3
|
|
:int_plus:ROOT 3
|
|
:int_max:ROOT 3
|
|
:int_minus:ROOT 3
|
|
:int_sum:ROOT 2
|
|
:int_times:ROOT 3
|
|
:f_lex_minimize_d1vi_i:ROOT 2
|
|
IMMI 1 R2
|
|
BUILTIN index_set R0 R2
|
|
POP R3
|
|
CALL FUN d_min_si 0 R3
|
|
POP R4
|
|
SUBI R1 R2 R5
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R4
|
|
PUSH R5
|
|
CLOSE_AGGREGATION
|
|
POP R6
|
|
ITER_ARRAY R6 l142
|
|
l141: ITER_NEXT R7
|
|
ITER_NEXT R8
|
|
ITER_RANGE R7 R8 l144
|
|
l143: ITER_NEXT R9
|
|
GET_ARRAY 1 R0 R9 R10 R11
|
|
BUILTIN sol R10
|
|
POP R12
|
|
DOM R10 R13
|
|
DOM R12 R14
|
|
INTERSECTION R13 R14 R13
|
|
ISEMPTY R13 R14
|
|
NOT R14 R14
|
|
SIMPLIFY_LIN R10 R12 0 R16 R17 R15
|
|
POST R11
|
|
POST R14
|
|
CALL ROOT f_pre_int_lin_eq_d1i_d1vi_i 1 R16 R17 R15
|
|
JMP l143
|
|
l144: JMP l141
|
|
l142: GET_ARRAY 1 R0 R1 R18 R19
|
|
BUILTIN sol R18
|
|
POP R20
|
|
LB R18 R21
|
|
UB R20 R22
|
|
LTI R21 R22 R21
|
|
SIMPLIFY_LIN R18 R20 1 R23 R24 R25
|
|
POST R19
|
|
POST R21
|
|
CALL ROOT f_pre_int_lin_le_d1i_d1vi_i 1 R23 R24 R25
|
|
RET
|
|
:f_min_si:FUN 1
|
|
LENGTH R0 R2
|
|
IMMI 1 R3
|
|
LEI R3 R2 R1
|
|
JMPIF R1 l162
|
|
ABORT
|
|
l162: GET_VEC R0 R3 R1
|
|
PUSH R1
|
|
RET
|
|
:f_min_dTvi:FUN 1
|
|
IMMI 0 R2
|
|
BUILTIN array_Xd R0 R2
|
|
POP R1
|
|
LENGTH R0 R3
|
|
IMMI 1 R4
|
|
LEI R4 R3 R5
|
|
CALL FUN f_min_t_d1vi 1 R1
|
|
POP R6
|
|
PUSH R6
|
|
RET
|
|
:d_min_si:FUN 1
|
|
ISPAR R0 R1
|
|
JMPIF R1 l139
|
|
JMP l140
|
|
l139: TCALL FUN f_min_si 0
|
|
l140: TCALL FUN f_min_dTvi 1
|
|
:f_min_t_d1vi:FUN 1
|
|
IMMI 1 R1
|
|
IMMI 1 R3
|
|
LENGTH R0 R4
|
|
IMMI 0 R5
|
|
EQI R4 R5 R6
|
|
JMPIFNOT R6 l146
|
|
IMMI 0 R3
|
|
MOV R5 R2
|
|
JMP l145
|
|
l146: EQI R4 R1 R7
|
|
JMPIFNOT R7 l147
|
|
GET_ARRAY 1 R0 R1 R8 R9
|
|
MOV R9 R3
|
|
MOV R8 R2
|
|
JMP l145
|
|
l147: IMMI 2 R10
|
|
EQI R4 R10 R11
|
|
JMPIFNOT R11 l148
|
|
GET_ARRAY 1 R0 R1 R12 R13
|
|
GET_ARRAY 1 R0 R10 R14 R15
|
|
CALL FUN d_min_i_i 1 R12 R14
|
|
POP R16
|
|
IMMI 0 R17
|
|
JMPIFNOT R13 l153
|
|
MOV R15 R17
|
|
l153: MOV R17 R3
|
|
MOV R16 R2
|
|
JMP l145
|
|
l148: OPEN_AGGREGATION OTHER
|
|
BUILTIN infinity R1
|
|
POP R18
|
|
ITER_ARRAY R0 l156
|
|
l155: ITER_NEXT R21
|
|
LB R21 R19
|
|
LTI R19 R18 R20
|
|
JMPIFNOT R20 l154
|
|
MOV R19 R18
|
|
l154: JMP l155
|
|
l156: BUILTIN infinity R5
|
|
POP R22
|
|
ITER_ARRAY R0 l159
|
|
l158: ITER_NEXT R25
|
|
UB R25 R23
|
|
LTI R22 R23 R24
|
|
JMPIFNOT R24 l157
|
|
MOV R23 R22
|
|
l157: JMP l158
|
|
l159: OPEN_AGGREGATION VEC
|
|
PUSH R18
|
|
PUSH R22
|
|
CLOSE_AGGREGATION
|
|
POP R26
|
|
CALL ROOT mk_intvar 0 R26
|
|
POP R27
|
|
CALL ROOT array_int_minimum 1 R27 R0
|
|
PUSH R27
|
|
CLEAR R18 R27
|
|
CLOSE_AGGREGATION
|
|
POP R18
|
|
IMMI 0 R3
|
|
MOV R18 R2
|
|
l145: PUSH R2
|
|
RET
|
|
:f_min_t_t:FUN 2
|
|
IMMI 1 R2
|
|
IMMI 1 R4
|
|
LTI R0 R1 R5
|
|
JMPIFNOT R5 l161
|
|
IMMI 0 R4
|
|
MOV R0 R3
|
|
JMP l160
|
|
l161: IMMI 0 R4
|
|
MOV R1 R3
|
|
l160: PUSH R3
|
|
RET
|
|
:f_min_vi_vi:FUN 2
|
|
OPEN_AGGREGATION OTHER
|
|
LB R0 R2
|
|
LB R1 R3
|
|
CALL FUN d_min_i_i 0 R2 R3
|
|
POP R4
|
|
UB R0 R5
|
|
UB R1 R6
|
|
CALL FUN d_min_i_i 0 R5 R6
|
|
POP R7
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R4
|
|
PUSH R7
|
|
CLOSE_AGGREGATION
|
|
POP R8
|
|
CALL ROOT mk_intvar 0 R8
|
|
POP R9
|
|
CALL ROOT int_min 1 R0 R1 R9
|
|
PUSH R9
|
|
CLEAR R2 R9
|
|
CLOSE_AGGREGATION
|
|
POP R2
|
|
PUSH R2
|
|
RET
|
|
:d_min_i_i:FUN 2
|
|
ISPAR R0 R2
|
|
JMPIF R2 l149
|
|
JMP l150
|
|
l149: ISPAR R1 R2
|
|
JMPIF R2 l151
|
|
JMP l152
|
|
l150: JMP l152
|
|
l151: TCALL FUN f_min_t_t 0
|
|
l152: TCALL FUN f_min_vi_vi 1
|
|
:array_int_minimum:ROOT 2
|
|
:int_min:ROOT 3
|
|
:f_max_t_d1vi:FUN 1
|
|
IMMI 1 R1
|
|
IMMI 1 R3
|
|
LENGTH R0 R4
|
|
IMMI 0 R5
|
|
EQI R4 R5 R6
|
|
JMPIFNOT R6 l164
|
|
IMMI 0 R3
|
|
MOV R5 R2
|
|
JMP l163
|
|
l164: EQI R4 R1 R7
|
|
JMPIFNOT R7 l165
|
|
BUILTIN index_set R0 R1
|
|
POP R8
|
|
CALL FUN d_min_si 0 R8
|
|
POP R9
|
|
GET_ARRAY 1 R0 R9 R10 R11
|
|
MOV R11 R3
|
|
MOV R10 R2
|
|
JMP l163
|
|
l165: IMMI 2 R12
|
|
EQI R4 R12 R13
|
|
JMPIFNOT R13 l166
|
|
GET_ARRAY 1 R0 R1 R14 R15
|
|
GET_ARRAY 1 R0 R12 R16 R17
|
|
CALL FUN d_max_i_i 0 R14 R16
|
|
POP R18
|
|
IMMI 0 R19
|
|
JMPIFNOT R15 l167
|
|
MOV R17 R19
|
|
l167: MOV R19 R3
|
|
MOV R18 R2
|
|
JMP l163
|
|
l166: OPEN_AGGREGATION OTHER
|
|
BUILTIN infinity R1
|
|
POP R20
|
|
ITER_ARRAY R0 l170
|
|
l169: ITER_NEXT R23
|
|
LB R23 R21
|
|
LTI R21 R20 R22
|
|
JMPIFNOT R22 l168
|
|
MOV R21 R20
|
|
l168: JMP l169
|
|
l170: BUILTIN infinity R5
|
|
POP R24
|
|
ITER_ARRAY R0 l173
|
|
l172: ITER_NEXT R27
|
|
UB R27 R25
|
|
LTI R24 R25 R26
|
|
JMPIFNOT R26 l171
|
|
MOV R25 R24
|
|
l171: JMP l172
|
|
l173: OPEN_AGGREGATION VEC
|
|
PUSH R20
|
|
PUSH R24
|
|
CLOSE_AGGREGATION
|
|
POP R28
|
|
CALL ROOT mk_intvar 0 R28
|
|
POP R29
|
|
CALL ROOT array_int_maximum 1 R29 R0
|
|
PUSH R29
|
|
CLEAR R20 R29
|
|
CLOSE_AGGREGATION
|
|
POP R20
|
|
IMMI 0 R3
|
|
MOV R20 R2
|
|
l163: PUSH R2
|
|
RET
|
|
:array_int_maximum:ROOT 2
|
|
:clause:ROOT 2
|
|
:clause:ROOT 2
|
|
:d_clause_d1b_d1b:ROOT 2
|
|
ISPAR R0 R2
|
|
JMPIF R2 l191
|
|
JMP l192
|
|
l191: ISPAR R1 R2
|
|
JMPIF R2 l193
|
|
JMP l194
|
|
l192: JMP l194
|
|
l193: TCALL ROOT clause 1
|
|
l194: TCALL ROOT clause 1
|
|
:bool_not:ROOT 2
|
|
:main:ROOT 0
|
|
OPEN_AGGREGATION OTHER
|
|
IMMI 1 R0
|
|
LOAD_GLOBAL 0 R1
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R0
|
|
PUSH R1
|
|
CLOSE_AGGREGATION
|
|
POP R2
|
|
STORE_GLOBAL R2 3
|
|
LOAD_GLOBAL 1 R3
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R0
|
|
PUSH R3
|
|
CLOSE_AGGREGATION
|
|
POP R4
|
|
STORE_GLOBAL R4 4
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R2 l3
|
|
l2: ITER_NEXT R5
|
|
ITER_NEXT R6
|
|
ITER_RANGE R5 R6 l5
|
|
l4: ITER_NEXT R7
|
|
ITER_ARRAY R4 l7
|
|
l6: ITER_NEXT R8
|
|
ITER_NEXT R9
|
|
ITER_RANGE R8 R9 l9
|
|
l8: ITER_NEXT R10
|
|
LOAD_GLOBAL 2 R11
|
|
GET_ARRAY 2 R11 R7 R10 R12 R13
|
|
PUSH R12
|
|
JMP l8
|
|
l9: JMP l6
|
|
l7: JMP l4
|
|
l5: JMP l2
|
|
l3: CLEAR R5 R13
|
|
CLOSE_AGGREGATION
|
|
POP R5
|
|
IMMI 0 R6
|
|
ITER_ARRAY R5 l11
|
|
l10: ITER_NEXT R7
|
|
ADDI R6 R7 R6
|
|
JMP l10
|
|
l11: STORE_GLOBAL R6 5
|
|
IMMI 0 R8
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R8
|
|
PUSH R6
|
|
CLOSE_AGGREGATION
|
|
POP R9
|
|
CALL ROOT mk_intvar 0 R9
|
|
POP R10
|
|
STORE_GLOBAL R10 6
|
|
MULI R1 R3 R11
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R8
|
|
PUSH R11
|
|
CLOSE_AGGREGATION
|
|
POP R12
|
|
CALL ROOT mk_intvar 0 R12
|
|
POP R13
|
|
STORE_GLOBAL R13 7
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R2 l13
|
|
l12: ITER_NEXT R14
|
|
ITER_NEXT R15
|
|
ITER_RANGE R14 R15 l15
|
|
l14: ITER_NEXT R16
|
|
ITER_ARRAY R4 l17
|
|
l16: ITER_NEXT R17
|
|
ITER_NEXT R18
|
|
ITER_RANGE R17 R18 l19
|
|
l18: ITER_NEXT R19
|
|
LOAD_GLOBAL 2 R20
|
|
GET_ARRAY 2 R20 R16 R19 R21 R22
|
|
PUSH R21
|
|
JMP l18
|
|
l19: JMP l16
|
|
l17: JMP l14
|
|
l15: JMP l12
|
|
l13: CLEAR R14 R22
|
|
CLOSE_AGGREGATION
|
|
POP R14
|
|
CALL FUN d_max_d1i 0 R14
|
|
POP R15
|
|
STORE_GLOBAL R15 8
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R0
|
|
PUSH R15
|
|
CLOSE_AGGREGATION
|
|
POP R16
|
|
STORE_GLOBAL R16 9
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R2 l23
|
|
l22: ITER_NEXT R19
|
|
ITER_NEXT R20
|
|
ITER_RANGE R19 R20 l25
|
|
l24: ITER_NEXT R21
|
|
ITER_ARRAY R4 l27
|
|
l26: ITER_NEXT R22
|
|
ITER_NEXT R23
|
|
ITER_RANGE R22 R23 l29
|
|
l28: ITER_NEXT R24
|
|
ITER_ARRAY R16 l31
|
|
l30: ITER_NEXT R25
|
|
ITER_NEXT R26
|
|
ITER_RANGE R25 R26 l33
|
|
l32: ITER_NEXT R27
|
|
CALL ROOT mk_intvar 0 R12
|
|
JMP l32
|
|
l33: JMP l30
|
|
l31: JMP l28
|
|
l29: JMP l26
|
|
l27: JMP l24
|
|
l25: JMP l22
|
|
l23: CLEAR R19 R27
|
|
CLOSE_AGGREGATION
|
|
POP R17
|
|
OPEN_AGGREGATION VEC
|
|
GET_VEC R2 R0 R18
|
|
PUSH R18
|
|
IMMI 2 R19
|
|
GET_VEC R2 R19 R18
|
|
PUSH R18
|
|
GET_VEC R4 R0 R18
|
|
PUSH R18
|
|
GET_VEC R4 R19 R18
|
|
PUSH R18
|
|
GET_VEC R16 R0 R18
|
|
PUSH R18
|
|
GET_VEC R16 R19 R18
|
|
PUSH R18
|
|
CLEAR R19 R19
|
|
CLOSE_AGGREGATION
|
|
POP R18
|
|
BUILTIN array_Xd R17 R18
|
|
POP R17
|
|
STORE_GLOBAL R17 10
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R16 l35
|
|
l34: ITER_NEXT R21
|
|
ITER_NEXT R22
|
|
ITER_RANGE R21 R22 l37
|
|
l36: ITER_NEXT R23
|
|
CALL ROOT mk_intvar 0 R12
|
|
JMP l36
|
|
l37: JMP l34
|
|
l35: CLEAR R21 R23
|
|
CLOSE_AGGREGATION
|
|
POP R19
|
|
OPEN_AGGREGATION VEC
|
|
GET_VEC R16 R0 R20
|
|
PUSH R20
|
|
IMMI 2 R21
|
|
GET_VEC R16 R21 R20
|
|
PUSH R20
|
|
CLEAR R21 R21
|
|
CLOSE_AGGREGATION
|
|
POP R20
|
|
BUILTIN array_Xd R19 R20
|
|
POP R19
|
|
STORE_GLOBAL R19 11
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R10
|
|
PUSH R13
|
|
CLOSE_AGGREGATION
|
|
POP R21
|
|
CALL ROOT output_this 1 R21
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R16 l39
|
|
l38: ITER_NEXT R22
|
|
ITER_NEXT R23
|
|
ITER_RANGE R22 R23 l41
|
|
l40: ITER_NEXT R24
|
|
GET_ARRAY 1 R19 R24 R25 R26
|
|
CALL FUN d_op_times_i_i 1 R24 R25
|
|
POP R27
|
|
PUSH R27
|
|
JMP l40
|
|
l41: JMP l38
|
|
l39: CLEAR R22 R27
|
|
CLOSE_AGGREGATION
|
|
POP R22
|
|
LENGTH R22 R23
|
|
JMPIFNOT R23 l48
|
|
EQI R0 R23 R24
|
|
JMPIF R24 l49
|
|
CALL FUN f_sum_cc_dTvi 1 R22
|
|
POP R24
|
|
JMP l50
|
|
l48: IMMI 0 R24
|
|
JMP l50
|
|
l49: GET_VEC R22 R0 R24
|
|
l50: DOM R10 R25
|
|
DOM R24 R26
|
|
INTERSECTION R25 R26 R25
|
|
ISEMPTY R25 R26
|
|
NOT R26 R26
|
|
SIMPLIFY_LIN R10 R24 0 R28 R29 R27
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R16 l52
|
|
l51: ITER_NEXT R30
|
|
ITER_NEXT R31
|
|
ITER_RANGE R30 R31 l54
|
|
l53: ITER_NEXT R32
|
|
GET_ARRAY 1 R19 R32 R33 R34
|
|
PUSH R33
|
|
JMP l53
|
|
l54: JMP l51
|
|
l52: CLEAR R30 R34
|
|
CLOSE_AGGREGATION
|
|
POP R30
|
|
LENGTH R30 R31
|
|
JMPIFNOT R31 l55
|
|
EQI R0 R31 R32
|
|
JMPIF R32 l56
|
|
CALL FUN f_sum_cc_dTvi 1 R30
|
|
POP R32
|
|
JMP l57
|
|
l55: IMMI 0 R32
|
|
JMP l57
|
|
l56: GET_VEC R30 R0 R32
|
|
l57: DOM R13 R33
|
|
DOM R32 R34
|
|
INTERSECTION R33 R34 R33
|
|
ISEMPTY R33 R34
|
|
NOT R34 R34
|
|
SIMPLIFY_LIN R13 R32 0 R36 R37 R35
|
|
ITER_ARRAY R2 l59
|
|
l58: ITER_NEXT R38
|
|
ITER_NEXT R39
|
|
ITER_RANGE R38 R39 l61
|
|
l60: ITER_NEXT R40
|
|
ITER_ARRAY R4 l63
|
|
l62: ITER_NEXT R41
|
|
ITER_NEXT R42
|
|
ITER_RANGE R41 R42 l65
|
|
l64: ITER_NEXT R43
|
|
LOAD_GLOBAL 2 R44
|
|
GET_ARRAY 2 R44 R40 R43 R45 R46
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R16 l67
|
|
l66: ITER_NEXT R47
|
|
ITER_NEXT R48
|
|
ITER_RANGE R47 R48 l69
|
|
l68: ITER_NEXT R49
|
|
GET_ARRAY 3 R17 R40 R43 R49 R50 R51
|
|
CALL FUN d_op_times_i_i 0 R49 R50
|
|
POP R52
|
|
PUSH R52
|
|
JMP l68
|
|
l69: JMP l66
|
|
l67: CLEAR R47 R52
|
|
CLOSE_AGGREGATION
|
|
POP R47
|
|
LENGTH R47 R48
|
|
JMPIFNOT R48 l70
|
|
EQI R0 R48 R49
|
|
JMPIF R49 l71
|
|
CALL FUN f_sum_cc_dTvi 1 R47
|
|
POP R49
|
|
JMP l72
|
|
l70: IMMI 0 R49
|
|
JMP l72
|
|
l71: GET_VEC R47 R0 R49
|
|
l72: DOM R45 R50
|
|
DOM R49 R51
|
|
INTERSECTION R50 R51 R50
|
|
ISEMPTY R50 R51
|
|
NOT R51 R51
|
|
SIMPLIFY_LIN R45 R49 0 R53 R54 R52
|
|
POST R46
|
|
POST R51
|
|
CALL ROOT f_pre_int_lin_eq_d1i_d1vi_i 1 R53 R54 R52
|
|
JMP l64
|
|
l65: JMP l62
|
|
l63: JMP l60
|
|
l61: JMP l58
|
|
l59: ITER_ARRAY R2 l74
|
|
l73: ITER_NEXT R55
|
|
ITER_NEXT R56
|
|
ITER_RANGE R55 R56 l76
|
|
l75: ITER_NEXT R57
|
|
ITER_ARRAY R16 l78
|
|
l77: ITER_NEXT R58
|
|
ITER_NEXT R59
|
|
ITER_RANGE R58 R59 l80
|
|
l79: ITER_NEXT R60
|
|
GET_ARRAY 1 R19 R60 R61 R62
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R4 l82
|
|
l81: ITER_NEXT R63
|
|
ITER_NEXT R64
|
|
ITER_RANGE R63 R64 l84
|
|
l83: ITER_NEXT R65
|
|
GET_ARRAY 3 R17 R57 R65 R60 R66 R67
|
|
PUSH R66
|
|
JMP l83
|
|
l84: JMP l81
|
|
l82: CLEAR R63 R67
|
|
CLOSE_AGGREGATION
|
|
POP R63
|
|
POST R62
|
|
CALL ROOT f_upper_bound_on_increments_vi_d1vi 1 R61 R63
|
|
JMP l79
|
|
l80: JMP l77
|
|
l78: JMP l75
|
|
l76: JMP l73
|
|
l74: POST R26
|
|
CALL ROOT f_pre_int_lin_eq_d1i_d1vi_i 1 R28 R29 R27
|
|
POST R34
|
|
CALL ROOT f_pre_int_lin_eq_d1i_d1vi_i 1 R36 R37 R35
|
|
OPEN_AGGREGATION VEC
|
|
PUSH R10
|
|
CLOSE_AGGREGATION
|
|
POP R64
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R64 l86
|
|
l85: ITER_NEXT R66
|
|
PUSH R66
|
|
JMP l85
|
|
l86: ITER_ARRAY R19 l88
|
|
l87: ITER_NEXT R67
|
|
PUSH R67
|
|
JMP l87
|
|
l88: CLEAR R66 R67
|
|
CLOSE_AGGREGATION
|
|
POP R65
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R2 l90
|
|
l89: ITER_NEXT R66
|
|
ITER_NEXT R67
|
|
ITER_RANGE R66 R67 l92
|
|
l91: ITER_NEXT R68
|
|
ITER_ARRAY R4 l94
|
|
l93: ITER_NEXT R69
|
|
ITER_NEXT R70
|
|
ITER_RANGE R69 R70 l96
|
|
l95: ITER_NEXT R71
|
|
ITER_ARRAY R16 l98
|
|
l97: ITER_NEXT R72
|
|
ITER_NEXT R73
|
|
ITER_RANGE R72 R73 l100
|
|
l99: ITER_NEXT R74
|
|
GET_ARRAY 3 R17 R68 R71 R74 R75 R76
|
|
PUSH R75
|
|
JMP l99
|
|
l100: JMP l97
|
|
l98: JMP l95
|
|
l96: JMP l93
|
|
l94: JMP l91
|
|
l92: JMP l89
|
|
l90: CLEAR R66 R76
|
|
CLOSE_AGGREGATION
|
|
POP R66
|
|
OPEN_AGGREGATION VEC
|
|
ITER_ARRAY R65 l102
|
|
l101: ITER_NEXT R68
|
|
PUSH R68
|
|
JMP l101
|
|
l102: ITER_ARRAY R66 l104
|
|
l103: ITER_NEXT R69
|
|
PUSH R69
|
|
JMP l103
|
|
l104: CLEAR R68 R69
|
|
CLOSE_AGGREGATION
|
|
POP R67
|
|
CALL ROOT solve_this 1 R8 R8 R67 R0 R0
|
|
CLEAR R0 R67
|
|
RET
|