代码之家 › 专栏 › 技术社区 › Patrick Trentin

解析时选项类型的实例是什么?

flatzinc minizinc constraint-programming

0

Patrick Trentin · 技术社区 · 7 年前

关于 选项类型 这个 specification Minizine(第6.6.3节)表示:

使用opt类型构造函数定义的选项类型,定义可能存在或不存在的类型。它们类似于Haskell隐式的可能类型,添加了一个新的值 <> 到类型。

[...]

初始化。 自动初始化为 <> .

我想分析和处理以下内容限制 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 分析此约束时。

我能简单地忽略 选择 修饰符并假设限制签名是否等于以下签名?

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

如果没有,我应该如何处理?

1 回复 | 直到 7 年前

1

Dekker1 7 年前

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

对于库作者来说,可以选择重写它,使您的解算器能够最好地处理它。在标准库中 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 内部函数用于测试变量是否存在。在Minizin库中可以找到更多变量类型的内部函数: http://www.minizinc.org/doc-lib/doc-optiontypes.html . 如有必要,还可以使用let表达式创建额外变量,然后将谓词映射到求解器内部谓词。

即使您的求解器没有更好的可选类型谓词分解,也仍然值得在没有选项类型的情况下实现谓词。由于Minizin的重载,每当使用非选项变量类型的数组调用谓词时,都将使用该实现。(请注意 可供替代的 谓词专门用于“可选任务”,不太可能这样称呼)。