Improve predtest.c's internal docs, and enhance its functionality a bit.

Commit b08df9cab left things rather poorly documented as far as the
exact semantics of "clause_is_check" mode went.  Also, that mode did
not really work correctly for predicate_refuted_by; although given the
lack of specification as to what it should do, as well as the lack
of any actual use-case, that's perhaps not surprising.

Rename "clause_is_check" to "weak" proof mode, and provide specifications
for what it should do.  I defined weak refutation as meaning "truth of A
implies non-truth of B", which makes it possible to use the mode in the
part of relation_excluded_by_constraints that checks for mutually
contradictory WHERE clauses.  Fix up several places that did things wrong
for that definition.  (As far as I can see, these errors would only lead
to failure-to-prove, not incorrect claims of proof, making them not
serious bugs even aside from the fact that v10 contains no use of this
mode.  So there seems no need for back-patching.)

In addition, teach predicate_refuted_by_recurse that it can use
predicate_implied_by_recurse after all when processing a strong NOT-clause,
so long as it asks for the correct proof strength.  This is an optimization
that could have been included in commit b08df9cab, but wasn't.

Also, simplify and generalize the logic that checks for whether nullness of
the argument of IS [NOT] NULL would force overall nullness of the predicate
or clause.  (This results in a change in the partition_prune test's output,
as it is now able to prune an all-nulls partition that it did not recognize
before.)

In passing, in PartConstraintImpliedByRelConstraint, remove bogus
conversion of the constraint list to explicit-AND form and then right back
again; that accomplished nothing except forcing a useless extra level of
recursion inside predicate_implied_by.

Discussion: https://postgr.es/m/5983.1520487191@sss.pgh.pa.us

src/backend/commands/tablecmds.c

@@ -13651,10 +13651,11 @@ ComputePartitionAttrs(Relation rel, List *partParams, AttrNumber *partattrs,
 
 /*
  * PartConstraintImpliedByRelConstraint
- *		Does scanrel's existing constraints imply the partition constraint?
+ *		Do scanrel's existing constraints imply the partition constraint?
  *
- * Existing constraints includes its check constraints and column-level
+ * "Existing constraints" include its check constraints and column-level
- * NOT NULL constraints and partConstraint describes the partition constraint.
+ * NOT NULL constraints.  partConstraint describes the partition constraint,
+ * in implicit-AND form.
  */
 bool
 PartConstraintImpliedByRelConstraint(Relation scanrel,
@@ -13724,10 +13725,15 @@ PartConstraintImpliedByRelConstraint(Relation scanrel,
 									  make_ands_implicit((Expr *) cexpr));
 	}
 
-	if (existConstraint != NIL)
+	/*
-		existConstraint = list_make1(make_ands_explicit(existConstraint));
+	 * Try to make the proof.  Since we are comparing CHECK constraints, we
-
+	 * need to use weak implication, i.e., we assume existConstraint is
-	/* And away we go ... */
+	 * not-false and try to prove the same for partConstraint.
+	 *
+	 * Note that predicate_implied_by assumes its first argument is known
+	 * immutable.  That should always be true for partition constraints, so we
+	 * don't test it here.
+	 */
 	return predicate_implied_by(partConstraint, existConstraint, true);
 }
 

src/backend/optimizer/util/plancat.c

@@ -1421,7 +1421,11 @@ relation_excluded_by_constraints(PlannerInfo *root,
 			safe_restrictions = lappend(safe_restrictions, rinfo->clause);
 	}
 
-	if (predicate_refuted_by(safe_restrictions, safe_restrictions, false))
+	/*
+	 * We can use weak refutation here, since we're comparing restriction
+	 * clauses with restriction clauses.
+	 */
+	if (predicate_refuted_by(safe_restrictions, safe_restrictions, true))
 		return true;
 
 	/*
@@ -1469,6 +1473,9 @@ relation_excluded_by_constraints(PlannerInfo *root,
 	 * an obvious optimization.  Some of the clauses might be OR clauses that
 	 * have volatile and nonvolatile subclauses, and it's OK to make
 	 * deductions with the nonvolatile parts.
+	 *
+	 * We need strong refutation because we have to prove that the constraints
+	 * would yield false, not just NULL.
 	 */
 	if (predicate_refuted_by(safe_constraints, rel->baserestrictinfo, false))
 		return true;

src/backend/optimizer/util/predtest.c

