On Mon, Feb 18, 2019 at 4:53 PM Tom Lane <t...@sss.pgh.pa.us> wrote:
> So ... this is actively wrong.
>
> This case shows that you can't ignore the empty-array possibility
> for a ScalarArrayOpExpr with useOr = false, because
> "SELECT null::int = all(array[]::int[])" yields TRUE:
>
> contrib_regression=# select * from test_predtest($$
> select x is not null, x = all(array(select i from generate_series(1,0) i))
> from integers
> $$);
> WARNING: strong_implied_by result is incorrect
> -[ RECORD 1 ]-----+--
> strong_implied_by | t
> weak_implied_by | f
> strong_refuted_by | f
> weak_refuted_by | f
> s_i_holds | f
> w_i_holds | f
> s_r_holds | f
> w_r_holds | f
>
> This case shows that you can't ignore the distinction between null
> and false results once you've descended through strict function(s):
>
> contrib_regression=# select * from test_predtest($$
> select x is not null, strictf(true, x = any(array(select i from
> generate_series(1,0) i)))
> from integers
> $$);
> WARNING: strong_implied_by result is incorrect
> -[ RECORD 1 ]-----+--
> strong_implied_by | t
> weak_implied_by | f
> strong_refuted_by | f
> weak_refuted_by | f
> s_i_holds | f
> w_i_holds | f
> s_r_holds | f
> w_r_holds | f
>
> (In this usage, the strictf() function from the test_predtest.sql
> will simply return the NOT of its second input; so it gives different
> answers depending on whether the SAOP returned false or null.)
>
> I think you could probably repair the second problem by adding
> an additional argument to clause_is_strict_for() indicating whether
> it has to prove the clause to be NULL or merely non-TRUE; when
> recursing you'd always have to ask for the former.
I've implemented this fix as suggested. The added argument I've
initially called "allow_false"; I don't love the name, but it is
directly what it does. I'd appreciate other suggestions (if you prefer
it change).
> The first problem could be resolved by insisting on being able to
> prove the array non-empty when !useOr, but I'm not sure if it's
> really worth the trouble, as opposed to just not trying to prove
> anything for !useOr cases. I'm not sure that "x op ALL(ARRAY)"
> occurs often enough in the wild to justify expending code on.
>
> The other case where being able to prove the array nonempty might
> be worth something is when you've recursed and hence need to be
> able to prove the SAOP's result to be NULL not just not-TRUE.
> Again though, I don't know how often that occurs in practice,
> so even the combination of those two motivations might not be
> worth having code to check the array argument.
I've implemented this also; the thing that puts it over the edge for
me on the question of "is it worth it in the wild" is cases like "x
!op ALL(ARRAY)", since it seems plausible to me that that's (unlike
the non-negated case) a reasonably common operation. At the very least
it seems likely to be a more logically interesting operation, which
I'm taking as a proxy for common, I suppose.
> It'd also be worth spending some brain cells on what happens
> when the SAOP's array argument is null overall, which causes
> its result to be null (not false). Maybe the logic goes
> through without needing any explicit test for that case
> (and indeed I couldn't break it in testing that), but it'd
> likely be worth a comment.
Since all SAOPs (both ALL and ANY) return NULL when the array is NULL
regardless of the LHS argument, then this case qualifies as strict.
I've included this in the above fix since both NULL constant arrays
and non-empty arrays can both be proven strict with strict operators.
Ideally I think this case would be handled elsewhere in the optimizer
by directly replacing the saop and a constant NULL array with NULL,
but this isn't the patch to do that, and at any rate I'd have to do a
bit more investigation to understand how to do such (if it's easily
possible).
> I don't especially care for the proposed function name
> "clause_proves_for_null_test". The only thing that brings to my
> mind is the question "proves WHAT, exactly?" --- and as these
> examples show, being crystal clear on what it proves is essential.
Given the new argument, I've reverted the name change.
I also updated the tests with a new helper function "opaque_array" to
make it easy to test cases where the planner can't inspect the array.
That way we don't need to rely on CTEs as an optimization fence --
thus improving both maintainability and readability. I also noticed
there were also some tests where the array was already opaque yet I
was still using CTEs as an optimization fence; I've cleaned those up.
I've updated the comments significantly to reflect the above changes.
I've attached an updated (and rebased) patch.
James Coleman
commit 2cf8f951ca6524d4eb4c927d9903736a0751c89c
Author: jcoleman <jtc...@gmail.com>
Date: Wed Nov 14 16:49:52 2018 +0000
Extend IS [NOT] NULL predicate proofs for arrays
For the purposes of predicate proof testing we limit ScalarArrayOpExpr
decomposition to arrays with <= MAX_SAOP_ARRAY_SIZE items (currently
100 items). Unfortunately this means that we miss opportunities for
proofs with both large and non-constant array expressions.
It's trivially shown that a scalar array op with a known non-empty array
is strict so long its operator is strict; similarly ops with constant
NULL arrays always result in NULL and are therefore strict.
If we don't know an array is NULL or non-empty, things are a bit more
complicated. For ANY ops an empty array results in FALSE, so we can
continue to derive proofs since in the base case we only care about
expressions that result in TRUE for proof correctness.
For ALL ops we can't make any assumptions: if the array isn't known to
be empty or NULL we have to pass on proving [NOT] NULL.
One other exception: once we've recursed through a strict function we
have to require strictness (rather than our relaxed "can be FALSE for
ANY ops" definition in the base case) since a strict function may return
TRUE at arbitrary points.
One of the main benefits of this change is that the planner may now use
partial indexes of the form "WHERE foo IS NOT NULL" when the query's
WHERE clause involves a scalar array op like "foo IN (1,2,...101)" or
"foo != ALL(ARRAY[1,2,...101])".
diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c
index 3c9f245e4d..214a85f701 100644
--- a/src/backend/optimizer/util/predtest.c
+++ b/src/backend/optimizer/util/predtest.c
@@ -99,7 +99,7 @@ static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
bool weak);
static Node *extract_not_arg(Node *clause);
static Node *extract_strong_not_arg(Node *clause);
-static bool clause_is_strict_for(Node *clause, Node *subexpr);
+static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false);
static bool operator_predicate_proof(Expr *predicate, Node *clause,
bool refute_it, bool weak);
static bool operator_same_subexprs_proof(Oid pred_op, Oid clause_op,
@@ -816,7 +816,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
* This function also implements enforcement of MAX_SAOP_ARRAY_SIZE: if a
* ScalarArrayOpExpr's array has too many elements, we just classify it as an
* atom. (This will result in its being passed as-is to the simple_clause
- * functions, which will fail to prove anything about it.) Note that we
+ * functions, many of which will fail to prove anything about it.) Note that we
* cannot just stop after considering MAX_SAOP_ARRAY_SIZE elements; in general
* that would result in wrong proofs, rather than failing to prove anything.
*/
@@ -1104,6 +1104,14 @@ arrayexpr_cleanup_fn(PredIterInfo info)
* (Again, this is a safe conclusion because "foo" must be immutable.)
* This doesn't work for weak implication, though.
*
+ * Similarly predicates of the form "foo IS NOT NULL" are strongly implied by
+ * the truthfulness of OR'd ScalarArrayOpExpr's since with non-empty arrays they
+ * are strict and empty arrays results in false which won't prove anything anyway.
+ * They are also implied by AND'd ScalarArrayOpExpr's as long as the array is
+ * known to be NULL or non-empty. However weak implication fails: e.g.,
+ * "NULL IS NOT NULL" is false, but "NULL = ANY(ARRAY[NULL])" is NULL, so
+ * non-falsity does not imply non-falsity.
+ *
* Finally, if both clauses are binary operator expressions, we may be able
* to prove something using the system's knowledge about operators; those
* proof rules are encapsulated in operator_predicate_proof().
@@ -1131,7 +1139,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
!ntest->argisrow)
{
/* strictness of clause for foo implies foo IS NOT NULL */
- if (clause_is_strict_for(clause, (Node *) ntest->arg))
+ if (clause_is_strict_for(clause, (Node *) ntest->arg, true))
return true;
}
return false; /* we can't succeed below... */
@@ -1158,10 +1166,16 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
* implication case), or is "foo IS NOT NULL". That works for either strong
* or weak refutation.
*
+ * Similarly, predicates of the form "foo IS NULL" are refuted by the
+ * truthfulness of OR'd and AND'd (with known NULL or non-empty arrays)
+ * ScalarArrayOpExpr's. Unlike implication, this also holds for weak refutation
+ * since empty arrays result in false and thus won't prove anything anyway.
+ *
* A clause "foo IS NULL" refutes a predicate "foo IS NOT NULL" in all cases.
* If we are considering weak refutation, it also refutes a predicate that
* is strict for "foo", since then the predicate must yield NULL (and since
- * "foo" appears in the predicate, it's known immutable).
+ * "foo" appears in the predicate, it's known immutable). ScalarArrayOpExpr's
+ * that strongly imply "foo IS NOT NULL" also weakly refute strict predicates.
*
* (The main motivation for covering these IS [NOT] NULL cases is to support
* using IS NULL/IS NOT NULL as partition-defining constraints.)
@@ -1194,7 +1208,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
return false;
/* strictness of clause for foo refutes foo IS NULL */
- if (clause_is_strict_for(clause, (Node *) isnullarg))
+ if (clause_is_strict_for(clause, (Node *) isnullarg, true))
return true;
/* foo IS NOT NULL refutes foo IS NULL */
@@ -1226,7 +1240,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
/* foo IS NULL weakly refutes any predicate that is strict for foo */
if (weak &&
- clause_is_strict_for((Node *) predicate, (Node *) isnullarg))
+ clause_is_strict_for((Node *) predicate, (Node *) isnullarg, true))
return true;
return false; /* we can't succeed below... */
@@ -1293,7 +1307,9 @@ extract_strong_not_arg(Node *clause)
/*
- * Can we prove that "clause" returns NULL if "subexpr" does?
+ * Most of this method proves that a clause is strict for a given expression.
+ * That is, it answers the question: Can we prove that "clause" returns NULL if
+ * "subexpr" does?
*
* The base case is that clause and subexpr are equal(). (We assume that
* the caller knows at least one of the input expressions is immutable,
@@ -1301,9 +1317,32 @@ extract_strong_not_arg(Node *clause)
*
* We can also report success if the subexpr appears as a subexpression
* of "clause" in a place where it'd force nullness of the overall result.
+ *
+ * ScalarArrayOpExpr's are a special case. With the exception of empty arrays
+ * we can treat them as any other operator expression and verify strictness of
+ * the operator.
+ *
+ * However an empty array results in either false (for ANY) or true (for ALL).
+ * Because the result is a real boolean (instead of NULL) even when when the
+ * argument is NULL, scalar array ops aren't actually strict.
+ *
+ * We can safely ignore this in the base case for ANY since the predicate proofs
+ * of implication and refutation both only matter when the expression is true;
+ * we are able to prove claims about "IS [NOT] NULL" clauses anyway. The same
+ * holds true if the array itself is NULL since the result is always NULL.
+ *
+ * In constrast the ALL base case requires us to additionally prove the array
+ * is not empty since a TRUE result means the implication or refutation must
+ * hold. We can also prove for known NULL arrays since the result is always
+ * NULL.
+ *
+ * In both cases we have to fallback to requiring fully strict behavior (and
+ * thus be able to prove the array is either non-empty or NULL) as soon as we've
+ * recursed through a strict function (since such a function is free to return
+ * TRUE at any point so long as the argument is NOT NULL).
*/
static bool
-clause_is_strict_for(Node *clause, Node *subexpr)
+clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
{
ListCell *lc;
@@ -1336,7 +1375,7 @@ clause_is_strict_for(Node *clause, Node *subexpr)
{
foreach(lc, ((OpExpr *) clause)->args)
{
- if (clause_is_strict_for((Node *) lfirst(lc), subexpr))
+ if (clause_is_strict_for((Node *) lfirst(lc), subexpr, false))
return true;
}
return false;
@@ -1346,7 +1385,7 @@ clause_is_strict_for(Node *clause, Node *subexpr)
{
foreach(lc, ((FuncExpr *) clause)->args)
{
- if (clause_is_strict_for((Node *) lfirst(lc), subexpr))
+ if (clause_is_strict_for((Node *) lfirst(lc), subexpr, false))
return true;
}
return false;
@@ -1362,16 +1401,66 @@ clause_is_strict_for(Node *clause, Node *subexpr)
*/
if (IsA(clause, CoerceViaIO))
return clause_is_strict_for((Node *) ((CoerceViaIO *) clause)->arg,
- subexpr);
+ subexpr, false);
if (IsA(clause, ArrayCoerceExpr))
return clause_is_strict_for((Node *) ((ArrayCoerceExpr *) clause)->arg,
- subexpr);
+ subexpr, false);
if (IsA(clause, ConvertRowtypeExpr))
return clause_is_strict_for((Node *) ((ConvertRowtypeExpr *) clause)->arg,
- subexpr);
+ subexpr, false);
if (IsA(clause, CoerceToDomain))
return clause_is_strict_for((Node *) ((CoerceToDomain *) clause)->arg,
- subexpr);
+ subexpr, false);
+
+ /*
+ * Since we limit decomposing ScalarArrayOpExpr nodes into AND/OR quals
+ * to arrays having at most MAX_SAOP_ARRAY_SIZE items, we need to handle
+ * large arrays separately (this is also useful for non-constant array
+ * expressions).
+ */
+ if (clause && IsA(clause, ScalarArrayOpExpr))
+ {
+ ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
+ if (op_strict(saop->opno) &&
+ clause_is_strict_for((Node *) linitial(saop->args), subexpr, false))
+ {
+ if (!allow_false|| !saop->useOr)
+ {
+ Node *arraynode = (Node *) lsecond(saop->args);
+ int nelems = 0;
+
+ if (arraynode && IsA(arraynode, Const))
+ {
+ ArrayType *arrval;
+ Const *arrayconst = (Const *) arraynode;
+ /*
+ * Scalar array ops with NULL array constants always result
+ * in NULL so are strict.
+ */
+ if (arrayconst->constisnull)
+ return true;
+
+ arrval = DatumGetArrayTypeP(arrayconst->constvalue);
+ nelems = ArrayGetNItems(ARR_NDIM(arrval), ARR_DIMS(arrval));
+ }
+ else if (arraynode && IsA(arraynode, ArrayExpr) &&
+ !((ArrayExpr *) arraynode)->multidims)
+ nelems = list_length(((ArrayExpr *) arraynode)->elements);
+
+ /*
+ * Empty AND/OR groups resolve to TRUE or FALSE rather than null,
+ * so in addition to verifying the operation is otherwise strict,
+ * we also have to verify we have a non-empty array.
+ */
+ if (nelems > 0)
+ return true;
+ else
+ return false;
+ }
+ else
+ return true;
+ }
+ }
return false;
}
diff --git a/src/test/modules/test_predtest/expected/test_predtest.out b/src/test/modules/test_predtest/expected/test_predtest.out
index 5574e03204..11e635a30a 100644
--- a/src/test/modules/test_predtest/expected/test_predtest.out
+++ b/src/test/modules/test_predtest/expected/test_predtest.out
@@ -19,6 +19,9 @@ from generate_series(0, 11*11-1) i;
-- and a simple strict function that's opaque to the optimizer
create function strictf(bool, bool) returns bool
language plpgsql as $$begin return $1 and not $2; end$$ strict;
+-- a simple function make arrays opaque to the optimizer
+create function opaque_array(int[]) returns int[]
+language plpgsql as $$begin return $1; end$$ strict;
-- Basic proof rules for single boolean variables
select * from test_predtest($$
select x, x
@@ -837,3 +840,556 @@ w_i_holds | f
s_r_holds | f
w_r_holds | f
+-- For the next several tests, we want to test an array longer than
+-- MAX_SAOP_ARRAY_SIZE so that we're not relying on predtest turning the
+-- array op into set of AND/OR quals. We also need test empty arrays since
+-- they are the case that deviates from this being merely a check for the
+-- clause being strict.
+--
+-- We also want to include test cases for non-constant array expressions.
+--
+-- Tests employing (x + x) to verify we don't infer implication or
+-- refutation of "strict_func(x) IS [NOT] NULL" from "x IS [NOT] NULL"
+-- will show *_holds=t even when *_by=f because int4pl never returns
+-- NULL unless an operand is NULL, but we can't assume this is true
+-- of all functions.
+--
+-- For tests using constant arrays the planner can inspect (i.e., not hidden
+-- behind an optimization fence like a CTE) we include NULL in our array
+-- for completeness's sake *unless* testing ALL since that would there it
+-- would force the expression to NULL which makes it generally less useful
+-- as a test case.
+--
+-- ScalarArrayOp implies IS NOT NULL
+select * from test_predtest($$
+select x is not null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is not null, x != all(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select y is not null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select (x + x) is not null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is not null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select y is not null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select (x + x) is not null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is not null, x = any(opaque_array(array[]::int[]))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | t
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select x is not null, x = all(opaque_array(array[]::int[]))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is not null, strictf(true, x = any(opaque_array(array[]::int[])))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is not null, strictf(true, x = all(null::int[]))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+-- ScalarArrayOp refutes IS NULL
+select * from test_predtest($$
+select x is null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | t
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select x is null, x != all(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | t
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select y is null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select (x + x) is null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select x is null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | t
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select y is null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select (x + x) is null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select x is null, x = any(opaque_array(array[]::int[]))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | t
+weak_refuted_by | t
+s_i_holds | t
+w_i_holds | t
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select x is null, x = all(opaque_array(array[]::int[]))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is null, strictf(true, x = any(opaque_array(array[]::int[])))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x is null, strictf(true, x = all(null::int[]))
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | t
+weak_refuted_by | t
+s_i_holds | t
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+-- Strict predicate weakly refutes ScalarArrayOp
+--
+-- We get w_i_holds despite not declaring weak_implied_by, but
+-- a simple case (not tested here) shows why this isn't desired:
+-- "(NULL IS NULL)" is true while "= ANY(ARRAY[])" is false.
+select * from test_predtest($$
+select x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+]), x is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | t
+
+select * from test_predtest($$
+select x != all(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101
+]), x is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | t
+
+select * from test_predtest($$
+select x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+]), y is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+]), (x + x) is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | t
+
+select * from test_predtest($$
+select x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+), x is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | t
+
+select * from test_predtest($$
+select x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+), y is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | f
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+), (x + x) is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | t
+
+select * from test_predtest($$
+select x = any(opaque_array(array[]::int[])), x is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | f
+s_r_holds | t
+w_r_holds | t
+
+select * from test_predtest($$
+select x = all(opaque_array(array[]::int[])), x is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | f
+s_i_holds | t
+w_i_holds | t
+s_r_holds | f
+w_r_holds | f
+
+select * from test_predtest($$
+select x = all(null::int[]), x is null
+from integers
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by | f
+strong_refuted_by | f
+weak_refuted_by | t
+s_i_holds | f
+w_i_holds | t
+s_r_holds | f
+w_r_holds | t
+
diff --git a/src/test/modules/test_predtest/sql/test_predtest.sql b/src/test/modules/test_predtest/sql/test_predtest.sql
index 2734735843..67160f3d83 100644
--- a/src/test/modules/test_predtest/sql/test_predtest.sql
+++ b/src/test/modules/test_predtest/sql/test_predtest.sql
@@ -25,6 +25,10 @@ from generate_series(0, 11*11-1) i;
create function strictf(bool, bool) returns bool
language plpgsql as $$begin return $1 and not $2; end$$ strict;
+-- a simple function make arrays opaque to the optimizer
+create function opaque_array(int[]) returns int[]
+language plpgsql as $$begin return $1; end$$ strict;
+
-- Basic proof rules for single boolean variables
select * from test_predtest($$
@@ -325,3 +329,268 @@ select * from test_predtest($$
select x <= y, x = any(array[1,3,y])
from integers
$$);
+
+-- For the next several tests, we want to test an array longer than
+-- MAX_SAOP_ARRAY_SIZE so that we're not relying on predtest turning the
+-- array op into set of AND/OR quals. We also need test empty arrays since
+-- they are the case that deviates from this being merely a check for the
+-- clause being strict.
+--
+-- We also want to include test cases for non-constant array expressions.
+--
+-- Tests employing (x + x) to verify we don't infer implication or
+-- refutation of "strict_func(x) IS [NOT] NULL" from "x IS [NOT] NULL"
+-- will show *_holds=t even when *_by=f because int4pl never returns
+-- NULL unless an operand is NULL, but we can't assume this is true
+-- of all functions.
+--
+-- For tests using constant arrays the planner can inspect (i.e., not hidden
+-- behind an optimization fence like a CTE) we include NULL in our array
+-- for completeness's sake *unless* testing ALL since that would there it
+-- would force the expression to NULL which makes it generally less useful
+-- as a test case.
+--
+-- ScalarArrayOp implies IS NOT NULL
+select * from test_predtest($$
+select x is not null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, x != all(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select y is not null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select (x + x) is not null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+
+select * from test_predtest($$
+select y is not null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+
+select * from test_predtest($$
+select (x + x) is not null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, x = any(opaque_array(array[]::int[]))
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, x = all(opaque_array(array[]::int[]))
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, strictf(true, x = any(opaque_array(array[]::int[])))
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, strictf(true, x = all(null::int[]))
+from integers
+$$);
+
+-- ScalarArrayOp refutes IS NULL
+select * from test_predtest($$
+select x is null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, x != all(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select y is null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select (x + x) is null, x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+])
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+
+select * from test_predtest($$
+select y is null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+
+select * from test_predtest($$
+select (x + x) is null, x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+)
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, x = any(opaque_array(array[]::int[]))
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, x = all(opaque_array(array[]::int[]))
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, strictf(true, x = any(opaque_array(array[]::int[])))
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, strictf(true, x = all(null::int[]))
+from integers
+$$);
+
+-- Strict predicate weakly refutes ScalarArrayOp
+--
+-- We get w_i_holds despite not declaring weak_implied_by, but
+-- a simple case (not tested here) shows why this isn't desired:
+-- "(NULL IS NULL)" is true while "= ANY(ARRAY[])" is false.
+select * from test_predtest($$
+select x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+]), x is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x != all(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101
+]), x is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+]), y is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = any(array[
+ 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,
+ 29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,
+ 54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,
+ 79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,null
+]), (x + x) is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+), x is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+), y is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = any(
+ (select array_agg(i) || null from generate_series(1, 101) t(i))::int[]
+), (x + x) is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = any(opaque_array(array[]::int[])), x is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = all(opaque_array(array[]::int[])), x is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x = all(null::int[]), x is null
+from integers
+$$);
