Skip to content

Commit

Permalink
addcg should not clobber any binding information.
Browse files Browse the repository at this point in the history
  • Loading branch information
@namin
namin committed Dec 19, 2012
1 parent 7db01c7 commit 5dbcf8f
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 2 deletions.
6 changes: 5 additions & 1 deletion src/main/clojure/clojure/core/logic.clj
View file
Expand Up @@ -2857,7 +2857,11 @@
(defn addcg [c]
(fn [a]
(let [a (reduce (fn [a x]
(ext-no-check a x (subst-val ::unbound)))
(let [[xp vp :as prev] (find (:s a) x)
a (ext-no-check a x (subst-val ::unbound))]
(if (nil? prev)
a
(ext-no-check a vp xp))))
a (unbound-rands a c))]
(assoc a :cs (addc (:cs a) c)))))

Expand Down
23 changes: 22 additions & 1 deletion src/test/clojure/clojure/core/logic/tests.clj
View file
Expand Up @@ -2364,6 +2364,15 @@
s (unify empty-s x0 x1)]
(is (= s empty-s))))

(deftest test-logic-81-fd []
(is (= (run* [q]
(fresh [x y z]
(== q x)
(distinctfd [q y])
(== y x)
(infd q x y (interval 1 3))))
())))

;; =============================================================================
;; predc

Expand All @@ -2386,7 +2395,19 @@
(is (= (run* [q]
(== q "foo")
(predc q number? `number?))
())))
()))
(is (= (run* [q]
(fresh [x]
(predc q number? `number?)
(== q x)
(== x "foo")))
()))
(is (= (run* [q]
(fresh [x]
(== q x)
(predc q number? `number?)
(== x "foo")))
())))

;; =============================================================================
;; Real cKanren programs
Expand Down

5 comments on commit 5dbcf8f

@swannodette
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I should explain a couple of things so it's clear why that original bit of code I wrote exists at all. The Scheme implementation of cKanren involves a lot of scanning of the constraint store. As an optimization I chose a different representation - the constraint store contains a map of variables to sets of constraint ids (integers) as well as a map of those ids to the actual constraints. Now finding the constraint set for a particular variable is a cheap operation.

However a complexity arises because logic vars can alias logic vars, imagine the case of (== u v) where u and v are both fresh. It easy to get into a situation where the aliasing is not reflected in the constraint store. My solution was to try and create stable "root" vars - there can only be one "root" var. Of course this means we have to do some merging of constraints and domain information if we have two fresh vars that have constraint information on them.

Ok, so what addcg does with fresh vars - it ensures they are created as roots. So to me this bug seems to be a violation of an invariant that unbound-rands should uphold. It should only return the vars which truly have no binding in the substitution map. Vars which have constraints but no binding appear as SubstValues in the substitution map with their value field, :v, set to ::unbound. So I don't think that addcg should check for clobbering, rather unbound-rands should be fixed (if it can of course).

Hopefully this makes sense. Happy to clarify further.

@namin
Copy link
Owner Author

@namin namin commented on 5dbcf8f Dec 19, 2012

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the clarification. It would be very helpful if we could do a text chat, perhaps via Gmail (nada.amin@gmail.com)?

@namin
Copy link
Owner Author

@namin namin commented on 5dbcf8f Dec 19, 2012

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In a nutshell, my understanding of the root issue is that 'rands' does not take the substitution map into account.

Consider this program:

(run* [q]
           (fresh [x]
             (== q x)
             (predc q number? `number?)
             (== x "foo")))

First, (q . x). So x is the implicit root. But then, predc is attaching the constraint keyed by q, which is not a root!

Then unbound-rands just returns q, and this clobbers the (q . x).

In order for predc to attach the constraint correctly, it needs to walk the rands. The API issue now is that addc, updatec, remc do not take a Substitution.

Do you agree with this assessment?

@swannodette
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes I think you are right! addc, updatec, and remc need the Substitution to know what vars a constraint actually refers to. This also opens the door for some optimizations I've been thinking about for a while - but more importantly I really do think this should address the underlying issue.

@swannodette
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW, let me know if you would like to tackle this. More than happy to take a patch for master. Or if you'd rather focus on the alphaKanren work, I'm also more than happy to dig into this one.

Please sign in to comment.