如何在MiniZinc中对var int类型的array[int]使用arg_sort？

问题背景 #

使用MiniZinc时，想获取var int类型数组的升序排列索引（类似arg_sort的效果）。用int数组时arg_sort正常工作，但换成var int数组时，报错：

MiniZinc: type error: no function or predicate with this signature found: arg_sort(array[int] of var int)

尝试直接声明predicate arg_sort(var_values, order);时，又报错：

MiniZinc: type error: type-inst must be par set but is 'array[int] of var int'

错误原因 #

1. arg_sort是参数化函数（par function），仅支持处理固定值（par）的数组，无法直接作用于变量（var）数组。你看到的文档中关于变量数组排序的部分，指的是sort的谓词（predicate）版本，而非arg_sort函数——arg_sort并没有对应的变量数组处理版本。
2. 直接声明predicate arg_sort(var_values, order);不符合MiniZinc语法：谓词需要明确的类型声明，且不能直接引用未定义的谓词。

正确实现方式 #

要获取var int数组的升序索引，需要手动构建约束逻辑：

• 定义一个索引数组order，约束它是原数组下标的排列（每个下标仅出现一次）
• 约束原数组按order的顺序满足升序关系

完整代码示例：

% 原始固定值数组
array[1..3] of int: values = [1, 5, 3];

% 转换为变量数组
array[1..3] of var int: var_values;
constraint forall (v in 1..3) (var_values[v] = values[v] + 5);

% 存储升序索引的数组
array[1..3] of var int: order;

% 约束1：order是1..3的排列（每个索引唯一）
constraint alldifferent(order);
constraint forall(i in 1..3) (order[i] in 1..3);

% 约束2：var_values按order的顺序升序排列
constraint forall(i in 1..2) (var_values[order[i]] <= var_values[order[i+1]]);

solve satisfy;

output ["order: \(order)\nvar_values: \(var_values)"];

如果需要严格升序（无重复值场景），可以把<=替换为<。

内容的提问来源于stack exchange，提问作者Woodsy