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

В документации 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);

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

Вопрос:

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

minizinc flatzinc
person Patrick Trentin    schedule 04.06.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

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

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

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

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

person Dekker1    schedule 05.06.2020