在解析时，Option Type的实例是什么

Question

关于选项类型，Minizinc的规范(第6.6.3节)说：

概述使用opt-type构造函数定义的选项类型，定义可能存在或不存在的类型。它们类似于Haskell implicity的Maybe类型，为该类型添加了一个新值<>。

[…]

初始化opt类型的变量不需要在实例时初始化。未初始化的选择类型变量为自动初始化为CCD_ 2。

我想用两种opt类型解析和处理以下约束：

predicate alternative(var opt int: s0, var int: d0,
array[int] of var opt int: s,
array[int] of var int: d);

但是，在解析此约束时，我不确定参数s0和s的值应该是什么。

我可以简单地忽略opt修饰符的存在，并假设约束签名等于以下签名吗？

predicate alternative(var int: s0, var int: d0,
array[int] of var int: s,
array[int] of var int: d);

如果没有，我该如何处理？

Answer 1

在MiniZinc中，变量选项类型被处理为可能不存在的变量。在编译器中，这些变量被转换，这些变量以FlatZinc输出仅包含实际变量的方式被解释和重写。通常，这意味着为每个为true的变量添加一个布尔变量，当且仅当变量"存在"时。

对于库编写器，可以选择以这样一种方式重写它，即您的解算器能够最好地处理它。在标准库中，alternative被定义为：

predicate alternative(var opt int: s0, var int: d0,
array[int] of var opt int: s,
array[int] of var int: d) =
assert(index_set(s) = index_set(d),
"alternative: index sets of third and fourth argument must be identical",
sum(i in index_set(s))(bool2int(occurs(s[i]))) <= 1 /
span(s0,d0,s,d)
);

请注意，occurs内在函数用于测试变量是否存在。更多变量类型的内部函数可以在MiniZinc库中找到：http://www.minizinc.org/doc-lib/doc-optiontypes.html.如果需要，还可以使用let表达式创建额外的变量，然后将谓词映射到求解器内部谓词。

即使求解器没有更好的可选类型谓词分解，实现没有选项类型的谓词仍然是值得的。由于MiniZinc的重载，每当使用非选项变量类型的数组调用谓词时，都会使用该实现。(请注意，alternative谓词专门用于"可选任务"，不太可能以这种方式调用)。