Fix logical errors in constraint exclusion: we cannot assume that a CHECK

constraint yields TRUE for every row of its table, only that it does not
yield FALSE (a NULL result isn't disallowed).  This breaks a couple of
implications that would be true in two-valued logic.  I had put in one such
mistake in an 8.2.5 patch: foo IS NULL doesn't refute a strict operator
on foo.  But there was another in the original 8.2 release: NOT foo doesn't
refute an expression whose truth would imply the truth of foo.
Per report from Rajesh Kumar Mallah.

To preserve the ability to do constraint exclusion with one partition
holding NULL values, extend relation_excluded_by_constraints() to check
for attnotnull flags, and add col IS NOT NULL expressions to the set of
constraints we hope to refute.

src/backend/optimizer/util/plancat.c

@@ -9,7 +9,7 @@
  *
  *
  * IDENTIFICATION
- *	  $PostgreSQL: pgsql/src/backend/optimizer/util/plancat.c,v 1.139 2008/01/01 19:45:50 momjian Exp $
+ *	  $PostgreSQL: pgsql/src/backend/optimizer/util/plancat.c,v 1.140 2008/01/12 00:11:39 tgl Exp $
  *
  *-------------------------------------------------------------------------
  */
@@ -47,7 +47,8 @@ get_relation_info_hook_type get_relation_info_hook = NULL;
 
 static void estimate_rel_size(Relation rel, int32 *attr_widths,
 				  BlockNumber *pages, double *tuples);
-static List *get_relation_constraints(Oid relationObjectId, RelOptInfo *rel);
+static List *get_relation_constraints(Oid relationObjectId, RelOptInfo *rel,
+						 bool include_notnull);
 
 
 /*
@@ -453,12 +454,16 @@ estimate_rel_size(Relation rel, int32 *attr_widths,
  * indicated by rel->relid.  This allows the expressions to be easily
  * compared to expressions taken from WHERE.
  *
+ * If include_notnull is true, "col IS NOT NULL" expressions are generated
+ * and added to the result for each column that's marked attnotnull.
+ *
  * Note: at present this is invoked at most once per relation per planner
  * run, and in many cases it won't be invoked at all, so there seems no
  * point in caching the data in RelOptInfo.
  */
 static List *
-get_relation_constraints(Oid relationObjectId, RelOptInfo *rel)
+get_relation_constraints(Oid relationObjectId, RelOptInfo *rel,
+						 bool include_notnull)
 {
 	List	   *result = NIL;
 	Index		varno = rel->relid;
@@ -513,6 +518,30 @@ get_relation_constraints(Oid relationObjectId, RelOptInfo *rel)
 			result = list_concat(result,
 								 make_ands_implicit((Expr *) cexpr));
 		}
+
+		/* Add NOT NULL constraints in expression form, if requested */
+		if (include_notnull && constr->has_not_null)
+		{
+			int		natts = relation->rd_att->natts;
+
+			for (i = 1; i <= natts; i++)
+			{
+				Form_pg_attribute att = relation->rd_att->attrs[i - 1];
+
+				if (att->attnotnull && !att->attisdropped)
+				{
+					NullTest *ntest = makeNode(NullTest);
+
+					ntest->arg = (Expr *) makeVar(varno,
+												  i,
+												  att->atttypid,
+												  att->atttypmod,
+												  0);
+					ntest->nulltesttype = IS_NOT_NULL;
+					result = lappend(result, ntest);
+				}
+			}
+		}
 	}
 
 	heap_close(relation, NoLock);
@@ -567,8 +596,11 @@ relation_excluded_by_constraints(RelOptInfo *rel, RangeTblEntry *rte)
 	if (rte->rtekind != RTE_RELATION || rte->inh)
 		return false;
 
-	/* OK to fetch the constraint expressions */
-	constraint_pred = get_relation_constraints(rte->relid, rel);
+	/*
+	 * OK to fetch the constraint expressions.  Include "col IS NOT NULL"
+	 * expressions for attnotnull columns, in case we can refute those.
+	 */
+	constraint_pred = get_relation_constraints(rte->relid, rel, true);
 
 	/*
 	 * We do not currently enforce that CHECK constraints contain only

src/backend/optimizer/util/predtest.c

@@ -9,7 +9,7 @@
  *
  *
  * IDENTIFICATION
- *	  $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.18 2008/01/01 19:45:50 momjian Exp $
+ *	  $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.19 2008/01/12 00:11:39 tgl Exp $
  *
  *-------------------------------------------------------------------------
  */
@@ -82,7 +82,6 @@ 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);
 static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause);
-static bool is_null_contradicts(NullTest *ntest, Node *clause);
 static Node *extract_not_arg(Node *clause);
 static bool list_member_strip(List *list, Expr *datum);
 static bool btree_predicate_proof(Expr *predicate, Node *clause,
@@ -129,6 +128,14 @@ predicate_implied_by(List *predicate_list, List *restrictinfo_list)
  * 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
+ * the predicate returns FALSE, not that it does not return TRUE.  This
+ * is normally used to try to refute CHECK constraints, and the only
+ * thing we can assume about a CHECK constraint is that it didn't return
+ * FALSE --- a NULL result isn't a violation per the SQL spec.  (Someday
+ * perhaps this code should be extended to support both "strong" and
+ * "weak" refutation, but for now we only need "strong".)
+ *
  * 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
  * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
@@ -408,10 +415,11 @@ predicate_implied_by_recurse(Node *clause, Node *predicate)
  *
  * In addition, if the predicate is a NOT-clause then we can use
  *	A R=> NOT B if:					A => B
- * while if the restriction clause is a NOT-clause then we can use
- *	NOT A R=> B if:					B => A
  * This works for several different SQL constructs that assert the non-truth
  * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN.
+ * Unfortunately we *cannot* use
+ *	NOT A R=> B if:					B => A
+ * because this type of reasoning fails to prove that B doesn't yield NULL.
  *
  * Other comments are as for predicate_implied_by_recurse().
  *----------
@@ -595,13 +603,21 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate)
 
 		case CLASS_ATOM:
 
+#ifdef NOT_USED
 			/*
 			 * If A is a NOT-clause, A R=> B if B => A's arg
+			 *
+			 * Unfortunately not: this would only prove that B is not-TRUE,
+			 * not that it's not NULL either.  Keep this code as a comment
+			 * because it would be useful if we ever had a need for the
+			 * weak form of refutation.
 			 */
 			not_arg = extract_not_arg(clause);
 			if (not_arg &&
 				predicate_implied_by_recurse(predicate, not_arg))
 				return true;
+#endif
+
 			switch (pclass)
 			{
 				case CLASS_AND:
@@ -990,9 +1006,11 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause)
  * 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
  * that has "foo" as an input (see notes for implication case), or if the
- * clause is "foo IS NOT NULL".  Conversely a clause "foo IS NULL" refutes
- * predicates of those types.  (The motivation for covering these cases is
- * to support using IS NULL/IS NOT NULL as partition-defining constraints.)
+ * clause is "foo IS NOT NULL".  A clause "foo IS NULL" refutes a predicate
+ * "foo IS NOT NULL", but unfortunately does not refute strict predicates,
+ * because we are looking for strong refutation.  (The motivation for covering
+ * these cases is to support using IS NULL/IS NOT NULL as partition-defining
+ * constraints.)
  *
  * Finally, we may be able to deduce something using knowledge about btree
  * operator families; this is encapsulated in btree_predicate_proof().
@@ -1010,40 +1028,13 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause)
 	if (predicate && IsA(predicate, NullTest) &&
 		((NullTest *) predicate)->nulltesttype == IS_NULL)
 	{
-		if (is_null_contradicts((NullTest *) predicate, clause))
-			return true;
-		return false;			/* we can't succeed below... */
-	}
-
-	/* Try the clause-IS-NULL case */
-	if (clause && IsA(clause, NullTest) &&
-		((NullTest *) clause)->nulltesttype == IS_NULL)
-	{
-		if (is_null_contradicts((NullTest *) clause, (Node *) predicate))
-			return true;
-		return false;			/* we can't succeed below... */
-	}
-
-	/* Else try btree operator knowledge */
-	return btree_predicate_proof(predicate, clause, true);
-}
-
-
-/*
- * Check whether a "foo IS NULL" test contradicts clause.  (We say
- * "contradicts" rather than "refutes" because the refutation goes
- * both ways.)
- */
-static bool
-is_null_contradicts(NullTest *ntest, Node *clause)
-{
-	Expr	   *isnullarg = ntest->arg;
+		Expr	   *isnullarg = ((NullTest *) predicate)->arg;
 
 		/* row IS NULL does not act in the simple way we have in mind */
 		if (type_is_rowtype(exprType((Node *) isnullarg)))
 			return false;
 
-	/* foo IS NULL contradicts any strict op/func on foo */
+		/* Any strict op/func on foo refutes foo IS NULL */
 		if (is_opclause(clause) &&
 			list_member_strip(((OpExpr *) clause)->args, isnullarg) &&
 			op_strict(((OpExpr *) clause)->opno))
@@ -1053,13 +1044,36 @@ is_null_contradicts(NullTest *ntest, Node *clause)
 			func_strict(((FuncExpr *) clause)->funcid))
 			return true;
 
-	/* foo IS NULL contradicts foo IS NOT NULL */
+		/* foo IS NOT NULL refutes foo IS NULL */
 		if (clause && IsA(clause, NullTest) &&
 			((NullTest *) clause)->nulltesttype == IS_NOT_NULL &&
 			equal(((NullTest *) clause)->arg, isnullarg))
 			return true;
 
+		return false;			/* we can't succeed below... */
+	}
+
+	/* Try the clause-IS-NULL case */
+	if (clause && IsA(clause, NullTest) &&
+		((NullTest *) clause)->nulltesttype == IS_NULL)
+	{
+		Expr	   *isnullarg = ((NullTest *) clause)->arg;
+
+		/* row IS NULL does not act in the simple way we have in mind */
+		if (type_is_rowtype(exprType((Node *) isnullarg)))
 			return false;
+
+		/* foo IS NULL refutes foo IS NOT NULL */
+		if (predicate && IsA(predicate, NullTest) &&
+			((NullTest *) predicate)->nulltesttype == IS_NOT_NULL &&
+			equal(((NullTest *) predicate)->arg, isnullarg))
+			return true;
+
+		return false;			/* we can't succeed below... */
+	}
+
+	/* Else try btree operator knowledge */
+	return btree_predicate_proof(predicate, clause, true);
 }