这些`float_div`和`float_times`约束在FlatZinc文件中是什么？

Question

我只是尝试在以下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

我有以下问题：

• 什么是float_div约束，FlatZinc 1.6标准似乎没有提到它
• 什么是float_times约束，FlatZinc 1.6标准似乎没有提到它

是否有任何FlatZinc解决程序真正支持它们？

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

Answer 1

在FlatZinc 1.6的文档中，似乎没有记录float_div和float_times的约束。这些约束是FlatZinc内置的必要部分，需要由支持浮点变量的求解器来理解。它们不能重写为FlatZinc内部构建中的其他约束，这就是编译器将使用它们的原因。我要指出的是，int_div和int_times是在旧版本的FlatZinc文档中记录的，约束的含义可以从这些约束中推断出来。(我的印象也是，在向FlatZinc 2.2.0的转换过程中，它们的含义并没有改变)

MiniZinc附带的CP解决程序Gecode支持这些约束。