Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

On Tue, Jan 15, 2019 at 12:47 AM David Rowley
<david(dot)rowley(at)2ndquadrant(dot)com> wrote:
> 1. In:
>
> + if (IsA(clause, ScalarArrayOpExpr))
> + {
> + ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
> + Node *subexpr = (Node *) ((NullTest *) predicate)->arg;
> + if (op_strict(saop->opno) &&
> + clause_is_strict_for((Node *) linitial(saop->args), subexpr))
> + return true;
> + }
> +
> /* foo IS NOT NULL refutes foo IS NULL */
> if (clause && IsA(clause, NullTest) &&
>
> Your IsA(clause, ScalarArrayOpExpr) condition should also be checking
> that "clause" can't be NULL. The NullTest condition one below does
> this.

Fixed in my local copy. I also did the same in
predicate_implied_by_simple_clause since it seems to have the same
potential issue.

After sleeping on it and looking at it again this morning, I also
realized I need to exclude weak implication in
predicate_refuted_by_simple_clause.

> 2. I was also staring predicate_implied_by_simple_clause() a bit at
> the use of clause_is_strict_for() to ensure that the IS NOT NULL's
> operand matches the ScalarArrayOpExpr left operand. Since
> clause_is_strict_for() = "Can we prove that "clause" returns NULL if
> "subexpr" does?", in this case, your clause is the ScalarArrayOpExpr's
> left operand and subexpr is the IS NOT NULL's operand. This means
> that a partial index with "WHERE a IS NOT NULL" should also be fine to
> use for WHERE strict_func(a) IN (1,2,..., 101); since strict_func(a)
> must be NULL if a is NULL. Also also works for WHERE a+a
> IN(1,2,...,101); I wonder if it's worth adding a test for that, or
> even just modify one of the existing tests to ensure you get the same
> result from it. Perhaps it's worth an additional test to ensure that x
> IN(1,2,...,101) does not imply x+x IS NOT NULL and maybe that x+x IS
> NULL does not refute x IN(1,2,...,101), as a strict function is free
> to return NULL even if it's input are not NULL.

Are you suggesting a different test than clause_is_strict_for to
verify the saop LHS is the same as the null test's arg? I suppose we
could use "equal()" instead?

I've added several tests, and noticed a few things:

1. The current code doesn't result in "strongly_implied_by = t" for
the "(x + x) is not null" case, but it does result in "s_i_holds = t".
This doesn't change if I switch to using "equal()" as mentioned above.

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

3. The tests I have for refuting "(x + x) is null" show that both
s_r_holds and w_r_holds. I'd expected these to be false.

I'm attaching the current version of the patch with the new tests, but
I'm not sure I understand the *_holds results mentioned above. Are
they an artifact of the data under test? Or do they suggest a
remaining bug? I'm a bit fuzzy on what to expect for *_holds though I
understand the requirements for strongly/weakly_implied/refuted_by.

James Coleman