Search code examples
minizincflatzinc

Are half-reified predicates considered part of the standard?

The FlatZinc documentation says that only non-standard predicates must be declared at the top of a FlatZinc model:

Predicates used in the model that are not standard FlatZinc must be declared at the top of a FlatZinc model, before any other lexical items. Predicate declarations take the form

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

source: link

Apparently, the mzn2fzn compiler adds half-reified predicate declarations at the top of compiled files (see: this github issue):

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

I find this behavior somewhat confusing, because half-reified predicates appear to be part of the standard.

Q:

  • Isn't this a bug, since only non-standard predicates should be declared at the top of the file?
  • Is there a way to suppress such declarations?
Solution

  • The definition of "non-standard" might not be well-defined in the current version of the documentation. The meaning is that all predicates that are not FlatZinc Builtins will be declared at the top of the FlatZinc model.

    As MiniZinc was originally designed for constraint programming solvers, the idea was that even FlatZinc could in some cases be compatible with different solvers. The assumption being that all solvers would support at least all required FlatZinc builtins and then the solver can quickly check the declarations to see if it supports all other predicates used in the FlatZinc model.

    These days, this is far from the truth. Many of the MiniZinc solvers do not support the FlatZinc builtins directly, but instead give redefinitions. Even the packaged CP solvers like Gecode and Chuffed do not actually use the declarations in the MiniZinc model, but process the constraints against their internal registry throwing an error when they encounter usage of an unknown predicate.

    If the FlatZinc standard was ever to change, then I think that it would either provide the declarations of all predicates used in the FlatZinc model or it would include any declarations. The latter might be more likely as we should not assume that FlatZinc models can be reused for different solvers, so the declaration offer little practical use.

    To summarise and answer your questions directly. This is not a bug, even though int_eq_imp might seem standard, it is not part of the FlatZinc builtins. There is currently not way to suppress these declarations, but a solver can simply ignore all lines that contain predicate declarations and handle unknown predicates when processing constraints.