MiniZinc 中的一般注释
General Annotations in MiniZinc
我对 MiniZinc 语言的一些通用注释的含义和用法有一些疑问。请说明何时应该使用它们，如果可能，请举例说明。
我从 MiniZinc 官方库中复制了我找到的定义以使问题更直接。
annotation is_defined_var
Declare the annotated variable as being functionally defined. This annotation is introduced into FlatZinc code by the compiler.
变量是函数定义的是什么意思？什么时候用？
annotation maybe_partial
Declare that expression may have undefined result (to avoid warnings)
表达式有未定义的结果是什么意思？有人可以举个例子吗？
annotation promise_total
Declare function as total, i.e. it does not put any constraints on its arguments.
这是什么意思？我很想看到这样的例子。是在引入自己的函数时这样，还是也可以用于已经定义好的Minizink函数？
annotation var_is_introduced
Declare a variable as being introduced by the compiler.
同样，编译器引入变量是什么意思？相反的说法是什么？变量不是编译器引入的？
annotation defines_var(var $t: c)
Declare variable: c as being functionally defined by the annotated constraint. This annotation is introduced into FlatZinc code by the compiler.
再说一次，c 是函数定义是什么意思，有人可以举个例子吗？
我知道这些是关于一个非常具体的库的很多问题，但我在任何地方都找不到任何好的解释。
首先让我说一下，您所询问的注释在 MiniZinc 中建模时通常不会使用。 （maybe_partial 可能是个例外，它可能有助于隐藏模型中的警告。）这些注释应该由 FlatZinc 求解器及其 MiniZinc 库的实现者使用。对于仍然感兴趣的任何人：这里遵循一些解释 + 这些注释的用法示例。
定义的变量
is_defined_var 和 defines_var(...) 是在函数定义变量时使用的注释。这些注释总是成对出现。当变量 x 具有 is_defined_var 注释时，则存在具有 defines_var(x).
的约束项
当一个变量的解值遵循单个 constraint/function 时，该变量在函数上定义。例如，我们可以键入 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 中表达我们的示例，我们必须具体化 and-expression 并在 or-expression 中使用真值。生成的 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 中，未定义的表达式将 "bubble up" 到它最近的父布尔上下文并将其定义为 false。有关此机制的更多信息，请参阅论文 "The Proper Treatment of Undefinedness in Constraint Languages"，其中它被称为关系语义。
在 MiniZinc 中，最常见的可以未定义的函数是数组访问 a[i]（越界时未定义）、除法和可选变量的值查找 deopt(x)（不存在时未定义） .
例如，给定一个范围为 1..1 的数组 a 和一个布尔变量 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 向编译器发出信号，表明所提供的函数可用于该函数的所有可能输入。你可以在标准库的很多地方找到它。
由于这些承诺，我们的库函数可以为包含的函数实现 关系语义 （如论文 "The Proper Treatment of Undefinedness in Constraint Languages" 中所述）。通常，部分函数必须进行额外的检查，然后 post 基于该检查的约束。为了确保没有无穷无尽的检查，承诺在部分函数中调用的谓词是完整的。
在com如果使用 promise_total 的函数，则其行为就好像该语言将使用 严格语义 （如同一篇论文中所述），并且未定义的结果可能会导致编译或求解器错误.
我对 MiniZinc 语言的一些通用注释的含义和用法有一些疑问。请说明何时应该使用它们，如果可能，请举例说明。
我从 MiniZinc 官方库中复制了我找到的定义以使问题更直接。
annotation is_defined_var
Declare the annotated variable as being functionally defined. This annotation is introduced into FlatZinc code by the compiler.
变量是函数定义的是什么意思？什么时候用？
annotation maybe_partial
Declare that expression may have undefined result (to avoid warnings)
表达式有未定义的结果是什么意思？有人可以举个例子吗？
annotation promise_total
Declare function as total, i.e. it does not put any constraints on its arguments.
这是什么意思？我很想看到这样的例子。是在引入自己的函数时这样，还是也可以用于已经定义好的Minizink函数？
annotation var_is_introduced
Declare a variable as being introduced by the compiler.
同样，编译器引入变量是什么意思？相反的说法是什么？变量不是编译器引入的？
annotation defines_var(var $t: c)
Declare variable: c as being functionally defined by the annotated constraint. This annotation is introduced into FlatZinc code by the compiler.
再说一次，c 是函数定义是什么意思，有人可以举个例子吗？
我知道这些是关于一个非常具体的库的很多问题，但我在任何地方都找不到任何好的解释。
首先让我说一下，您所询问的注释在 MiniZinc 中建模时通常不会使用。 （maybe_partial 可能是个例外，它可能有助于隐藏模型中的警告。）这些注释应该由 FlatZinc 求解器及其 MiniZinc 库的实现者使用。对于仍然感兴趣的任何人：这里遵循一些解释 + 这些注释的用法示例。
定义的变量
is_defined_var 和 defines_var(...) 是在函数定义变量时使用的注释。这些注释总是成对出现。当变量 x 具有 is_defined_var 注释时，则存在具有 defines_var(x).
当一个变量的解值遵循单个 constraint/function 时，该变量在函数上定义。例如，我们可以键入 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 中表达我们的示例，我们必须具体化 and-expression 并在 or-expression 中使用真值。生成的 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 中，未定义的表达式将 "bubble up" 到它最近的父布尔上下文并将其定义为 false。有关此机制的更多信息，请参阅论文 "The Proper Treatment of Undefinedness in Constraint Languages"，其中它被称为关系语义。
在 MiniZinc 中，最常见的可以未定义的函数是数组访问 a[i]（越界时未定义）、除法和可选变量的值查找 deopt(x)（不存在时未定义） .
例如，给定一个范围为 1..1 的数组 a 和一个布尔变量 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 向编译器发出信号，表明所提供的函数可用于该函数的所有可能输入。你可以在标准库的很多地方找到它。
由于这些承诺，我们的库函数可以为包含的函数实现 关系语义 （如论文 "The Proper Treatment of Undefinedness in Constraint Languages" 中所述）。通常，部分函数必须进行额外的检查，然后 post 基于该检查的约束。为了确保没有无穷无尽的检查，承诺在部分函数中调用的谓词是完整的。
在com如果使用 promise_total 的函数，则其行为就好像该语言将使用 严格语义 （如同一篇论文中所述），并且未定义的结果可能会导致编译或求解器错误.