Конечный домен Core.logic со значениями -ve

Question

Я не уверен, почему приведенный ниже код не возвращает никакого результата при использовании -5 в качестве одного из значений домена

user=> (run* [q] (infd q (domain -5 5)) (*fd q q 25))
()
user=> (run* [q] (infd q (domain 0 5)) (*fd q q 25))
(5)

ПРИМЕЧАНИЕ. Этот код относится к поведению в бета-версиях core.logic 0.8.0.

Answer 1

В настоящее время в бета-версиях core.logic 0.8.0 поддержка доменов с отрицательными значениями отсутствует. Если это работает, то это совершенно случайно. Я не собираюсь лично работать над тем, чтобы добавить поддержку для этого в ближайшем будущем, хотя всесторонний патч будет приветствоваться после того, как 0.8.0 получит надлежащую версию.

Answer 2

Похоже, реализация *fd ограничение работает только для доменов со всеми положительными значениями. Он вычисляет верхнюю и нижнюю границы для левого фактора на основе простого деления нижней / верхней границ области продукта на верхнюю / нижнюю границы правой области фактора, и наоборот. Вы можете видеть, как добавление негативов в микс приведет к тому, что это не сработает:

 (run* [q]
   (fresh [r]
     (infd q (domain 1 2 3 4 5))
     (infd r (domain 20 25))
     (*fd q q r)))

 Product = [20..25], RHS = [1..5] => LHS = [20/5..25/1] = [4..25]

 (run* [q]
   (fresh [r]
     (infd q (domain -1 0 1 2 3 4 5))
     (infd r (domain 20 25))
     (*fd q q r)))

 Product = [20..25], RHS = [-1..5] => LHS = [20/5..25/-1] = [4..-25]

Так как знаки выключены, вы получите неудовлетворительный интервал для LHS, потому что нижняя граница больше, чем верхняя граница.

Конечные домены с отрицательными значениями работают на +fd ограничение:

 (run* [q] (fresh [a b] (infd a b (domain -1 0 1)) (+fd a b 0) (== q [a b])))
 => ([-1 1] [0 0] [1 -1])