解析时 Option Type 的实例是什么？

Question

关于选项类型，Minizinc（第6.6.3节）的specification说：

Overview. Option types defined using the opt type constructor, define types that may or may not be there. They are similar to Maybe types of Haskell implicity adding a new value <> to the type.

[...]

Initialisation. An opt type variable does not need to be initialised at instance-time. An uninitialised opt type variable is automatically initialised to <>.

我想用两种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 修饰符的存在并假设 constraint 签名等于以下签名吗？

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

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

Answer 1

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

为真时

对于库编写者，可以选择以您的求解器能够处理得最好的方式重写它。在标准库中 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 谓词专门用于 "optional tasks"，不太可能那样称呼）。

解析时 Option Type 的实例是什么？

What is an instance of Option Type at parsing time?

constraint-programming

minizinc

flatzinc