SWI-Prolog сообщает о неправильном ответе с помощью битовых сдвигов CLPFD - PullRequest
Новая
       45

SWI-Prolog сообщает о неправильном ответе с помощью битовых сдвигов CLPFD

3 голосов
/ 21 марта 2020

Я столкнулся с этим в гораздо большей кодовой базе, но сократил ее до минимального воспроизводимого примера. Вот некоторый код для ассемблера: 

:- 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 .

Is это ошибка в моей программе или ошибка в Прологе? Как бы это исправить?

Ответы [ 2 ]

2 голосов
/ 21 марта 2020

Это ошибка в моей программе или ошибка в Прологе? Как бы это исправить?

Это ошибка юзабилити используемого вами верхнего уровня. Если вы присмотритесь очень внимательно, вы можете найти крошечный намек: 

81#=_42146<<4 .
             ^ SPACE

Это крошечное пространство означает: пожалуйста, обратите внимание, что есть больше, чем этот ответ. И на самом деле, есть два ответа. Первый ответ (от 'ADD') - подделка, он не содержит никакого решения. Только второй ответ содержит одно решение.

Обратите внимание, что Пролог в основном дает ответы, а не решения. Вот почему мы говорим о заменах ответов . Связь между ответами и решениями неуловима. Ответ может содержать от нуля до бесконечного числа решений.

Так почему же Prolog не производит решения напрямую?

Прежде всего, для бесконечных решений, которые были бы очень неэффективными. Подумайте о length(L,3), который имеет единственный ответ, который содержит все списки длины 3 с любыми возможными элементами, а значит, бесконечное количество решений. Как L = [1,2,3] или L = [bof, toto, machin-maschin] или L = [louis_XVI, bernie, bernie] и так далее. С помощью логической переменной мы можем свернуть эту бесконечность трехэлементных списков в следующий ответ: L = [_A,_B,_C]. Это сила логической переменной!

Эта сила также используется в ограничениях. Но с этой силой приходит большая ответственность и много бремени. В конце концов, многие задачи легко вычислить в одном направлении, а наоборот - сложно. Вы обнаружили такую ​​проблему. В этом случае можно улучшить clpfd, чтобы легко справиться с этим случаем, но в общем случае это неразрешимо. Таким образом, иногда нет никакого алгоритма вообще. И в таких случаях дать ложный ответ (несоответствие, Scheinlösung, решение бланш) - это лучшее, что может сделать система. В качестве альтернативы это может вызвать ошибку и прервать все вычисления. Но это грубо. Часто мы можем жить с такими несоответствиями.

Возьмите ваш случай, если вы действительно хотите быть уверенным в существовании решения, удалите ограничения из ответа, обозначив их! 

?- asm(I,81), I = instruction(_,[R]).
   I = instruction('ADD', [R]),
   R in 0..1023,
   81#=R<<4
;  I = instruction('SUB', [R]),
   R in 0..1023,
   80#=R<<4.

?- asm(I,81), I = instruction(_,[R]), labeling([],[R]).
   I = instruction('SUB', [5]),
   R = 5
;  false.

Другой метод - сделать ограничения сильнее, как показывал @ Guy-Coder. Это может работать (и тогда это хорошо), но более сложно понять. И может также быть менее эффективным в определенных ситуациях. Это настоящая инженерная проблема. Когда мы принимаем несоответствие в качестве цены для более быстрых решений в определенных случаях?

2 голосов
/ 21 марта 2020

Когда я нашел ответ, это был LOL. Я использовал много странных моделей для решения проблемы, но я никогда не использовал эту модель раньше. Как только я увидел, что это работает, я понял, что у меня появился новый инструмент для ящика для инструментов.

С проблемами CLP (FD) они обычно могут работать в обоих направлениях, и это то, что вы хотели. Первая проблема, с которой вы столкнулись, заключается в том, что у вас есть bigconst(A), который действует как охранное заявление. Так что просто отбросьте это.

Затем следующее: R #= 0b0000 + (A << 4) работает, как ожидалось, но страдает от проблемы, не работает как нужно в обоих направлениях, 

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

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

Аналогично reverse 

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]).
...