2

FlatZinc 文档说只有非标准谓词必须在 FlatZinc 模型的顶部声明：

模型中使用的非标准 FlatZinc 谓词必须在 FlatZinc 模型的顶部声明，在任何其他词汇项之前。谓词声明的形式

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

来源：链接

显然，mzn2fzn 编译器在编译文件的顶部添加了半具体化的谓词声明（参见： this github issue）：

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

我觉得这种行为有点令人困惑，因为半具体化的谓词似乎是标准的一部分。

问：

  • 这不是一个错误，因为只有非标准谓词应该在文件顶部声明？
  • 有没有办法压制这样的声明？
4

1 回答 1

2

“非标准”的定义在当前版本的文档中可能没有明确定义。意思是所有不是FlatZinc Builtins的谓词都将在 FlatZinc 模型的顶部声明。

由于 MiniZinc 最初是为约束规划求解器设计的，其想法是即使 FlatZinc 在某些情况下也可以与不同的求解器兼容。假设所有求解器都至少支持所有必需的 FlatZinc 内置函数，然后求解器可以快速检查声明以查看它是否支持 FlatZinc 模型中使用的所有其他谓词。

如今，这与事实相去甚远。许多 MiniZinc 求解器不直接支持 FlatZinc 内置函数，而是重新定义。甚至像 Gecode 和 Chuffed 这样的打包 CP 求解器实际上也没有使用 MiniZinc 模型中的声明，而是在遇到使用未知谓词时针对其内部注册表处理约束并抛出错误。

如果 FlatZinc 标准要改变，那么我认为它要么提供 FlatZinc 模型中使用的所有谓词的声明，要么包括任何声明。后者可能更有可能，因为我们不应该假设 FlatZinc 模型可以用于不同的求解器，因此该声明几乎没有实际用途。

总结并直接回答您的问题。这不是一个错误，尽管int_eq_imp它看起来很标准，但它不是 FlatZinc 内置函数的一部分。目前没有办法抑制这些声明，但求解器可以简单地忽略所有包含谓词声明的行，并在处理约束时处理未知谓词。

于 2020-06-05T02:26:14.563 回答