如何在Flatzinc输出中产生一个具体化的`array_int_maximum`？

Question

给出下面的minizinc程序：

var 0..4: a;
var 0..5: b;
var -5..2: c;
var -8..-3: d;
var 0..8: m;
var bool: r;
constraint r <-> m = max([a,b,c,d]);
solve satisfy;

和redefinitions-2.0.mzn文件

predicate array_int_maximum(var int: m, array[int] of var int: x);                                      
predicate array_int_maximum_reif(var int: m, array[int] of var int: x, var bool: r);                    
predicate array_int_maximum_imp(var int: m, array[int] of var int: x, var bool: r); 

我希望得到一个具体化的版本作为扁平化的输出，但我确实得到了：

predicate array_int_maximum(var int: m,array [int] of var int: x);
predicate int_eq_imp(var int: a,var int: b,var bool: r);
var 0..4: a:: output_var;
var 0..13: b:: output_var;
var -5..2: c:: output_var;
var -8..-3: d:: output_var;
var 0..16: m:: output_var;
var bool: r:: output_var;
var -8..13: X_INTRODUCED_1_ ::var_is_introduced :: is_defined_var;
array [1..4] of var int: X_INTRODUCED_0_ ::var_is_introduced  = [a,b,c,d];
constraint array_int_maximum(X_INTRODUCED_1_,X_INTRODUCED_0_):: defines_var(X_INTRODUCED_1_);
constraint int_eq_imp(m,X_INTRODUCED_1_,r);
solve  satisfy;

我如何以及在哪里添加我确实支持此谓词的reif和imp版本的信息，并因此具有比自动转换更快的处理速度？(此未解决的issue的副本)

Answer 1

简单的答案是array_int_maximum_reif目前未被使用。它必须由编译器生成，但是编译器选择只创建一个array_int_maximum约束并使用int_eq_reif约束。

它仍然不完全清楚何时具体化一个函数。很明显，total函数永远不应该被具体化，因为它没有提供任何额外的好处。对于部分函数，当它是一个好主意时，它仍然是一个问题。max是MiniZinc中的一个分部函数，但它在进入array_int_maximum之前是合计的。希望很快会有更多关于这个问题的信息。