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

ECLiPSe CLP produces variable with unexpected range

我对以下代码有疑问:

:-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。非常感谢您的帮助。

ECLiPSe 的 lib(ic) 约束求解器设计用于处理 实数 整数 值 variables/constraints 的混合.所有计算都使用 double floats 来表示上限和下限,甚至是整数运算(完整性被简单地视为附加约束)。

因为双精度浮点数有 53 位精度,所以只能精确表示 -9007199254740991..9007199254740991 范围内的整数。较大的整数由包含真实值的浮点区间近似。这就是您得到非零宽度间隔的原因。

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