如何通过非标准FlatZinc扩展获得有理数的精确无穷表示形式? [英] How to obtain an exact infinite-precision representation of rational numbers via a non-standard FlatZinc extension?
问题描述
默认情况下，mzn2fzn自动计算 MiniZinc 模型中浮点除法的结果，并将其作为常量 float 值存储在结果中FlatZinc 模型.
By default mzn2fzn automatically computes the result of a floating point division within a MiniZinc model, and stores it as a constant float value in the resulting FlatZinc model.
示例:
文件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 文件，其内容如下:
What we would like to obtain***, instead, is a FlatZinc file along the following lines:
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 约束.
where float_div() is a newly introduced, non-standard, FlatZinc constraint.
是否可以通过使用约束的std目录的变体生成这种原始问题的编码，还是这种编码需要对mzn2fzn工具的源代码进行更重大的更改?在后一种情况下，我们可以提供一些指导吗?
Is it possible to generate such an encoding of the original problem by using a variant of the std directory of constraints, or does this encoding require a more significant change of the source code of the mzn2fzn tool? In the latter case, could we have some guidance?
***:我们有一些不适用于有限精度浮点表示的公式，因为它将SAT结果转换为UNSAT.
***: we have some formulas for which the finite-precision floating-point representation is unsuitable, because it changes a SAT result into UNSAT.
推荐答案
当前无法生成无限精度的FlatZinc.尽管已经对该想法进行了几次讨论，但它需要使用可提供这些无限精确类型的库来重写或附加许多MiniZinc.这样的库，例如Boost interval库，似乎缺少选项，并且当前无法针对分发MiniZinc的所有计算机目标进行编译.对于无限精确类型，似乎有各种有趣的情况，但是在MiniZinc编译器的实现中，我们仍在寻找一种合适的实现方式.
Currently there is no way of generating FlatZinc with infinite precision. Although the idea has been discussed a few times, it would require much of MiniZinc to be rewritten or appended using a library that could provide these infinite precise types. Libraries like these, such as the Boost interval library, seem to be lacking in options and do currently not compile for all machine targets on which MiniZinc is distributed. There seem to be various interesting cases for infinite precise types, but within the implementation of the MiniZinc compiler we are still looking for finding a decent way of implementing them.
尽管表中没有无限精度.根据浮点标准，MiniZinc编译器确实打算正确.随时向 MiniZinc问题跟踪器报告任何可能发生的问题.
Although infinite precision is not on the table. The MiniZinc compiler does intend to be correct according to the floating point standards. Feel free to report any problems that might occur to the MiniZinc Issue Tracker.
这篇关于如何通过非标准FlatZinc扩展获得有理数的精确无穷表示形式?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
