Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

On Mon, Jan 14, 2019 at 11:34 AM Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us> wrote:
> >> Hm. That would be annoying, but on reflection I think maybe we don't
> >> actually need to worry about emptiness of the array after all. The
> >> thing that we need to prove, at least for the implication case, is
> >> "truth of the ScalarArrayOp implies truth of the IS NOT NULL clause".
>
> > Are you thinking that implies clause_is_strict_for might not be the
> > right/only place? Or just that the code in that function needs to
> > consider if it should return different results in some cases to handle
> > all 4 proof rules properly?
>
> The latter is what I was envisioning, but I haven't worked out details.

The more that I look at this I'm wondering if there aren't two things
here: it seems that the existing patch (with the code that excludes
empty arrays) is likely useful on its own for cases I hadn't
originally envisioned (or tested). Specifically it seems to allow us
to conclude the result will be null if a field is known to be null. I
think I'll try to add a test specific to this, but I'm not immediately
sure I know a case where that matters. If anyone has an idea on what
direction to head with this, I'd be happy to code it up.

For the original goal of "truth of the ScalarArrayOp implies truth of
the IS NOT NULL clause", it seems to me the proper place is
predicate_implied_by_simple_clause where we already have a place to
specifically work with IS NOT NULL expressions. That will allow this
to be more targeted, work for empty arrays as well, and not
potentially introduce an optimizer bug for strictness with empty
arrays.

I'm attaching an updated patch that does that. I've also added the
"parallel" case in predicate_refuted_by_simple_clause, but I haven't
added a test for that yet. I also would like to add a test for the sad
path to parallel the happy path computed array/cte test.

While I add that though I wanted to get this updated version out to
get feedback on the approach.

James Coleman