[LOGIC-91] nom/tie and spurious reification of predc constraint Created: 02/Jan/13 Updated: 02/Jan/13 Resolved: 02/Jan/13 |
|
| Status: | Resolved |
| Project: | core.logic |
| Component/s: | None |
| Affects Version/s: | None |
| Fix Version/s: | None |
| Type: | Defect | Priority: | Blocker |
| Reporter: | Nada Amin | Assignee: | David Nolen |
| Resolution: | Completed | Votes: | 0 |
| Labels: | None | ||
| Description |
(is (= (run* [q]
(nom/fresh [a]
(fresh [x]
(predc x number? `number?)
(== x 1)
(== (nom/tie a [a x]) q))))
[(nom/tie 'a_0 '(a_0 1))]))
(is (= (run* [q]
(nom/fresh [a]
(fresh [x]
(== x 1)
(predc x number? `number?)
(== (nom/tie a [a x]) q))))
[(nom/tie 'a_0 '(a_0 1))])) ;; false b/c of extra :- number? constraint
|
| Comments |
| Comment by Nada Amin [ 02/Jan/13 5:07 AM ] |
|
Implementing -force-ans in Tie clojure.core.logic.IForceAnswerTerm
(-force-ans [v x]
(force-ans (:body v)))
resolves the test above, but not this one: (is (= (run* [q]
(nom/fresh [a b c]
(fresh [x y]
(== x 1)
(predc x number? `number?)
(== (nom/tie b (nom/tie a [a x])) (nom/tie c q)))))
[(nom/tie 'a_0 '(a_0 1))])) ;; still false b/c of extra :- number? constraint
|
| Comment by David Nolen [ 02/Jan/13 8:15 AM ] |
|
This issue actually impacts any "single shot" constraint that implements `-relevant?` as simply returning `true`. The problem is that the `cgoal` constraint wrapper checks `runnable?`, runs the constraint, and then checks `relevant?` and if that's true adds the constraint even though it may very well may be entailed! There are 6 constraints (1 of them the `defc` macro) which implement `-relevant?` as returning `true`. I think we should have more support (a protocol) for constraints which are essentially "single shot" and don't need to bother with implementing the `IRelevant` protocol. For some background - the CLP(FD) constraints benefit most from the `IRelevant` protocol, where the constraints involve up to 3 terms and a considerable amount of propagation work may be avoided by doing some checking up front. |
| Comment by Nada Amin [ 02/Jan/13 8:19 AM ] |
|
Hi David, I have a fix proposed in pull request https://github.com/clojure/core.logic/pull/15 The idea there is that to honor single-shot constraints, we only need to honor the (remcg this) that they contain. This is only possible if they have proper ids. That's what I fix. Let me know what you think. |
| Comment by David Nolen [ 02/Jan/13 8:46 AM ] |
|
fixed, http://github.com/clojure/core.logic/commit/020f730429d71315f752ea51abad20dca896c8b0 |