Open mrrodriguez opened 7 years ago
I suspect the compiler check for the non-sensical condition of a binding within a single negation is being overly sensitive and catching something that it shouldn't. I agree that I'd expect at least the first example to work, and can't think of any structural reason why it isn't doable.
Agreed that something like
[[:not [:and
[:x (= ?z (:z this))]
[:y (= ?z (:z this))]]]])])
ought to work. I wonder if this is actually a functional issue or just an error detection issue.
More broadly, I think some thought and reflection on how we handle complex negations is in order. https://github.com/cerner/clara-rules/issues/343 and https://github.com/cerner/clara-rules/issues/304 are other outstanding issues in this area.
It looks like to-dnf is the culprit here.
clara.test-rules> (com/to-dnf [:not [:and {:type :x, :constraints '[(= ?z (:z this))]}
{:type :y, :constraints '[(= ?z (:z this))]}]])
(:or [:not {:type :x, :constraints [(= ?z (:z this))]}] [:not {:type :y, :constraints [(= ?z (:z this))]}])
The not-and is turned into an or of not conditions; see to-dnf's implementation of this. However, the laws of Boolean algebra don't actually fully apply here since the meaning of each of the terms A and B in [:not [:and [A] [B]]] is dependent on the other term.
I'd expect the extract-negation transformation (which runs before the conversion to DNF) to pull this out into a separate rule that can handle this flow and inserts a NegationResult. So I wonder if we can tweak the logic in in extract-negation to catch this as well.
@rbrush @WilliamParker I'm revising what I said here. I was thinking along the wrong track. Luckily, the discussion on #373 made me realize this.
It does look like analysis happening prior to extraction is an issue. The sorting of conditions is another topic that can factor in, but that's what the other issue is for.
Sorry for my confusion causing any more confusion here. :P
On the Clojurians #clara Slack channel user
enn
reported an session compilation error that didn't make sense in something like the followingExample 1:
On the surface it seemed that this was somehow due to the "negated conjuction" handling done within the compiler, however, the issue is a bit more shallow than that.
Consider this
Example 2:
This has the same exception in the compilation about the variable
?z
being "unbound".Contrast that with
Example 3:
This compiles successfully since
?z
is bound in a condition before the negated condition.I haven't looked closely at the compiler to identify the specific place that relates to this issue, but I think the general idea is that the compiler does not support negated conditions that introduce new variable bindings within a LHS.
In a case like (Example 2)
[:not [:x (= ?z (:z this))]]
it doesn't really make a lot of sense to introduce a new variable binding since it cannot be made visible outside of the:not
- because negation means "no match" of course.However, in the case of a negated conjunction it can make sense to want to join multiple conditions together when performing the negated conjuctive condition. This can be seen in my first example here.
I think the behavior of Example 1 is surprising to find that it doesn't work.