Re: Proving IS NOT NULL inference for ScalarArrayOpExpr's

James Coleman <jtc331(at)gmail(dot)com> writes:
> 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.

IIRC, the "foo_holds" outputs mean "the foo relationship appears
to hold for these expressions across all tested inputs", for instance
s_i_holds means "there were no tested cases where A is true and B is not
true". The implied_by/refuted_by outputs mean "predtest.c claims it can
prove this". Obviously, a claimed proof for a relationship that fails
experimentally would be big trouble. The other way around just means
that either the proof rules are inadequate to prove this particular case,
or the set of test values for the expressions don't expose the fact that
the relationship doesn't hold.

Now, if we *expected* that predtest.c should be able to prove something,
failure to do so would be a bug, but it's not a bug if we know it's
incapable of making that proof. The second explanation might represent
a bug in the test case.

I added the foo_holds columns just as a sort of cross-check on the
test cases themselves, they don't test anything about the predtest
code.

regards, tom lane