如何通过非标准的FlatZinc扩展得到有理数的精确无限精度表示？

Question

默认情况下，mzn2fzn会自动计算MiniZinc模型中浮点除法的结果，并将其存储为结果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。

Answer 1

目前还没有产生无限精度的FlatZinc的方法。虽然这个想法已经讨论过几次，但是它需要使用一个库来重写或附加大量的MiniZinc，这个库可以提供这些无限精确的类型。像Boost interval库这样的库似乎缺乏选项，而且目前还没有为MiniZinc分布的所有机器目标进行编译。对于无限精确的类型，似乎有各种各样有趣的例子，但是在MiniZinc编译器的实现中，我们仍然在寻找一种很好的方法来实现它们。

尽管没有无限的精度在桌面上。MiniZinc编译器确实打算根据浮点标准进行正确的操作。请随时报告MiniZinc问题跟踪器可能出现的任何问题。