Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's - Mailing list pgsql-hackers

From James Coleman
Subject Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's
Date
Msg-id CAAaqYe-6RdE8Zv41hRbMtPEmA7uyyOVdt+jVs0=B=MmjdRNGJg@mail.gmail.com
Whole thread Raw
In response to Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's  (David Rowley <david.rowley@2ndquadrant.com>)
Responses Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's
List pgsql-hackers
On Tue, Jan 15, 2019 at 8:14 PM David Rowley
<david.rowley@2ndquadrant.com> wrote:
>
> On Wed, 16 Jan 2019 at 14:05, James Coleman <jtc331@gmail.com> wrote:
> > At the risk of missing something obvious, I'm not sure I see a case
> > where "x is not null" does not imply "(x + x) is not null", at least
> > for integers. Since an integer + an integer results in an integer,
> > then it must imply the addition of itself is not null also?
>
> A strict function guarantees it will return NULL on any NULL input.
> This does not mean it can't return NULL on a non-NULL input.
>
> While int4pl might do what you want, some other strict function might
> not. A simple example would be a strict function that decided to
> return NULL when the two ints combined overflowed int.

Yes, the claim about not all strict functions guarantee this (like
int4pl) made sense.

Is your preference in this kind of case to comment the code and/or
tests but stick with int4pl even though it doesn't demonstrate the
"problem", or try to engineer a different test case such that the
*_holds results in the tests don't seem to imply we could prove more
things than we do?

James Coleman


pgsql-hackers by date:

Previous
From: David Rowley
Date:
Subject: Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's
Next
From: David Rowley
Date:
Subject: Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's