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

当我找到答案时，是哈哈。我使用了许多奇怪的模式来解决问题，但这是我以前从未使用过的模式。看到它的工作原理后，我就知道我有一个用于工具箱的闪亮的新工具。

对于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('ADD', [A]), R) :-
    R #= 0b0000 + (A << 4),
    A #= (R - 0b0000) >> 4.
示例用法

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

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

Answer 2

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