Set membership in core.logic without CLP(set) - defne behaviour

103 views Asked by At

As CLP(set) seems to be stuck in the "immediate" roadmap for now 7 years and counting, I'm trying to make an incomplete, inefficient substitute to at least be able to reflect the semantics of set membership. The main idea is to both check membership on a membero-like function, and use CLP(fd) to force order in an integer list so permutations of a "set" list do not make the number of possible solutions explode exponentially. I came up with the following:

(defne set-membero [elt set both]
  ([elt set both]
   (== set both)
   (membero elt set))
  ([elt [] [elt]])
  ([elt [x . smallrest] [x . bigrest]]
   (fd/in elt x Integer/MIN_VALUE Integer/MAX_VALUE)
   (fd/< x elt)
   (set-membero elt smallrest bigrest))
  ([elt [x . _] [elt . set]]
   (fd/in elt x Integer/MIN_VALUE Integer/MAX_VALUE)
   (fd/< elt x)))

With the expected usage being something similar to the following:

(run 2 [q] (set-membero 1 [2 3] q)) "=> ((1 2 3))"   ; adds non existing members as membero                                                                                                                      
(run 2 [q] (set-membero 1 [1 2] q)) "=> ((1 2))"     ; but does not add existing elements                                                                                                                        
(run 2 [q] (set-membero q [1 2] [1 2 3])) "=> (3)"   ; substracts sets as expected                                                                                                                               
(run 2 [q] (set-membero q [1] [1 2 3])) "=> ()"      ; remember it is not set-difference!                                                                                                                        
(run 2 [q] (set-membero 1 q [1 2])) "=> ((1 2))"     ; extracts elements as expected
(run 2 [q] (set-membero 2 [3 1] q)) "=> ()"          ; fails with non-compliant "sets" (unordered)

But I'm stuck at why this happens:

(run 2 [q] (set-membero 4 [3] q))
=> () ; expected ([3 4])

This simpler case works:

(run 2 [q] (set-membero 4 [] q))
=> ([4]) ; as expected

Shouldn't (set-membero 4 [3] q) reduce to (set-membero 4 [] q) through the third defne reduction rule?

0

There are 0 answers