ECLiPSe CLP 产生具有意外范围的变量答案

【问题标题】：ECLiPSe CLP produces variable with unexpected rangeECLiPSe CLP 产生具有意外范围的变量
【发布时间】：2017-04-04 16:02:02
【问题描述】：

我对以下代码有疑问：

:-lib(ic).

buggy_pred(Result, In0, In1, In2, In3, In4, In5, In6, In7) :-

    Args = [In0, In1, In2, In3, In4, In5, In6, In7],
    Args :: [0..255],

    Result :: [0..18446744073709551615],    % 64bits wide

    % put 8 bytes together to form a 64-bit value
    Result #= (In0 + (In1 * 256) + (In2 * 65536) + (In3 * 16777216) + (In4 * 4294967296) +
        (In5 * 1099511627776) + (In6 * 281474976710656) + (In7 * 72057594037927936)).


buggy_pred_test :-
    buggy_pred(Result, 56, 8, 0, 0, 16, 0, 0, 1),
    get_bounds(Result, Lo, Hi),

    write(Lo), nl,
    write(Hi).

上面的代码（谓词 buggy_pred_test）不应该打印两个相同的数字吗？在这种情况下，它会产生两个不同的数字（分别为 Lo 和 Hi）：

72057662757406720
72057662757406800

我无法弄清楚这种行为的原因是什么。我正在为 Linux 使用 ECLiPSE 6.1 #194、x86_64。非常感谢您的帮助。

【问题讨论】：

标签： constraint-programming eclipse-clp

【解决方案1】：

ECLiPSe 的 lib(ic) 约束求解器设计用于处理 real 和 integer 值变量/约束的混合。所有的计算都使用 double floats 来表示上限和下限，甚至是整数运算（整数被简单地视为附加约束）。

由于双浮点数具有 53 位精度，因此只有 -9007199254740991..9007199254740991 范围内的整数可以精确表示。较大的整数由包含真值的浮点间隔来近似。这就是为什么你会得到一个非零宽度间隔的原因。

这听起来可能不太令人满意，但在实践中，涉及巨大整数域的模型很少能有效地求解，因此并没有看起来那么有用。因此，建议是对问题进行不同的建模，请参阅 here for an example 以两种方式建模问题。

【讨论】：