Какая польза от функции minizinc fix?

я вижу, что в документации fix говорится:

http://www.minizinc.org/doc-lib/doc-builtins-reflect.html#Ifunction-dd-T-cl-fix-po-var-opt-dd-T-cl-x-pc

function array [$U] of $T: fix(array [$U] of var opt $T: x)
Check if the value of every element of the array x is fixedat this point in evaluation. If all are fixed, return an array of their values, otherwise abort.

Я думаю, что его можно использовать для принуждения var к номиналу. Вот код.

array [1..num]   of var int: value  ;
%% generate random numbers from 0..num-1, this should fix the value of the var "value"  or so i think
constraint forall(i in index_set(value))(let {int:temp_value=discrete_distribution([1|i in index_set(value)]); } in value[i]=trace(show(temp_value)++"\n", temp_value));

%%% this i was expecting to work, as "value" elements are fixed above
array [1..num]   of int:value__  =[ trace(show(fix(value[i])), fix(value[i])) | i in index_set(value)] ;

Но я получаю:

MiniZinc: evaluation error:
    with i = 1
  in call 'trace'
  in call 'fix'
  expression is not fixed

Мои вопросы:

1) Я думаю, мне следует ожидать эту ошибку, так как minizinc не является языком последовательного выполнения?

2) Примеры fix в руководстве пользователя приведены только там, где используется оператор output. Это единственное место, где можно использовать fix?

3) Как бы я принудил var к par?

Кстати, я пытаюсь преобразовать эту переменную в номинал, потому что у меня проблема с выражением генератора массива. Вот код

int:num__=200;
int:seed=134;
int: two_m=2097184;
%% prepare weights for generating numbers form 1..(two_m div 64), basically same weight
array [1..(two_m div 64)] of int: value_6_wt= [seed+1 | i in 1..(two_m div 64)] ;
%% generate numbers. this dose not work gives out 
%% in variable declaration for 'value6'
%% parameter value out of range
array [1..num__] of int : value6 = [ discrete_distribution(value_6_wt) | j in 1..num__];

minizinc
person Gautam    schedule 08.10.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В языке MiniZinc разница между параметром и переменной заключается только в том, что параметр должен иметь значение во время компиляции. В компиляторе мы превращаем как можно больше переменных в параметры. Это избавляет решатель от необходимости выполнять некоторую работу. Когда мы знаем, что переменная была превращена в параметр, мы можем использовать функцию fix, чтобы убедить систему типов, что мы действительно можем использовать эту переменную в качестве параметра и увидеть ее значение.

Однако проблема здесь в том, что fix определено для прерывания, когда переменная не зафиксирована на одном значении. Если тестирование не проводится, это требует некоторых (магических) знаний о процессе компиляции. В вашем случае кажется, что второй массив оценивается до этапа оптимизации, на котором разрешаются все псевдонимы. Это причина, почему это не работает. (Это действительно одна из вещей, которая является следствием декларативного языка)

Хотя fix можно использовать только в операторах вывода в примерах (где он гарантированно работает), он используется во многих местах библиотек MiniZinc. Если мы, например, посмотрим на библиотеку, которая используется для решателей MIP, мы увидим множество ограничений, которые можно кодировать более эффективно, если один из аргументов является параметром. Поэтому вы часто будете видеть, что ограничение a в этой библиотеке сначала проверяет свои аргументы с помощью is_fixed, а затем использует лучшую кодировку, если это возвращает true.

Оператор вывода и когда is_fixed возвращает true, дадут гарантию, что переменная зафиксирована, и гарантируют, что компиляция не прервется. Нет другого способа привести переменную к параметру, но если вы не имеете дело с зависимыми определениями предикатов, вы можете просто довериться компилятору MiniZinc, чтобы гарантировать, что полученный FlatZinc будет содержать параметр вместо переменной.

person Dekker1    schedule 08.10.2018