Allow predicate_refuted_by() to deduce that NOT A refutes A.

We had originally made the stronger assumption that NOT A refutes any B
if B implies A, but this fails in three-valued logic, because we need to
prove B is false not just that it's not true.  However the logic does
go through if B is equal to A.

Recognizing this limited case is enough to handle examples that arise when
we have simplified "bool_var = true" or "bool_var = false" to just "bool_var"
or "NOT bool_var".  If we had not done that simplification then the
btree-operator proof logic would have been able to prove that the expressions
were contradictory, but only for identical expressions being compared to the
constants; so handling identical A and B covers all the same cases.

The motivation for doing this is to avoid unexpected asymmetrical behavior
when a partitioned table uses a boolean partitioning column, as in today's
gripe from Dominik Sander.

Back-patch to 8.2, which is as far back as predicate_refuted_by attempts to
do anything at all with NOTs.

1 files changed, 38 insertions, 11 deletions

diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c
index 56e709093b2..6c61445a8a4 100644
--- a/src/backend/optimizer/util/predtest.c
+++ b/src/backend/optimizer/util/predtest.c
@@ -9,7 +9,7 @@
  *
  *
  * IDENTIFICATION
- *	  $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.10.2.5 2009/05/11 17:56:22 tgl Exp $
+ *	  $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.10.2.6 2010/02/25 21:00:15 tgl Exp $
  *
  *-------------------------------------------------------------------------
  */
@@ -93,6 +93,7 @@ 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 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 btree_predicate_proof(Expr *predicate, Node *clause,
 					  bool refute_it);
@@ -430,6 +431,8 @@ predicate_implied_by_recurse(Node *clause, Node *predicate)
  * 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.
+ * We can however make the more limited deduction that
+ *	NOT A R=> A
  *
  * Other comments are as for predicate_implied_by_recurse().
  *----------
@@ -613,20 +616,18 @@ 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
+			 * If A is a strong NOT-clause, A R=> B if B equals 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.
+			 * We cannot make the stronger conclusion that B is refuted if
+			 * B implies A's arg; that would only prove that B is not-TRUE,
+			 * not that it's not NULL either.  Hence use equal() rather than
+			 * predicate_implied_by_recurse().  We could do the latter 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))
+			not_arg = extract_strong_not_arg(clause);
+			if (not_arg && equal(predicate, not_arg))
 				return true;
-#endif
 
 			switch (pclass)
 			{
@@ -1136,6 +1137,32 @@ extract_not_arg(Node *clause)
 	return NULL;
 }
 
+/*
+ * If clause asserts the falsity of a subclause, return that subclause;
+ * otherwise return NULL.
+ */
+static Node *
+extract_strong_not_arg(Node *clause)
+{
+	if (clause == NULL)
+		return NULL;
+	if (IsA(clause, BoolExpr))
+	{
+		BoolExpr   *bexpr = (BoolExpr *) clause;
+
+		if (bexpr->boolop == NOT_EXPR)
+			return (Node *) linitial(bexpr->args);
+	}
+	else if (IsA(clause, BooleanTest))
+	{
+		BooleanTest *btest = (BooleanTest *) clause;
+
+		if (btest->booltesttype == IS_FALSE)
+			return (Node *) btest->arg;
+	}
+	return NULL;
+}
+
 
 /*
  * Check whether an Expr is equal() to any member of a list, ignoring