1

我对以下代码有疑问：

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

4

1 回答 1

0

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

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

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

于 2017-04-06T01:09:34.087 回答