问题标签 [mzn2fzn]

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

例子：

文件test.mzn

翻译成

变得等于

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

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

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

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

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

这是生成的FlatZinc文件：

的版本mzn2fzn如下：

我有以下问题：

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

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

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

我只想知道这两个 MiniZinc 求解器是否默认使用无限精度算术。

来自 MiniZinc规范：

浮点数代表实数。浮点表示是实现定义的。这意味着浮点数的可表示范围和精度是实现定义的。然而，一个实现应该在运行时中止异常浮点操作（例如，如果使用 IEEE754 浮点，则产生 NaN 的那些）。

Float 表示是实现定义的，这意味着什么？这是否取决于将使用的求解器？

mzn2fzn工具如何处理浮点表示？它的界限是什么？