最近我注意到，一些最新版本的FlatZinc支持半化谓词：
半化谓词本质上表示布尔变量所隐含的约束，而不是等效于一个变量。
来源： 文档
问：
- 现在所有全局谓词都有
_reif版本吗？ - 是否所有全局谓词也有
_imp版本？
查看share/minizinc/的内容，我可以看到std里面只有nosets.mzn使用_imp谓词，所以我的印象是还没有强制支持_imp谓词。问：这是对的吗？
查看文档，我发现：
因此，求解器库应尽可能提供约束的简化版本。该库包含为此目的
fzn__reif.mzn的文件。来源： 文档
如果我正确解释它，则没有必要支持_reif谓词，因为它们已经在share/minizinc中重新定义(尽管它可能对性能有益(。问：这是对的吗？
大多数情况下，谓词(调用(R(...)用作实际约束：constraint R(...)。现在处理表达式R(...)时的问题是，它是否可以直接提供给求解器，或者它是否具有需要评估的重定义。
如果谓词用于更复杂的表达式B / R(...)，那么我们不能只给求解器调用R(...)，因为我们不想强制执行R(...)。相反，我们想知道R(...)描述的关系是否成立。这就是我们所说的化。
因此，必须有一个强制r <-> R(...)R_reif(..., r)谓词。从本质上讲，这给出了R(...)的真值。同样，当编译器被赋予表达式R_reif(...,r)时，它将查看是否可以将其直接提供给求解器，或者是否有可用的重定义。如果这两个都不可用，则编译器将尝试从R(...)的重定义生成重定义。如果这也失败，则编译器将停止编译。
如果我们回顾一下我们的示例，B / R(...)，那么人们可能会注意到使用r <-> R(...)不仅仅是必要的。如果R(...)是假的，那么我们仍然需要Btrue，如果B是false我们仍然想强制R(...);但是，我们知道没有什么会迫使R(...)变得false。我们说R(...)是在积极的背景下。在这种情况下，这意味着拥有r -> R(...)就足够了。这被称为半化。
在MiniZinc中，可以引入一个R_imp(..., r)谓词来提供单独的半化谓词。这可以是直接传递到求解器或重定义中的内容。如果编译器必须R(...)具体化表达式并看到它处于积极的上下文中，那么它将首先尝试查看它是否可以找到R_imp(..., r)，否则回退到R_reif(..., r)。请注意，如果生成重定义，则调用的上下文将向内传播，并且重定义中仍可能发生半重定义。
总结并直接回答您的问题：
- 所有全局谓词都可以统一。
_reif的重定义可以显式定义，也可以通过从其重定义生成生成。 - 没有一个全局变量是半化的。这不是必需的，因为在生成重新定义时仍然可以触发半化，并且目前没有已知的情况表明显式半化定义表现更好。
- 目前没有需要求解器支持的半化谓词。但请注意，任何
_reif谓词都可以由求解器_imp实现(包括 FlatZinc 内置(。 - 它不需要支持任何全局
_reif谓词;但是，FlatZinc 内置中有几个必需的_reif谓词确实需要支持。如果求解器未重新定义或实现这些谓词，则求解器无法支持生成的 FlatZinc。