SWI-Prolog и ограничения, библиотека CLP (FD)

Я играю с ограничениями в (swi) прологе, используя библиотеку clpfd.

Я пытаюсь определить, когда один набор ограничений инкапсулирует или включает в себя другой, например, X <4 инкапсулирует X <7, поскольку всякий раз, когда первое истинно, второе истинно. Это можно легко представить с помощью логического вывода. Однако я не смог получить # ==> чтобы получить желаемый результат, поэтому я прибег к использованию not (Co1 # / \ # \ Co2), где Co1 и Co2 являются ограничениями. Это нормально для отдельных ограничений, но затем я хотел передать соединение ограничений в Co1 и Co2.

Теперь вот проблема. Когда я пробую

X#<7 #/\ #\X#<4.

, я возвращаюсь

X in 4..6,
X+1#=_G822,
X+1#=_G834,
_G822 in 5..7,
_G834 in 5..7.

(как ни странно, выполнение этого в Sicstus приводит к ошибке сегментации)

Когда я передаю

X#<7,X#<4

, я получаю желаемое

X in inf..3.

Очевидно, я не могу пройти последнее в not (Co1 # / \ # \ Co2), но первое не дает мне желаемого результата. Может ли кто-нибудь объяснить, почему два подхода дают разные результаты, и как я могу заставить первый работать как второй?

5
задан false 23 January 2014 в 16:44
поделиться