Что является экземпляром Option Type во время синтаксического анализа?

Question

О типах опций в спецификации Minizinc (раздел 6.6.3) говорится:

Обзор. Типы опций, определенные с помощью конструктора типов opt, определяют типы, которые могут быть или не быть там. Они похожи на типы типа "возможно" в Haskell, добавляя новое значение <> к типу.

[...]

Инициализация. Переменная типа opt не требует инициализации во время экземпляра. Неинициализированная переменная типа opt автоматически инициализируется <>,

Я хотел бы проанализировать и обработать следующее ограничение с двумя opt типы:

predicate alternative(var opt int: s0, var int: d0,
                      array[int] of var opt int: s,
                      array[int] of var int: d);

Тем не менее, я не уверен, что я должен ожидать в качестве значений для аргументов s0 а также s при разборе этого ограничения.

Могу ли я просто игнорировать присутствие opt модификатор и предположить, что подпись ограничения равна следующей?

predicate alternative(var int: s0, var int: d0,
                      array[int] of var int: s,
                      array[int] of var int: d);

Если нет, как я должен справиться с этим?

Answer 1

В MiniZinc типы параметров переменных обрабатываются как переменные, которые могут не существовать. Внутри компилятора эти переменные преобразуются, эти переменные интерпретируются и переписываются таким образом, что вывод FlatZinc содержит только действительные переменные. Обычно это означает, что булева переменная добавляется для каждой переменной, которая имеет значение true, если-и-только-если переменная "существует".

Для авторов библиотеки есть возможность переписать его таким образом, чтобы ваш решатель справился с ним наилучшим образом. В стандартной библиотеке alternative определяется как:

predicate alternative(var opt int: s0, var int: d0,
                  array[int] of var opt int: s,
                  array[int] of var int: d) =
          assert(index_set(s) = index_set(d),
                 "alternative: index sets of third and fourth argument must be identical",
          sum(i in index_set(s))(bool2int(occurs(s[i]))) <= 1 /\
          span(s0,d0,s,d)
      );

Обратите внимание, что occurs intrinsic используется для проверки существования переменной. Дополнительные сведения о типах переменных можно найти в библиотеке MiniZinc: http://www.minizinc.org/doc-lib/doc-optiontypes.html. При необходимости вы также можете использовать выражение let для создания дополнительной переменной, а затем сопоставить предикат с внутренним предикатом решателя.

Даже если нет лучшей декомпозиции необязательного предиката типа для вашего решателя, все же стоит реализовать предикат без типов опций. Из-за перегрузки MiniZinc эта реализация будет использоваться всякий раз, когда предикат вызывается с массивами типов переменных, не являющихся опциями. (Обратите внимание, что alternative Предикат специально предназначен для "необязательных задач" и вряд ли так будет называться).