core.logic

nom/tie and spurious reification of predc constraint

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Blocker Blocker
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • 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

Activity

Hide
Nada Amin added a comment -

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.

Show
Nada Amin added a comment - 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.
Hide
David Nolen added a comment - - edited

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.

Show
David Nolen added a comment - - edited 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.
Hide
Nada Amin added a comment -

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
Show
Nada Amin added a comment - 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

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: