Как создать переработанный массив array_int_maximum в выводе Flatzinc?

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 и, следовательно, обрабатываю их, возможно, быстрее, чем автоматический перевод? (дубликат этой нерешенной проблемы)

Answer 1

Простой ответ: array_int_maximum_reifв настоящее время не используется. Он должен быть сгенерирован компилятором, но вместо этого компилятор предпочитает просто создать ограничение и использовать int_eq_reif ограничение.

До сих пор не совсем ясно, когда реифицировать функцию. Совершенно очевидно, что комплексные функции никогда не следует переформулировать, поскольку это не дает дополнительных преимуществ. Для частичных функций это все еще вопрос, когда это хорошая идея. max является частичной функцией MiniZinc, но она выполняется полностью до того, как array_int_maximum. Надеюсь, в ближайшее время будет больше информации по этому поводу.