0

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

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

[...]

初始化。opt 类型变量不需要在实例时初始化。未初始化的 opt 类型变量会自动初始化为<>.

我想用两种类型解析和处理以下约束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);

如果不是，我应该如何处理？

4

1 回答 1

1

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

对于库编写者，可以选择以您的求解器能够最好地处理的方式重写它。在标准库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谓词专门用于“可选任务”，不太可能以这种方式调用）。

于 2017-11-06T05:47:52.703 回答