1

默认情况下，自动计算MiniZincmzn2fzn模型中浮点除法的结果，并将其作为常量浮点值存储在生成的FlatZinc模型中。

例子：

文件test.mzn

var float: x;
constraint      1.0 / 1000000000000000000000000000000000.0 <= x;
constraint x <= 2.0 / 1000000000000000000000000000000000.0;
solve satisfy;

翻译成

mzn2fzn test.mzn

变得等于

var 1e-33..2e-33: x;
solve satisfy;

相反，我们想要获得的是一个FlatZinc文件，内容如下：

var float: x;
var float: lb;
var float: ub;
constraint float_div(1.0, 1000000000000000000000000000000000.0, lb);
constraint float_div(2.0, 1000000000000000000000000000000000.0, ub);
solve satisfy;

其中float_div()是一个新引入的非标准FlatZinc约束。

是否可以通过使用约束目录的变体来生成原始问题的std这种编码，或者这种编码是否需要对工具的源代码进行更重大的更改mzn2fzn？在后一种情况下，我们可以提供一些指导吗？

***：我们有一些公式不适合有限精度浮点表示，因为它会将SAT结果更改为UNSAT.

4

1 回答 1

2

目前没有办法以无限精度生成 FlatZinc。尽管这个想法已经讨论过几次，但它需要使用可以提供这些无限精确类型的库来重写或附加 MiniZinc 的大部分内容。像这样的库，例如 Boostinterval库，似乎缺少选项，并且目前不能针对所有分发 MiniZinc 的机器目标进行编译。对于无限精确类型，似乎有各种有趣的案例，但在 MiniZinc 编译器的实现中，我们仍在寻找一种体面的方式来实现它们。

虽然无限精度不在桌面上。MiniZinc 编译器确实打算根据浮点标准是正确的。随时向MiniZinc 问题跟踪器报告可能出现的任何问题。

于 2018-12-19T23:02:33.560 回答