Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

On Wed, Jan 16, 2019 at 8:49 AM James Coleman <jtc331(at)gmail(dot)com> wrote:
>
> On Tue, Jan 15, 2019 at 11:37 PM Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us> wrote:
> > Well, as I said upthread, it seems like we need to think a bit more
> > carefully about what it is that clause_is_strict_for is testing ---
> > and if that ends up finding that some other name is more apposite,
> > I'd not have any hesitation about renaming it. But we're really
> > missing a bet if the ScalarArrayOp-specific check isn't inside that
> > recursive check of an "atomic" expression's properties. The
> > routines above there only recurse through things that act like
> > AND or OR, but clause_is_strict_for is capable of descending
> > through other stuff as long as it's strict in some sense. What
> > we need to be clear about here is exactly what that sense is.
>
> All right, I'll look over all of the other callers and see what makes
> sense as far as naming (or perhaps consider a new parallel function;
> unsure at this point.)

I investigated all of the callers of clause_is_strict_for and
confirmed they fall into two buckets:
- Recursive case inside the function itself.
- Callers proving a variant of IS [NOT] NULL.

Given all cases appear to be safe to extend to scalar array ops, I've
tentatively renamed the function clause_proved_for_null_test and moved
the code back into that function rather than be in the caller. This
also guarantees that beyond proving implication of IS NOT NULL and
refutation of IS NULL we also get proof of weak refutation of strict
predicates (since IS NOT NULL refutes them and we strongly imply IS
NOT NULL); I've added tests for this case.

I added many more comments explaining the proofs here, but it boils
down to the fact that non-empty array ops are really just a strict
clause, and the empty array case isn't strict, but when not returning
NULL returns false, and therefore we can still make the same proofs.

Since the empty array case is really the only interesting one, I
brought back the empty array tests, but modified them to use
calculated/non-constant arrays so that they actually hit the new code
paths. I also verified that the proofs they make are a subset of the
ones we get from existing code for constant empty arrays (it makes
sense we'd be able to prove less about possibly empty arrays than
known empty arrays.)

> I might also try to see if we can edit the tests slightly to require
> the recursion case to be exercised.

I didn't tackle this, but if you think it would add real value, then I
can look into it further.

I also updated the commit message to better match the more extended
implications of this change over just the IS NOT NULL case I was
originally pursuing.

One other thing: for known non-empty arrays we could further extend
this to prove that an IS NULL clause weakly implies the ScalarArrayOp.
I'm not sure this is worth is it; if someone things otherwise let me
know.

James Coleman