Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

On Tue, Jan 15, 2019 at 3:53 PM Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us> wrote:
>
> James Coleman <jtc331(at)gmail(dot)com> writes:
> > [ saop_is_not_null-v6.patch ]
>
> I quite dislike taking the responsibility out of clause_is_strict_for
> and putting it in the callers. Aside from requiring duplicative code,
> it means that this fails to prove anything for recursive situations
> (i.e., where the ScalarArrayOp appears one or more levels down in a
> clause examined by clause_is_strict_for).
>
> If the behavior needs to vary depending on proof rule, which it
> looks like it does, the way to handle that is to add flag argument(s)
> to clause_is_strict_for.

The reason I moved it was that we're no longer just proving
strictness, so it seemed odd to put it in a function specifically
named to be about proving strictness.

If you'd prefer an argument like "bool allow_false" or "bool
check_saop_implies_is_null" I'm happy to make that change, but it
seems generally unhelpful to change the function implementation to
contradict the name (the empty array case that returns false even then
the lhs is null).

> I'm also not happy about the lack of comments justifying the proof
> rules -- eg, it's far from obvious why you need to restrict one
> case to !weak but not the other.

Both implication and refutation have the !weak check; it's just that
the check in the implication function was already present.

I'll add more comments inline for the proof rules, but from what I can
tell only strong implication holds for implication of IS NOT NULL. A
sample case disproving weak implication is "select null is not null,
null::int = any(array[null]::int[])" which results in "false, null",
so non-falsity does not imply non-falsity.

However I'm currently unable to come up with a case for refutation
such that truth of a ScalarArrayOp refutes IS NULL, so I'll update
code and tests for that. That also takes care of my point:

James Coleman <jtc331(at)gmail(dot)com> writes:
> 2. The tests I have for refuting "x is null" show that w_r_holds as
> well as s_r_holds. I'd only expected the latter, since only
> "strongly_refuted_by = t".

But it still leaves my questions (1) and (3).

James Coleman