MiniZinc中的一般注释

Question

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

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

注释is_defined_var 将带注释的变量声明为功能定义。此注释由编译器引入到FlatZinc代码中。

变量是函数定义的，这意味着什么？什么时候应该使用呢？

注释maybe_partial 声明该表达式可能具有未定义的结果(以避免警告)

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

注释promise_total 将函数声明为总计，即它不对其参数设置任何限制。

这是什么意思？我很想看看这方面的例子。这是当您引入您自己的函数时，还是也可以用于已经定义的Minizink函数？

注释var_is_introduced 将变量声明为编译器引入的变量。

再说一遍，变量是由编译器引入的，这意味着什么？相反的说法是什么？这个变量不是编译器引入的吗？

注释defines_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的解决方案值将来自于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)。该表达式至少需要两个约束，一个bool_and约束和一个bool_or约束。但是，在FlatZinc中，谓词调用不能包含除标识符或文字以外的任何内容。因此，要在FlatZinc中表达我们的示例，我们必须对和表达式进行具体化，并在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)的除法和值查找(不在时未定义)。

例如，给定一个具有range 1..1的数组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的函数将表现为该语言将使用严格的语义(正如在同一篇文章中描述的那样)，而未定义的结果可能会导致编译或求解程序错误。