如何通过非标准的扁平锌扩展获得有理数的精确无限精度表示?

默认情况下 mzn2fzn 自动计算 微型计算机 建模,并将其存储为常量 浮动 结果中的值 扁锌 模型。

例子:

文件 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;

相反,我们想要得到的是 扁锌 沿以下行归档:

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() 是一个 最近 引入,非标准, 扁锌 约束。

是否可以通过使用 std 约束目录,或者此编码是否需要对 MZN2FZn 工具?在后一种情况下,我们能得到一些指导吗?

***:我们有一些公式不适合有限精度浮点表示,因为它改变了 SAT 结果 UNSAT .