Я играю с ограничениями в (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), но первое не дает мне желаемого результата. Может ли кто-нибудь объяснить, почему два подхода дают разные результаты, и как я могу заставить первый работать как второй?