Считаются ли полуварифицированные предикаты частью стандарта?

Question

В документации FlatZinc сказано, что только нестандартные предикаты должны быть объявлены в верхней части модели FlatZinc:

Предикаты, используемые в модели, которые не являются стандартными FlatZinc, должны быть объявлены в верхней части модели FlatZinc перед любыми другими лексическими элементами. Объявления предикатов принимают форму

<predicate-item> ::= "predicate" <identifier> "(" [ <pred-param-type> : <identifier> "," ... ] ")" ";"

источник: ссылка

Судя по всему, компилятор mzn2fzn добавляет объявления предикатов с полувеществом вверху скомпилированных файлов (см.: эту проблему на github):

predicate int_eq_imp(var int: a, var int: b, var bool: r);

Я нахожу такое поведение несколько сбивающим с толку, потому что полу-овеществленные предикаты кажутся частью стандарта.

Вопрос:

• Разве это не ошибка, поскольку в верхней части файла следует объявлять только нестандартные предикаты?
• Есть ли способ подавить такие объявления?

Answer 1

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

Поскольку MiniZinc изначально разрабатывался для решателей программирования ограничений, идея заключалась в том, что даже FlatZinc в некоторых случаях мог быть совместим с разными решателями. Предполагается, что все решатели будут поддерживать по крайней мере все необходимые встроенные функции FlatZinc, а затем решатель может быстро проверить объявления, чтобы увидеть, поддерживает ли он все другие предикаты, используемые в модели FlatZinc.

В наши дни это далеко от истины. Многие решатели MiniZinc не поддерживают встроенные функции FlatZinc напрямую, а вместо этого дают переопределение. Даже упакованные решатели CP, такие как Gecode и Chuffed, на самом деле не используют объявления в модели MiniZinc, но обрабатывают ограничения в своем внутреннем реестре, вызывая ошибку, когда они сталкиваются с использованием неизвестного предиката.

Если бы стандарт FlatZinc когда-либо изменился, я думаю, что он либо предоставил бы объявления всех предикатов, используемых в модели FlatZinc, либо включил бы любые объявления. Последнее может быть более вероятным, поскольку мы не должны предполагать, что модели FlatZinc могут быть повторно использованы для разных решателей, поэтому декларация не имеет практического применения.

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