@@ -78,9 +78,9 @@ typedef struct PredIterInfoData
 
 
 static bool predicate_implied_by_recurse(Node *clause, Node *predicate,
-							 bool clause_is_check);
+							 bool weak);
 static bool predicate_refuted_by_recurse(Node *clause, Node *predicate,
-							 bool clause_is_check);
+							 bool weak);
 static PredClass predicate_classify(Node *clause, PredIterInfo info);
 static void list_startup_fn(Node *clause, PredIterInfo info);
 static Node *list_next_fn(PredIterInfo info);
@@ -93,12 +93,12 @@ static void arrayexpr_startup_fn(Node *clause, PredIterInfo info);
 static Node *arrayexpr_next_fn(PredIterInfo info);
 static void arrayexpr_cleanup_fn(PredIterInfo info);
 static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
-								   bool clause_is_check);
+								   bool weak);
 static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
-								   bool clause_is_check);
+								   bool weak);
 static Node *extract_not_arg(Node *clause);
 static Node *extract_strong_not_arg(Node *clause);
-static bool list_member_strip(List *list, Expr *datum);
+static bool clause_is_strict_for(Node *clause, Node *subexpr);
 static bool operator_predicate_proof(Expr *predicate, Node *clause,
 						 bool refute_it);
 static bool operator_same_subexprs_proof(Oid pred_op, Oid clause_op,
@@ -112,10 +112,23 @@ static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, uint32 hashv
 /*
  * predicate_implied_by
  *	  Recursively checks whether the clauses in clause_list imply that the
- *	  given predicate is true.  If clause_is_check is true, assume that the
+ *	  given predicate is true.
- *	  clauses in clause_list are CHECK constraints (where null is
+ *
- *	  effectively true) rather than WHERE clauses (where null is effectively
+ * We support two definitions of implication:
- *	  false).
+ *
+ * "Strong" implication: A implies B means that truth of A implies truth of B.
+ * We use this to prove that a row satisfying one WHERE clause or index
+ * predicate must satisfy another one.
+ *
+ * "Weak" implication: A implies B means that non-falsity of A implies
+ * non-falsity of B ("non-false" means "either true or NULL").  We use this to
+ * prove that a row satisfying one CHECK constraint must satisfy another one.
+ *
+ * Strong implication can also be used to prove that a WHERE clause implies a
+ * CHECK constraint, although it will fail to prove a few cases where we could
+ * safely conclude that the implication holds.  There's no support for proving
+ * the converse case, since only a few kinds of CHECK constraint would allow
+ * deducing anything.
  *
  * The top-level List structure of each list corresponds to an AND list.
  * We assume that eval_const_expressions() has been applied and so there
@@ -125,18 +138,19 @@ static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, uint32 hashv
  * valid, but no worse consequences will ensue.
  *
  * We assume the predicate has already been checked to contain only
- * immutable functions and operators.  (In most current uses this is true
+ * immutable functions and operators.  (In many current uses this is known
- * because the predicate is part of an index predicate that has passed
+ * true because the predicate is part of an index predicate that has passed
- * CheckPredicate().)  We dare not make deductions based on non-immutable
+ * CheckPredicate(); otherwise, the caller must check it.)  We dare not make
- * functions, because they might change answers between the time we make
+ * deductions based on non-immutable functions, because they might change
- * the plan and the time we execute the plan.
+ * answers between the time we make the plan and the time we execute the plan.
+ * Immutability of functions in the clause_list is checked here, if necessary.
  */
 bool
 predicate_implied_by(List *predicate_list, List *clause_list,
-					 bool clause_is_check)
+					 bool weak)
 {
 	Node	   *p,
-			   *r;
+			   *c;
 
 	if (predicate_list == NIL)
 		return true;			/* no predicate: implication is vacuous */
@@ -154,32 +168,39 @@ predicate_implied_by(List *predicate_list, List *clause_list,
 	else
 		p = (Node *) predicate_list;
 	if (list_length(clause_list) == 1)
-		r = (Node *) linitial(clause_list);
+		c = (Node *) linitial(clause_list);
 	else
-		r = (Node *) clause_list;
+		c = (Node *) clause_list;
 
 	/* And away we go ... */
-	return predicate_implied_by_recurse(r, p, clause_is_check);
+	return predicate_implied_by_recurse(c, p, weak);
 }
 
 /*
  * predicate_refuted_by
  *	  Recursively checks whether the clauses in clause_list refute the given
- *	  predicate (that is, prove it false).  If clause_is_check is true, assume
+ *	  predicate (that is, prove it false).
- *	  that the clauses in clause_list are CHECK constraints (where null is
- *	  effectively true) rather than WHERE clauses (where null is effectively
- *	  false).
  *
  * This is NOT the same as !(predicate_implied_by), though it is similar
  * in the technique and structure of the code.
  *
- * An important fine point is that truth of the clauses must imply that
+ * We support two definitions of refutation:
- * the predicate returns FALSE, not that it does not return TRUE.  This
+ *
- * is normally used to try to refute CHECK constraints, and the only
+ * "Strong" refutation: A refutes B means truth of A implies falsity of B.
- * thing we can assume about a CHECK constraint is that it didn't return
+ * We use this to disprove a CHECK constraint given a WHERE clause, i.e.,
- * FALSE --- a NULL result isn't a violation per the SQL spec.  (Someday
+ * prove that any row satisfying the WHERE clause would violate the CHECK
- * perhaps this code should be extended to support both "strong" and
+ * constraint.  (Observe we must prove B yields false, not just not-true.)
- * "weak" refutation, but for now we only need "strong".)
+ *
+ * "Weak" refutation: A refutes B means truth of A implies non-truth of B
+ * (i.e., B must yield false or NULL).  We use this to detect mutually
+ * contradictory WHERE clauses.
+ *
+ * Weak refutation can be proven in some cases where strong refutation doesn't
+ * hold, so it's useful to use it when possible.  We don't currently have
+ * support for disproving one CHECK constraint based on another one, nor for
+ * disproving WHERE based on CHECK.  (As with implication, the last case
+ * doesn't seem very practical.  CHECK-vs-CHECK might be useful, but isn't
+ * currently needed anywhere.)
  *
  * The top-level List structure of each list corresponds to an AND list.
  * We assume that eval_const_expressions() has been applied and so there
@@ -192,13 +213,14 @@ predicate_implied_by(List *predicate_list, List *clause_list,
  * immutable functions and operators.  We dare not make deductions based on
  * non-immutable functions, because they might change answers between the
  * time we make the plan and the time we execute the plan.
+ * Immutability of functions in the clause_list is checked here, if necessary.
  */
 bool
 predicate_refuted_by(List *predicate_list, List *clause_list,
-					 bool clause_is_check)
+					 bool weak)
 {
 	Node	   *p,
-			   *r;
+			   *c;
 
 	if (predicate_list == NIL)
 		return false;			/* no predicate: no refutation is possible */
@@ -216,12 +238,12 @@ predicate_refuted_by(List *predicate_list, List *clause_list,
 	else
 		p = (Node *) predicate_list;
 	if (list_length(clause_list) == 1)
-		r = (Node *) linitial(clause_list);
+		c = (Node *) linitial(clause_list);
 	else
-		r = (Node *) clause_list;
+		c = (Node *) clause_list;
 
 	/* And away we go ... */
-	return predicate_refuted_by_recurse(r, p, clause_is_check);
+	return predicate_refuted_by_recurse(c, p, weak);
 }
 
 /*----------
@@ -243,7 +265,9 @@ predicate_refuted_by(List *predicate_list, List *clause_list,
  *
  * An "atom" is anything other than an AND or OR node.  Notice that we don't
  * have any special logic to handle NOT nodes; these should have been pushed
- * down or eliminated where feasible by prepqual.c.
+ * down or eliminated where feasible during eval_const_expressions().
+ *
+ * All of these rules apply equally to strong or weak implication.
  *
  * We can't recursively expand either side first, but have to interleave
  * the expansions per the above rules, to be sure we handle all of these
@@ -261,7 +285,7 @@ predicate_refuted_by(List *predicate_list, List *clause_list,
  */
 static bool
 predicate_implied_by_recurse(Node *clause, Node *predicate,
-							 bool clause_is_check)
+							 bool weak)
 {
 	PredIterInfoData clause_info;
 	PredIterInfoData pred_info;
@@ -289,7 +313,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_implied_by_recurse(clause, pitem,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -309,7 +333,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (predicate_implied_by_recurse(clause, pitem,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -327,7 +351,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (predicate_implied_by_recurse(citem, predicate,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -345,7 +369,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (predicate_implied_by_recurse(citem, predicate,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -373,7 +397,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 						iterate_begin(pitem, predicate, pred_info)
 						{
 							if (predicate_implied_by_recurse(citem, pitem,
-															 clause_is_check))
+															 weak))
 							{
 								presult = true;
 								break;
@@ -401,7 +425,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (!predicate_implied_by_recurse(citem, predicate,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -424,7 +448,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_implied_by_recurse(clause, pitem,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -442,7 +466,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (predicate_implied_by_recurse(clause, pitem,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -459,7 +483,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
 					return
 						predicate_implied_by_simple_clause((Expr *) predicate,
 														   clause,
-														   clause_is_check);
+														   weak);
 			}
 			break;
 	}
@@ -486,22 +510,23 @@ predicate_implied_by_recurse(Node *clause, Node *predicate,
  *	OR-expr A R=> AND-expr B iff:	each of A's components R=> any of B's
  *	OR-expr A R=> OR-expr B iff:	A R=> each of B's components
  *
+ * All of the above rules apply equally to strong or weak refutation.
+ *
  * In addition, if the predicate is a NOT-clause then we can use
  *	A R=> NOT B if:					A => B
  * This works for several different SQL constructs that assert the non-truth
- * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN.
+ * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN, although some
- * Unfortunately we *cannot* use
+ * of them require that we prove strong implication.  Likewise, we can use
  *	NOT A R=> B if:					B => A
- * because this type of reasoning fails to prove that B doesn't yield NULL.
+ * but here we must be careful about strong vs. weak refutation and make
- * We can however make the more limited deduction that
+ * the appropriate type of implication proof (weak or strong respectively).
- *	NOT A R=> A
  *
  * Other comments are as for predicate_implied_by_recurse().
  *----------
  */
 static bool
 predicate_refuted_by_recurse(Node *clause, Node *predicate,
-							 bool clause_is_check)
+							 bool weak)
 {
 	PredIterInfoData clause_info;
 	PredIterInfoData pred_info;
@@ -532,7 +557,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (predicate_refuted_by_recurse(clause, pitem,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -550,7 +575,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (predicate_refuted_by_recurse(citem, predicate,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -568,7 +593,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_refuted_by_recurse(clause, pitem,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -580,12 +605,19 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 				case CLASS_ATOM:
 
 					/*
-					 * If B is a NOT-clause, A R=> B if A => B's arg
+					 * If B is a NOT-type clause, A R=> B if A => B's arg
+					 *
+					 * Since, for either type of refutation, we are starting
+					 * with the premise that A is true, we can use a strong
+					 * implication test in all cases.  That proves B's arg is
+					 * true, which is more than we need for weak refutation if
+					 * B is a simple NOT, but it allows not worrying about
+					 * exactly which kind of negation clause we have.
 					 */
 					not_arg = extract_not_arg(predicate);
 					if (not_arg &&
 						predicate_implied_by_recurse(clause, not_arg,
-													 clause_is_check))
+													 false))
 						return true;
 
 					/*
@@ -595,7 +627,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (predicate_refuted_by_recurse(citem, predicate,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -618,7 +650,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_refuted_by_recurse(clause, pitem,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -641,7 +673,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 						iterate_begin(pitem, predicate, pred_info)
 						{
 							if (predicate_refuted_by_recurse(citem, pitem,
-															 clause_is_check))
+															 weak))
 							{
 								presult = true;
 								break;
@@ -660,12 +692,14 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 				case CLASS_ATOM:
 
 					/*
-					 * If B is a NOT-clause, A R=> B if A => B's arg
+					 * If B is a NOT-type clause, A R=> B if A => B's arg
+					 *
+					 * Same logic as for the AND-clause case above.
 					 */
 					not_arg = extract_not_arg(predicate);
 					if (not_arg &&
 						predicate_implied_by_recurse(clause, not_arg,
-													 clause_is_check))
+													 false))
 						return true;
 
 					/*
@@ -675,7 +709,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(citem, clause, clause_info)
 					{
 						if (!predicate_refuted_by_recurse(citem, predicate,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -689,16 +723,18 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 		case CLASS_ATOM:
 
 			/*
-			 * If A is a strong NOT-clause, A R=> B if B equals A's arg
+			 * If A is a strong NOT-clause, A R=> B if B => A's arg
 			 *
-			 * We cannot make the stronger conclusion that B is refuted if B
+			 * Since A is strong, we may assume A's arg is false (not just
-			 * implies A's arg; that would only prove that B is not-TRUE, not
+			 * not-true).  If B weakly implies A's arg, then B can be neither
-			 * that it's not NULL either.  Hence use equal() rather than
+			 * true nor null, so that strong refutation is proven.  If B
-			 * predicate_implied_by_recurse().  We could do the latter if we
+			 * strongly implies A's arg, then B cannot be true, so that weak
-			 * ever had a need for the weak form of refutation.
+			 * refutation is proven.
 			 */
 			not_arg = extract_strong_not_arg(clause);
-			if (not_arg && equal(predicate, not_arg))
+			if (not_arg &&
+				predicate_implied_by_recurse(predicate, not_arg,
+											 !weak))
 				return true;
 
 			switch (pclass)
@@ -712,7 +748,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (predicate_refuted_by_recurse(clause, pitem,
-														 clause_is_check))
+														 weak))
 						{
 							result = true;
 							break;
@@ -730,7 +766,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					iterate_begin(pitem, predicate, pred_info)
 					{
 						if (!predicate_refuted_by_recurse(clause, pitem,
-														  clause_is_check))
+														  weak))
 						{
 							result = false;
 							break;
@@ -742,12 +778,14 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 				case CLASS_ATOM:
 
 					/*
-					 * If B is a NOT-clause, A R=> B if A => B's arg
+					 * If B is a NOT-type clause, A R=> B if A => B's arg
+					 *
+					 * Same logic as for the AND-clause case above.
 					 */
 					not_arg = extract_not_arg(predicate);
 					if (not_arg &&
 						predicate_implied_by_recurse(clause, not_arg,
-													 clause_is_check))
+													 false))
 						return true;
 
 					/*
@@ -756,7 +794,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 					return
 						predicate_refuted_by_simple_clause((Expr *) predicate,
 														   clause,
-														   clause_is_check);
+														   weak);
 			}
 			break;
 	}
@@ -1054,19 +1092,16 @@ arrayexpr_cleanup_fn(PredIterInfo info)
  * implies another:
  *
  * A simple and general way is to see if they are equal(); this works for any
- * kind of expression.  (Actually, there is an implied assumption that the
+ * kind of expression, and for either implication definition.  (Actually,
- * functions in the expression are immutable, ie dependent only on their input
+ * there is an implied assumption that the functions in the expression are
- * arguments --- but this was checked for the predicate by the caller.)
+ * immutable --- but this was checked for the predicate by the caller.)
  *
- * When clause_is_check is false, we know we are within an AND/OR
+ * If the predicate is of the form "foo IS NOT NULL", and we are considering
- * subtree of a WHERE clause.  So, if the predicate is of the form "foo IS
+ * strong implication, we can conclude that the predicate is implied if the
- * NOT NULL", we can conclude that the predicate is implied if the clause is
+ * clause is strict for "foo", i.e., it must yield NULL when "foo" is NULL.
- * a strict operator or function that has "foo" as an input.  In this case
+ * In that case truth of the clause requires that "foo" isn't NULL.
- * the clause must yield NULL when "foo" is NULL, which we can take as
+ * (Again, this is a safe conclusion because "foo" must be immutable.)
- * equivalent to FALSE given the context. (Again, "foo" is already known
+ * This doesn't work for weak implication, though.
- * immutable, so the clause will certainly always fail.) Also, if the clause
- * is just "foo" (meaning it's a boolean variable), the predicate is implied
- * since the clause can't be true if "foo" is NULL.
  *
  * Finally, if both clauses are binary operator expressions, we may be able
  * to prove something using the system's knowledge about operators; those
@@ -1075,7 +1110,7 @@ arrayexpr_cleanup_fn(PredIterInfo info)
  */
 static bool
 predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
-								   bool clause_is_check)
+								   bool weak)
 {
 	/* Allow interrupting long proof attempts */
 	CHECK_FOR_INTERRUPTS();
@@ -1085,23 +1120,17 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 		return true;
 
 	/* Next try the IS NOT NULL case */
-	if (predicate && IsA(predicate, NullTest) &&
+	if (!weak &&
-		((NullTest *) predicate)->nulltesttype == IS_NOT_NULL)
+		predicate && IsA(predicate, NullTest))
 	{
-		Expr	   *nonnullarg = ((NullTest *) predicate)->arg;
+		NullTest   *ntest = (NullTest *) predicate;
 
 		/* row IS NOT NULL does not act in the simple way we have in mind */
-		if (!((NullTest *) predicate)->argisrow && !clause_is_check)
+		if (ntest->nulltesttype == IS_NOT_NULL &&
+			!ntest->argisrow)
 		{
-			if (is_opclause(clause) &&
+			/* strictness of clause for foo implies foo IS NOT NULL */
-				list_member_strip(((OpExpr *) clause)->args, nonnullarg) &&
+			if (clause_is_strict_for(clause, (Node *) ntest->arg))
-				op_strict(((OpExpr *) clause)->opno))
-				return true;
-			if (is_funcclause(clause) &&
-				list_member_strip(((FuncExpr *) clause)->args, nonnullarg) &&
-				func_strict(((FuncExpr *) clause)->funcid))
-				return true;
-			if (equal(clause, nonnullarg))
 				return true;
 		}
 		return false;			/* we can't succeed below... */
@@ -1118,17 +1147,23 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
  *
  * We return true if able to prove the refutation, false if not.
  *
- * Unlike the implication case, checking for equal() clauses isn't
+ * Unlike the implication case, checking for equal() clauses isn't helpful.
- * helpful.
+ * But relation_excluded_by_constraints() checks for self-contradictions in a
+ * list of clauses, so that we may get here with predicate and clause being
+ * actually pointer-equal, and that is worth eliminating quickly.
  *
  * When the predicate is of the form "foo IS NULL", we can conclude that
- * the predicate is refuted if the clause is a strict operator or function
+ * the predicate is refuted if the clause is strict for "foo" (see notes for
- * that has "foo" as an input (see notes for implication case), or if the
+ * implication case), or is "foo IS NOT NULL".  That works for either strong
- * clause is "foo IS NOT NULL".  A clause "foo IS NULL" refutes a predicate
+ * or weak refutation.
- * "foo IS NOT NULL", but unfortunately does not refute strict predicates,
+ *
- * because we are looking for strong refutation.  (The motivation for covering
+ * A clause "foo IS NULL" refutes a predicate "foo IS NOT NULL" in all cases.
- * these cases is to support using IS NULL/IS NOT NULL as partition-defining
+ * If we are considering weak refutation, it also refutes a predicate that
- * constraints.)
+ * is strict for "foo", since then the predicate must yield 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.)
  *
  * Finally, if both clauses are binary operator expressions, we may be able
  * to prove something using the system's knowledge about operators; those
@@ -1137,7 +1172,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
  */
 static bool
 predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
-								   bool clause_is_check)
+								   bool weak)
 {
 	/* Allow interrupting long proof attempts */
 	CHECK_FOR_INTERRUPTS();
@@ -1153,21 +1188,12 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 	{
 		Expr	   *isnullarg = ((NullTest *) predicate)->arg;
 
-		if (clause_is_check)
-			return false;
-
 		/* row IS NULL does not act in the simple way we have in mind */
 		if (((NullTest *) predicate)->argisrow)
 			return false;
 
-		/* Any strict op/func on foo refutes foo IS NULL */
+		/* strictness of clause for foo refutes foo IS NULL */
-		if (is_opclause(clause) &&
+		if (clause_is_strict_for(clause, (Node *) isnullarg))
-			list_member_strip(((OpExpr *) clause)->args, isnullarg) &&
-			op_strict(((OpExpr *) clause)->opno))
-			return true;
-		if (is_funcclause(clause) &&
-			list_member_strip(((FuncExpr *) clause)->args, isnullarg) &&
-			func_strict(((FuncExpr *) clause)->funcid))
 			return true;
 
 		/* foo IS NOT NULL refutes foo IS NULL */
@@ -1197,6 +1223,11 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 			equal(((NullTest *) predicate)->arg, isnullarg))
 			return true;
 
+		/* foo IS NULL weakly refutes any predicate that is strict for foo */
+		if (weak &&
+			clause_is_strict_for((Node *) predicate, (Node *) isnullarg))
+			return true;
+
 		return false;			/* we can't succeed below... */
 	}
 
@@ -1261,29 +1292,63 @@ extract_strong_not_arg(Node *clause)
 
 
 /*
- * Check whether an Expr is equal() to any member of a list, ignoring
+ * Can we prove that "clause" returns NULL if "subexpr" does?
- * any top-level RelabelType nodes.  This is legitimate for the purposes
+ *
- * we use it for (matching IS [NOT] NULL arguments to arguments of strict
+ * The base case is that clause and subexpr are equal().  (We assume that
- * functions) because RelabelType doesn't change null-ness.  It's helpful
+ * the caller knows at least one of the input expressions is immutable,
- * for cases such as a varchar argument of a strict function on text.
+ * as this wouldn't hold for volatile expressions.)
+ *
+ * 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
-list_member_strip(List *list, Expr *datum)
+clause_is_strict_for(Node *clause, Node *subexpr)
 {
-	ListCell   *cell;
+	ListCell   *lc;
 
-	if (datum && IsA(datum, RelabelType))
+	/* safety checks */
-		datum = ((RelabelType *) datum)->arg;
+	if (clause == NULL || subexpr == NULL)
+		return false;
 
-	foreach(cell, list)
+	/*
-	{
+	 * Look through any RelabelType nodes, so that we can match, say,
-		Expr	   *elem = (Expr *) lfirst(cell);
+	 * varcharcol with lower(varcharcol::text).  (In general we could recurse
+	 * through any nullness-preserving, immutable operation.)  We should not
+	 * see stacked RelabelTypes here.
+	 */
+	if (IsA(clause, RelabelType))
+		clause = (Node *) ((RelabelType *) clause)->arg;
+	if (IsA(subexpr, RelabelType))
+		subexpr = (Node *) ((RelabelType *) subexpr)->arg;
 
-		if (elem && IsA(elem, RelabelType))
+	/* Base case */
-			elem = ((RelabelType *) elem)->arg;
+	if (equal(clause, subexpr))
-
-		if (equal(elem, datum))
 		return true;
+
+	/*
+	 * If we have a strict operator or function, a NULL result is guaranteed
+	 * if any input is forced NULL by subexpr.  This is OK even if the op or
+	 * func isn't immutable, since it won't even be called on NULL input.
+	 */
+	if (is_opclause(clause) &&
+		op_strict(((OpExpr *) clause)->opno))
+	{
+		foreach(lc, ((OpExpr *) clause)->args)
+		{
+			if (clause_is_strict_for((Node *) lfirst(lc), subexpr))
+				return true;
+		}
+		return false;
+	}
+	if (is_funcclause(clause) &&
+		func_strict(((FuncExpr *) clause)->funcid))
+	{
+		foreach(lc, ((FuncExpr *) clause)->args)
+		{
+			if (clause_is_strict_for((Node *) lfirst(lc), subexpr))
+				return true;
+		}
+		return false;
 	}
 
 	return false;
@@ -1420,6 +1485,23 @@ static const StrategyNumber BT_refute_table[6][6] = {
  * in one routine.)  We return true if able to make the proof, false
  * if not able to prove it.
  *
+ * We mostly need not distinguish strong vs. weak implication/refutation here.
+ * This depends on the assumption that a pair of related operators (i.e.,
+ * commutators, negators, or btree opfamily siblings) will not return one NULL
+ * and one non-NULL result for the same inputs.  Then, for the proof types
+ * where we start with an assumption of truth of the clause, the predicate
+ * operator could not return NULL either, so it doesn't matter whether we are
+ * trying to make a strong or weak proof.  For weak implication, it could be
+ * that the clause operator returned NULL, but then the predicate operator
+ * would as well, so that the weak implication still holds.  This argument
+ * doesn't apply in the case where we are considering two different constant
+ * values, since then the operators aren't being given identical inputs.  But
+ * we only support that for btree operators, for which we can assume that all
+ * non-null inputs result in non-null outputs, so that it doesn't matter which
+ * two non-null constants we consider.  Currently the code below just reports
+ * "proof failed" if either constant is NULL, but in some cases we could be
+ * smarter (and that likely would require checking strong vs. weak proofs).
+ *
  * We can make proofs involving several expression forms (here "foo" and "bar"
  * represent subexpressions that are identical according to equal()):
  *	"foo op1 bar" refutes "foo op2 bar" if op1 is op2's negator
@@ -1594,6 +1676,11 @@ operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it)
 	 * are not identical but are both Consts; and we have commuted the
 	 * operators if necessary so that the Consts are on the right.  We'll need
 	 * to compare the Consts' values.  If either is NULL, fail.
+	 *
+	 * Future work: in some cases the desired proof might hold even with NULL
+	 * constants.  But beware that we've not yet identified the operators as
+	 * btree ops, so for instance it'd be quite unsafe to assume they are
+	 * strict without checking.
 	 */
 	if (pred_const->constisnull)
 		return false;

src/include/optimizer/predtest.h

@@ -18,8 +18,8 @@
 
 
 extern bool predicate_implied_by(List *predicate_list, List *clause_list,
-					 bool clause_is_check);
+					 bool weak);
 extern bool predicate_refuted_by(List *predicate_list, List *clause_list,
-					 bool clause_is_check);
+					 bool weak);
 
 #endif							/* PREDTEST_H */

src/test/modules/test_predtest/expected/test_predtest.out

@@ -16,6 +16,9 @@ select
   case i%11 when 10 then null else i%11 end as x,
   case (i/11)%11 when 10 then null else (i/11)%11 end as y
 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;
 -- Basic proof rules for single boolean variables
 select * from test_predtest($$
 select x, x
@@ -109,7 +112,7 @@ $$);
 strong_implied_by | f
 weak_implied_by   | f
 strong_refuted_by | t
-weak_refuted_by   | f
+weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
@@ -199,7 +202,7 @@ w_i_holds         | t
 s_r_holds         | f
 w_r_holds         | t
 
--- XXX seems like we should be able to refute x is null here
+-- Assorted not-so-trivial refutation rules
 select * from test_predtest($$
 select x is null, x
 from booleans
@@ -207,8 +210,8 @@ $$);
 -[ RECORD 1 ]-----+--
 strong_implied_by | f
 weak_implied_by   | f
-strong_refuted_by | f
+strong_refuted_by | t
-weak_refuted_by   | f
+weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
@@ -222,12 +225,68 @@ $$);
 strong_implied_by | f
 weak_implied_by   | f
 strong_refuted_by | f
-weak_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 strictf(x,y), x is null
+from booleans
+$$);
+-[ 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 is not null) is not true, x
+from booleans
+$$);
+-[ 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 strictf(x,y), (x is not null) is false
+from booleans
+$$);
+-[ 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 > y, (y < x) is false
+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
+
 -- Tests involving AND/OR constructs
 select * from test_predtest($$
 select x, x and y
@@ -369,6 +428,20 @@ w_i_holds         | t
 s_r_holds         | f
 w_r_holds         | f
 
+select * from test_predtest($$
+select x and z, x and y and z
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+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 z or w, x or y
 from booleans
@@ -644,7 +717,7 @@ $$);
 strong_implied_by | f
 weak_implied_by   | f
 strong_refuted_by | t
-weak_refuted_by   | f
+weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
@@ -658,7 +731,7 @@ $$);
 strong_implied_by | f
 weak_implied_by   | f
 strong_refuted_by | t
-weak_refuted_by   | f
+weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
@@ -708,7 +781,7 @@ w_i_holds         | f
 s_r_holds         | f
 w_r_holds         | f
 
--- XXX ideally, we could prove this case too
+-- XXX ideally, we could prove this case too, for strong implication
 select * from test_predtest($$
 select x <= 5, x in (1,3,5,null)
 from integers

src/test/modules/test_predtest/sql/test_predtest.sql

@@ -21,6 +21,10 @@ select
   case (i/11)%11 when 10 then null else (i/11)%11 end as y
 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;
+
 -- Basic proof rules for single boolean variables
 
 select * from test_predtest($$
@@ -88,7 +92,8 @@ select x, x is unknown
 from booleans
 $$);
 
--- XXX seems like we should be able to refute x is null here
+-- Assorted not-so-trivial refutation rules
+
 select * from test_predtest($$
 select x is null, x
 from booleans
@@ -99,6 +104,26 @@ select x, x is null
 from booleans
 $$);
 
+select * from test_predtest($$
+select strictf(x,y), x is null
+from booleans
+$$);
+
+select * from test_predtest($$
+select (x is not null) is not true, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select strictf(x,y), (x is not null) is false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x > y, (y < x) is false
+from integers
+$$);
+
 -- Tests involving AND/OR constructs
 
 select * from test_predtest($$
@@ -151,6 +176,11 @@ select x or y or z, x or z
 from booleans
 $$);
 
+select * from test_predtest($$
+select x and z, x and y and z
+from booleans
+$$);
+
 select * from test_predtest($$
 select z or w, x or y
 from booleans
@@ -276,7 +306,7 @@ select x <= 5, x in (1,3,5,7)
 from integers
 $$);
 
--- XXX ideally, we could prove this case too
+-- XXX ideally, we could prove this case too, for strong implication
 select * from test_predtest($$
 select x <= 5, x in (1,3,5,null)
 from integers

src/test/regress/expected/partition_prune.out

@@ -235,7 +235,7 @@ explain (costs off) select * from rlp where a = 1::bigint;		/* same as above */
          Filter: (a = '1'::bigint)
 (3 rows)
 
-explain (costs off) select * from rlp where a = 1::numeric;	/* no pruning */
+explain (costs off) select * from rlp where a = 1::numeric;	/* only null can be pruned */
                   QUERY PLAN                   
 -----------------------------------------------
  Append
@@ -265,11 +265,9 @@ explain (costs off) select * from rlp where a = 1::numeric;	/* no pruning */
          Filter: ((a)::numeric = '1'::numeric)
    ->  Seq Scan on rlp_default_30
          Filter: ((a)::numeric = '1'::numeric)
-   ->  Seq Scan on rlp_default_null
-         Filter: ((a)::numeric = '1'::numeric)
    ->  Seq Scan on rlp_default_default
          Filter: ((a)::numeric = '1'::numeric)
-(31 rows)
+(29 rows)
 
 explain (costs off) select * from rlp where a <= 10;
               QUERY PLAN               

src/test/regress/sql/partition_prune.sql

@@ -60,7 +60,7 @@ explain (costs off) select * from rlp where 1 > a;	/* commuted */
 explain (costs off) select * from rlp where a <= 1;
 explain (costs off) select * from rlp where a = 1;
 explain (costs off) select * from rlp where a = 1::bigint;		/* same as above */
-explain (costs off) select * from rlp where a = 1::numeric;	/* no pruning */
+explain (costs off) select * from rlp where a = 1::numeric;	/* only null can be pruned */
 explain (costs off) select * from rlp where a <= 10;
 explain (costs off) select * from rlp where a > 10;
 explain (costs off) select * from rlp where a < 15;