1

我只是尝试运行mzn2fzn以下MiniZinc文件：

var float: x1;
var float: y1;
var float: x2;
var float: y2;
constraint (x1 / y1) = 6.0;
constraint x2 * y2 <= 5.0;
solve satisfy;

这是生成的FlatZinc文件：

var -1.7976931348623157e+308..5.0: FLOAT____00001 :: is_defined_var :: var_is_introduced;
var float: x1;
var float: x2;
var float: y1;
var float: y2;
constraint float_div(x1, y1, 6.0);
constraint float_times(x2, y2, FLOAT____00001) :: defines_var(FLOAT____00001);
solve satisfy;

的版本mzn2fzn如下：

~$ mzn2fzn --version
G12 MiniZinc to FlatZinc converter, version 1.6.0
Copyright (C) 2006-2012 The University of Melbourne and NICTA

我有以下问题：

是否有任何FlatZinc求解器实际上支持它们？

注意我实际上在FlatZinc 2.2.0 的文档中找到了这些函数的踪迹，但是，我不明白为什么这些函数是由 1.6 版生成的，mzn2fzn因为它的文档似乎没有提到它们中的任何一个。

4

1 回答 1

3

在 FlatZinc 1.6 的文档中似乎疏忽了约束float_div并且float_times没有记录。这些约束是 FlatZinc 内置函数的必要部分，支持浮点变量的求解器可以理解这些约束。它们不能被重写为 FlatZinc 内置的其他约束，这就是编译器将使用它们的原因。我会注意到int_div并int_times记录在旧版本的 FlatZinc 的文档中，并且可以从这些约束中推断出约束的含义。（我也觉得他们的意思在转换到 FlatZinc 2.2.0 时没有改变）

Gecode 是 MiniZinc 附带的 CP 求解器，支持这些约束。

于 2018-12-21T00:25:09.450 回答