Ankur
Ankur

Reputation: 33657

Core.logic finite domain with -ve values

I am not sure why the below code doesn't return any result when using -5 as one of the domain value

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)

NOTE: This code refers to behavior in the core.logic 0.8.0 betas.

Upvotes: 3

Views: 520

Answers (2)

dnolen
dnolen

Reputation: 18556

There is no support currently in the core.logic 0.8.0 betas for domains with negative values at all. If it works it's completely by accident. I don't intend on personally working to add support for this in the near future, though a comprehensive patch would be welcome after 0.8.0 gets a proper release.

Upvotes: 2

Alex
Alex

Reputation: 13961

It looks like the implementation of the *fd constraint only works for domains with all positive values. It calculates an upper and lower bound for the left-hand factor based on simple division of the lower/upper bounds of the product domain by the upper/lower bounds of the right-hand factor domain, and vice versa. You can see how throwing negatives into the mix will cause this not to work:

 (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]

Since the signs are off, you wind up with an unsatisfiable interval for the LHS because the lower bound is greater than the upper bound.

Finite domains with negative values do work for the +fd constraint:

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

Upvotes: 1

Related Questions