commit d899833f8d329610a237d2269ac4580b27a709d2 Author: jcoleman 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 to prove with both large and non-constant array expressions. But it turns out that all IS [NOT] NULL proofs we already derive for strict clauses are valid for ScalarArrayOpExpr's with strict operators despite the fact that array ops are not guaranteed to be strict (empty arrays can result in false when the LHS is null). 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)". diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c index 3d5ef6922c..fab90d97c4 100644 --- a/src/backend/optimizer/util/predtest.c +++ b/src/backend/optimizer/util/predtest.c @@ -98,7 +98,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_proves_for_null_test(Node *clause, Node *subexpr); 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, @@ -815,7 +815,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. */ @@ -1103,6 +1103,12 @@ 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 ScalarArrayOpExpr's since with non-empty arrays they are + * strict and empty arrays results in false which won't prove anything anyway. + * 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(). @@ -1130,7 +1136,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_proves_for_null_test(clause, (Node *) ntest->arg)) return true; } return false; /* we can't succeed below... */ @@ -1157,10 +1163,17 @@ 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 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). Because + * ScalarArrayOpExpr's strongly imply "foo IS NOT NULL", they 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.) @@ -1193,7 +1206,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_proves_for_null_test(clause, (Node *) isnullarg)) return true; /* foo IS NOT NULL refutes foo IS NULL */ @@ -1225,7 +1238,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_proves_for_null_test((Node *) predicate, (Node *) isnullarg)) return true; return false; /* we can't succeed below... */ @@ -1292,7 +1305,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, @@ -1300,9 +1315,17 @@ 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 false rather than NULL when + * the argument is NULL, so these ops aren't actually strict. But since our + * 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. */ static bool -clause_is_strict_for(Node *clause, Node *subexpr) +clause_proves_for_null_test(Node *clause, Node *subexpr) { ListCell *lc; @@ -1335,7 +1358,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_proves_for_null_test((Node *) lfirst(lc), subexpr)) return true; } return false; @@ -1345,12 +1368,26 @@ clause_is_strict_for(Node *clause, Node *subexpr) { foreach(lc, ((FuncExpr *) clause)->args) { - if (clause_is_strict_for((Node *) lfirst(lc), subexpr)) + if (clause_proves_for_null_test((Node *) lfirst(lc), subexpr)) return true; } return 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_proves_for_null_test((Node *) linitial(saop->args), subexpr)) + 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..046bb3942c 100644 --- a/src/test/modules/test_predtest/expected/test_predtest.out +++ b/src/test/modules/test_predtest/expected/test_predtest.out @@ -837,3 +837,393 @@ w_i_holds | f s_r_holds | f w_r_holds | f +-- For the next few 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. +-- +-- 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 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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x is not null, x = any((select vals from a)::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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select y is not null, x = any((select vals from a)::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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select (x + x) is not null, x = any((select vals from a)::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($$ +with a(vals) as (select array[]::int[]) +select x is not null, x = any((select vals from a)::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 + +-- 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 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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x is null, x = any((select vals from a)::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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select y is null, x = any((select vals from a)::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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select (x + x) is null, x = any((select vals from a)::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($$ +with a(vals) as (select array[]::int[]) +select x is null, x = any((select vals from a)::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 + +-- 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 = 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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x = any((select vals from a)::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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x = any((select vals from a)::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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x = any((select vals from a)::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($$ +with a(vals) as (select array[]::int[]) +select x = any((select vals from a)::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 + diff --git a/src/test/modules/test_predtest/sql/test_predtest.sql b/src/test/modules/test_predtest/sql/test_predtest.sql index 2734735843..10198b27d7 100644 --- a/src/test/modules/test_predtest/sql/test_predtest.sql +++ b/src/test/modules/test_predtest/sql/test_predtest.sql @@ -325,3 +325,204 @@ select * from test_predtest($$ select x <= y, x = any(array[1,3,y]) from integers $$); + +-- For the next few 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. +-- +-- 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 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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x is not null, x = any((select vals from a)::int[]) +from integers +$$); + +select * from test_predtest($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select y is not null, x = any((select vals from a)::int[]) +from integers +$$); + +select * from test_predtest($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select (x + x) is not null, x = any((select vals from a)::int[]) +from integers +$$); + +select * from test_predtest($$ +with a(vals) as (select array[]::int[]) +select x is not null, x = any((select vals from a)::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 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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x is null, x = any((select vals from a)::int[]) +from integers +$$); + +select * from test_predtest($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select y is null, x = any((select vals from a)::int[]) +from integers +$$); + +select * from test_predtest($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select (x + x) is null, x = any((select vals from a)::int[]) +from integers +$$); + +select * from test_predtest($$ +with a(vals) as (select array[]::int[]) +select x is null, x = any((select vals from a)::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 = 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($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x = any((select vals from a)::int[]), x is null +from integers +$$); + +select * from test_predtest($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x = any((select vals from a)::int[]), y is null +from integers +$$); + +select * from test_predtest($$ +with a(vals) as ( + select array_agg(i) || null from generate_series(1, 101) t(i) +) +select x = any((select vals from a)::int[]), (x + x) is null +from integers +$$); + +select * from test_predtest($$ +with a(vals) as (select array[]::int[]) +select x = any((select vals from a)::int[]), x is null +from integers +$$);