Teach optimizer's predtest.c more things about ScalarArrayOpExpr.

In particular, make it possible to prove/refute "x IS NULL" and
"x IS NOT NULL" predicates from a clause involving a ScalarArrayOpExpr
even when we are unable or unwilling to deconstruct the expression
into an AND/OR tree.  This avoids a former unexpected degradation of
plan quality when the size of an ARRAY[] expression or array constant
exceeded the arbitrary MAX_SAOP_ARRAY_SIZE limit.  For IS-NULL proofs,
we don't really care about the values of the individual array elements;
at most, we care whether there are any, and for some common cases we
needn't even know that.

The main user-visible effect of this is to let the optimizer recognize
applicability of partial indexes with "x IS NOT NULL" predicates to
queries with "x IN (array)" clauses in some cases where it previously
failed to recognize that.  The structure of predtest.c is such that a
bunch of related proofs will now also succeed, but they're probably
much less useful in the wild.

James Coleman, reviewed by David Rowley

Discussion: https://postgr.es/m/CAAaqYe8yKSvzbyu8w-dThRs9aTFMwrFxn_BkTYeXgjqe3CbNjg@mail.gmail.com

Author: tglsfdc

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.
  */
@@ -1099,8 +1099,8 @@ arrayexpr_cleanup_fn(PredIterInfo info)
  *
  * If the predicate is of the form "foo IS NOT NULL", and we are considering
  * strong implication, we can conclude that the predicate is implied if the
- * clause is strict for "foo", i.e., it must yield NULL when "foo" is NULL.
- * In that case truth of the clause requires that "foo" isn't NULL.
+ * clause is strict for "foo", i.e., it must yield false or NULL when "foo"
+ * is NULL.  In that case truth of the clause ensures that "foo" isn't NULL.
  * (Again, this is a safe conclusion because "foo" must be immutable.)
  * This doesn't work for weak implication, though.
  *
@@ -1131,7 +1131,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... */
@@ -1160,8 +1160,8 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
  *
  * 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).
+ * is strict for "foo", since then the predicate must yield false or NULL
+ * (and since "foo" appears in the predicate, it's known immutable).
  *
  * (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 +1194,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 +1226,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,17 +1293,30 @@ extract_strong_not_arg(Node *clause)
 
 
 /*
- * Can we prove that "clause" returns NULL if "subexpr" does?
+ * Can we prove that "clause" returns NULL (or FALSE) if "subexpr" is
+ * assumed to yield NULL?
  *
- * 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,
- * as this wouldn't hold for volatile expressions.)
+ * In most places in the planner, "strictness" refers to a guarantee that
+ * an expression yields NULL output for a NULL input, and that's mostly what
+ * we're looking for here.  However, at top level where the clause is known
+ * to yield boolean, it may be sufficient to prove that it cannot return TRUE
+ * when "subexpr" is NULL.  The caller should pass allow_false = true when
+ * this weaker property is acceptable.  (When this function recurses
+ * internally, we pass down allow_false = false since we need to prove actual
+ * nullness of the subexpression.)
+ *
+ * We assume that the caller checked that least one of the input expressions
+ * is immutable.  All of the proof rules here involve matching "subexpr" to
+ * some portion of "clause", so that this allows assuming that "subexpr" is
+ * immutable without a separate check.
+ *
+ * The base case is that clause and subexpr are equal().
  *
  * 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.
  */
 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 +1349,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 +1359,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 +1375,89 @@ 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);
+
+	/*
+	 * ScalarArrayOpExpr is a special case.  Note that we'd only reach here
+	 * with a ScalarArrayOpExpr clause if we failed to deconstruct it into an
+	 * AND or OR tree, as for example if it has too many array elements.
+	 */
+	if (IsA(clause, ScalarArrayOpExpr))
+	{
+		ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
+		Node	   *scalarnode = (Node *) linitial(saop->args);
+		Node	   *arraynode = (Node *) lsecond(saop->args);
+
+		/*
+		 * If we can prove the scalar input to be null, and the operator is
+		 * strict, then the SAOP result has to be null --- unless the array is
+		 * empty.  For an empty array, we'd get either false (for ANY) or true
+		 * (for ALL).  So if allow_false = true then the proof succeeds anyway
+		 * for the ANY case; otherwise we can only make the proof if we can
+		 * prove the array non-empty.
+		 */
+		if (clause_is_strict_for(scalarnode, subexpr, false) &&
+			op_strict(saop->opno))
+		{
+			int			nelems = 0;
+
+			if (allow_false && saop->useOr)
+				return true;	/* can succeed even if array is empty */
+
+			if (arraynode && IsA(arraynode, Const))
+			{
+				Const	   *arrayconst = (Const *) arraynode;
+				ArrayType  *arrval;
+
+				/*
+				 * If array is constant NULL then we can succeed, as in the
+				 * case below.
+				 */
+				if (arrayconst->constisnull)
+					return true;
+
+				/* Otherwise, we can compute the number of elements. */
+				arrval = DatumGetArrayTypeP(arrayconst->constvalue);
+				nelems = ArrayGetNItems(ARR_NDIM(arrval), ARR_DIMS(arrval));
+			}
+			else if (arraynode && IsA(arraynode, ArrayExpr) &&
+					 !((ArrayExpr *) arraynode)->multidims)
+			{
+				/*
+				 * We can also reliably count the number of array elements if
+				 * the input is a non-multidim ARRAY[] expression.
+				 */
+				nelems = list_length(((ArrayExpr *) arraynode)->elements);
+			}
+
+			/* Proof succeeds if array is definitely non-empty */
+			if (nelems > 0)
+				return true;
+		}
+
+		/*
+		 * If we can prove the array input to be null, the proof succeeds in
+		 * all cases, since ScalarArrayOpExpr will always return NULL for a
+		 * NULL array.  Otherwise, we're done here.
+		 */
+		return clause_is_strict_for(arraynode, subexpr, false);
+	}
+
+	/*
+	 * When recursing into an expression, we might find a NULL constant.
+	 * That's certainly NULL, whether it matches subexpr or not.
+	 */
+	if (IsA(clause, Const))
+		return ((Const *) clause)->constisnull;
 
 	return false;
 }