1%-----------------------------------------------------------------------------% 2% Requires that the array 'x' is strictly lexicographically less than array 'y'. 3% Compares them from first to last element, regardless of indices 4%-----------------------------------------------------------------------------% 5 6predicate fzn_lex_less_int(array[int] of var int: x, 7 array[int] of var int: y) = 8 assert(length(x) == length(y), 9 "lex_less_int(\(x), \(y)): arrays of different lengths") 10 /\ 11 fzn_lex_less_int__MIP(x, y) 12 ; 13 14predicate fzn_lex_less_int__MIP(array[int] of var int: x, 15 array[int] of var int: y) = 16 let { int: lx = min(index_set(x)), 17 int: ux = max(index_set(x)), 18 int: ly = min(index_set(y)), 19 int: uy = max(index_set(y)), 20 int: size = min(ux - lx, uy - ly), 21 array[0..size] of var 0..1: fEQ; 22 array[0..size] of var 0..1: fLT; 23 } in 24 sum(fLT) == 1 25 /\ 26 fEQ[0] + fLT[0] == 1 27 /\ 28 forall(i in 1..size) ( 29 fEQ[i-1] == fEQ[i] + fLT[i] 30 ) 31 /\ 32 forall(i in 0..size) ( 33 aux_int_eq_if_1(x[lx+i], y[ly+i], fEQ[i]) 34 /\ 35 aux_int_lt_if_1(x[lx+i], y[ly+i], fLT[i]) 36 ) 37 ; 38 39%-----------------------------------------------------------------------------% 40