clojure - -ve値を持つCore.logic有限ドメイン

Question

ドメイン値の1つとして-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.logic0.8.0ベータ版の動作を示しています。

Answer 1

現在、負の値を持つドメインのcore.logic0.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])