prolog - SWI-Prolog 使用移位 CLPFD 报告错误答案

Question

我在一个更大的代码库中遇到过这个问题，但将其缩减为一个最小的可重现示例。这是汇编程序的一些代码:

:- use_module(library(clpfd)).

bigconst(X) :- X #=< 0x3FF, X #>= 0.

asm(instruction('ADD', [A]), R) :-
  bigconst(A),
  R #= 0b0000 + (A << 4).
asm(instruction('SUB', [A]), R) :-
  bigconst(A),
  R #= 0b0001 + (A << 4).

它似乎在组装时起作用:

?- asm(instruction('SUB', [5]), R).
R = 81.

但是反汇编的时候好像失败了:

?- asm(I, 81).
I = instruction('ADD', [_42146]),
_42146 in 0..1023,
81#=_42146<<4 .

这是我程序中的错误还是 Prolog 中的错误？我该如何解决这个问题？

Answer 1

当我找到答案时，大声笑。我用过很多奇怪的模式来解决问题，但这是我以前从未使用过的。一旦我看到它的工作，我就知道我有一个用于工具箱的 Shiny 新工具。

对于 CLP(FD) 问题，它们通常可以双向工作，这正是您想要的。你遇到的第一个问题是你有 bigconst(A)这就像守卫声明。所以把它扔掉。

接下来就是R #= 0b0000 + (A << 4)按预期工作但遇到问题，两种方式都无法按预期工作，

?- X #= 4 << 4.
X = 64.

?- 64 #= X << 4.
64#=X<<4.

反之亦然

B #= A >> 4.

也按预期工作，也遇到同样的问题。

?- X #= 64 >> 4.
X = 4.

?- 4 #= X >> 4.
4#=X>>4.

所以我尝试使用 in/2 添加一些约束那没有用，然后意识到我已经有了所有需要的约束并且它们起作用了。

asm(instruction('ADD', [A]), R) :-
    R #= 0b0000 + (A << 4),
    A #= (R - 0b0000) >> 4.

示例用法

?- asm(instruction('ADD', [5]), R).
R = 80.

?- asm(I,80).
I = instruction('ADD', [5]).

为了表明它不是一击而出的奇迹。

asm(instruction('SUB', [A]), R) :-
    R #= 0b0001 + (A << 4),
    A #= (R - 0b0001) >> 4.

示例用法

?- asm(instruction('SUB', [5]), R).
R = 81.

?- asm(I,81).
I = instruction('SUB', [5]).