Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

James Coleman <jtc331(at)gmail(dot)com> writes:
> On Mon, Jan 14, 2019 at 11:08 AM Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us> wrote:
>> I think these test cases don't actually prove much about the behavior
>> of your patch. Wouldn't they be handled by the generic OR-conversion
>> logic, since there's fewer than MAX_SAOP_ARRAY_SIZE items?

> Which ones are you looking at in particular? The "inline" (non-cte)
> happy and sad path cases have 102 total array elements (as does the
> happy path cte case), and MAX_SAOP_ARRAY_SIZE is 100. The other two
> tests are about the empty array case so much have 0 items (and were
> the ones that showed different behavior between v3 and v4).

I was looking at the empty-array ones. I don't see how that reaches
your patch; we should not be doing predicate_implied_by_simple_clause
on the ScalarArrayOp itself, because predicate_classify should've
decided to treat it as an OR clause.

>> 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.

regards, tom lane