0

给定以下 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 版本的信息，因此处理速度可能比自动翻译快？（这个未解决问题的重复）

4

1 回答 1

1

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

何时具体化功能仍不完全清楚。很明显，总功能不应该被具体化，因为它没有提供额外的好处。对于偏函数，何时是一个好主意仍然是一个问题。max是 MiniZinc 中的一个偏函数，但在它变成array_int_maximum. 希望很快会有更多关于这个问题的信息。

于 2021-07-01T00:39:29.127 回答