MiniZinc 中的通用注释

Question

我对 MiniZinc 语言的一些通用注释的含义和用法有一些疑问。请解释何时应该使用它们，如果可能的话，请举例说明。

我从 MiniZinc 官方库中复制了我发现的定义，以使问题更加直接。

注释is_define_var

将带注释的变量声明为函数定义的。该注释由编译器引入到 FlatZinc 代码中。

变量是函数定义的是什么意思？什么时候应该使用这个？

注释Maybe_partial

声明表达式可能有未定义的结果（以避免警告）

表达式具有未定义的结果是什么意思？有人可以举个例子吗？

注释promise_total

将函数声明为total，即它不会对其参数施加任何限制。

这是什么意思？我很想看到这样的例子。这是你引入自己的函数时的情况，还是也可以用于已经定义的Minizink函数？

注释var_is_introduced

声明一个由编译器引入的变量。

再说一遍，变量是由编译器引入的是什么意思？相反的说法会是什么？该变量不是编译器引入的？

注释定义_var(var $t: c)

声明变量：c 由带注释的约束在功能上定义。该注释由编译器引入到 FlatZinc 代码中。

再说一次，c 是函数定义的意味着什么，有人可以举个例子吗？

我知道这些是关于一个非常具体的库的很多问题，但我在任何地方都找不到任何好的解释。

Answer 1

首先我要说的是，在 MiniZinc 中建模时通常不会使用您所询问的注释。（也许例外maybe_partial，它对于隐藏模型中的警告很有用。）这些注释应该由 FlatZinc 求解器及其 MiniZinc 库的实现者使用。对于仍然感兴趣的人：这里有一些解释以及这些注释的用法示例。

定义变量

is_defined_var和defines_var(...)是在函数定义变量时使用的注释。这些注释总是成对出现。当变量x带有is_defined_var注解时，则存在带有 . 的约束项defines_var(x)。

当变量的解值遵循单个约束/函数时，该变量就被函数定义了。例如，我们可以输入a * b = c，现在 的解值c将来自 just a * b。这意味着在生成的 FlatZinc 中我们会发现类似以下内容：

var int: a;
var int: b;
var int: c ::is_defined_var;
constraint int_times(a,b,c) ::defines_var(c);

请注意，这些函数定义经常出现在数学表达式和具体化中。

您可能永远不需要添加这些注释。它们将由 MiniZinc 编译器自动添加。然后，求解器可以使用这些注释来分析约束和变量之间的关系。例如，在某些情况下，求解器可能会使用视图而不是完整变量。

引入变量

MiniZinc 中的某些表达式无法用简单的约束连接来表达。由于各种约束之间的关系，可能需要添加一个新变量才能在 FlatZinc 中具有与原始 MiniZinc 表达式等效的逻辑表达式。

以表达式 为例a \/ (b /\ c)。该表达式至少需要两个约束：abool_and和abool_or约束。然而，在 FlatZinc 中，谓词调用不能包含除标识符或文字之外的任何内容。因此，为了在 FlatZinc 中表达我们的示例，我们必须具体化 and 表达式并在 or 表达式中使用真值。生成的 FlatZinc 将类似于：

var bool: a;
var bool: b;
var bool: c;
var bool: X_INTRODUCED_0_ ::var_is_introduced ::is_defined_var;
constraint bool_or(a,X_INTRODUCED_0_,true);
constraint bool_and(b,c,X_INTRODUCED_0_) ::defines_var(X_INTRODUCED_0_);

请注意，因为我们使用的是具体化，所以我们再次看到一个函数定义的变量。

var_is_introduced解算器可以再次使用注释来优化其过程。它可以使用变量的视图，甚至可能在知道变量的值后丢失它。

部分功能

有些函数，即使在纯粹的数学中，也是部分的，这意味着它们没有为所有可能的输入提供定义的结果。最常见的例子是除法：我们不能除以零，x / 0 == ??。在大多数编程语言中，编写这样的代码会产生编译错误。然而，在 MiniZinc 中，未定义的表达式将“冒泡”到最接近的父布尔上下文并将其定义为 false。有关此机制的更多信息，请参阅论文“约束语言中未定义的正确处理”，其中它被称为关系语义。

在 MiniZinc 中，最常见的可以未定义的函数是数组访问a[i]（越界时未定义）、除法和可选变量的值查找deopt(x)（不存在时未定义）。

例如，给定一个a具有范围的数组1..1和一个布尔变量，b我可以编写一个表达式b -> (a[0] == 1)。由于a[0]不存在，因此没有可比较的值1。根据 MiniZinc 语义，这意味着(a[0] == 1)将被设置为false。

尽管这是 MiniZinc 的有效使用，但以这种方式使用部分函数可能是错误的。（当循环的边界太大时，通常会发生这种情况）。为了让建模者意识到这一点，MiniZinc 编译器将打印一条警告WARNING: undefined result becomes false in Boolean context。然而，有时建模者知道他在做什么，并且可能实际上想要使用这些语义。在这种情况下，可以对表达式进行注释，maybe_partial以告诉编译器不需要警告建模者。对于我们的例子，我们可以使用b -> (a[0] == 1)::maybe_partial

maybe_partial当必须使用部分语义时，该注释主要在 MiniZinc 库中使用。由于建模者不应收到有关正确使用库函数的任何警告，因此这些注释很重要。

全部功能

总函数与偏函数相反。promise_total向编译器发出信号，表明所提供的函数可用于函数的所有可能输入。您可以在标准库的许多地方找到它。

由于这些承诺，我们的库函数可以为包含的函数实现关系语义（如论文“约束语言中未定义的正确处理”中所述）。通常，部分函数必须进行额外的检查，然后根据该检查发布约束。为了确保不会有无休止的检查，部分函数中调用的谓词被承诺是完整的。

在编译器中，函数的promise_total行为就像该语言使用严格的语义（如同一篇论文中所述），并且未定义的结果可能会导致编译或求解器错误。