First, notin must be special-cased in rewrite. Here's why. Currently, the non-monotonicity detection logic checks the op against a standard whitelist. In an expression such as "x <= a.b.c.notin(d)", where a.b.c is a fully qualified collection name, we introduce a a negative depenency between x and a.b.c, since the op "notin" is not in the whitelist. The situation is exactly the reverse in this case .. there should be a positive dependency between x and a.b.c, but a negative dependency between x and d.
Second, the PushNotIn element waits until stratum_end to push out its results.
So, in a set of rules like this:
x <= y.notin(z)
u <= x
.. the table x gets the correct result at the end of the stratum, but by that time it has already exit the fixpoint loop, and u never gets to see the changes to x.
There are two errors in processing notin.
First, notin must be special-cased in rewrite. Here's why. Currently, the non-monotonicity detection logic checks the op against a standard whitelist. In an expression such as "x <= a.b.c.notin(d)", where a.b.c is a fully qualified collection name, we introduce a a negative depenency between x and a.b.c, since the op "notin" is not in the whitelist. The situation is exactly the reverse in this case .. there should be a positive dependency between x and a.b.c, but a negative dependency between x and d.
Second, the PushNotIn element waits until stratum_end to push out its results. So, in a set of rules like this:
.. the table x gets the correct result at the end of the stratum, but by that time it has already exit the fixpoint loop, and u never gets to see the changes to x.