On Wed, Jan 16, 2019 at 8:49 AM James Coleman <jtc...@gmail.com> wrote: > > On Tue, Jan 15, 2019 at 11:37 PM Tom Lane <t...@sss.pgh.pa.us> wrote: > > Well, as I said upthread, it seems like we need to think a bit more > > carefully about what it is that clause_is_strict_for is testing --- > > and if that ends up finding that some other name is more apposite, > > I'd not have any hesitation about renaming it. But we're really > > missing a bet if the ScalarArrayOp-specific check isn't inside that > > recursive check of an "atomic" expression's properties. The > > routines above there only recurse through things that act like > > AND or OR, but clause_is_strict_for is capable of descending > > through other stuff as long as it's strict in some sense. What > > we need to be clear about here is exactly what that sense is. > > All right, I'll look over all of the other callers and see what makes > sense as far as naming (or perhaps consider a new parallel function; > unsure at this point.)
I investigated all of the callers of clause_is_strict_for and confirmed they fall into two buckets: - Recursive case inside the function itself. - Callers proving a variant of IS [NOT] NULL. Given all cases appear to be safe to extend to scalar array ops, I've tentatively renamed the function clause_proved_for_null_test and moved the code back into that function rather than be in the caller. This also guarantees that beyond proving implication of IS NOT NULL and refutation of IS NULL we also get proof of weak refutation of strict predicates (since IS NOT NULL refutes them and we strongly imply IS NOT NULL); I've added tests for this case. I added many more comments explaining the proofs here, but it boils down to the fact that non-empty array ops are really just a strict clause, and the empty array case isn't strict, but when not returning NULL returns false, and therefore we can still make the same proofs. Since the empty array case is really the only interesting one, I brought back the empty array tests, but modified them to use calculated/non-constant arrays so that they actually hit the new code paths. I also verified that the proofs they make are a subset of the ones we get from existing code for constant empty arrays (it makes sense we'd be able to prove less about possibly empty arrays than known empty arrays.) > I might also try to see if we can edit the tests slightly to require > the recursion case to be exercised. I didn't tackle this, but if you think it would add real value, then I can look into it further. I also updated the commit message to better match the more extended implications of this change over just the IS NOT NULL case I was originally pursuing. One other thing: for known non-empty arrays we could further extend this to prove that an IS NULL clause weakly implies the ScalarArrayOp. I'm not sure this is worth is it; if someone things otherwise let me know. James Coleman
saop_is_not_null-v7.patch
Description: Binary data
