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.

diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c
index dd19e4390b2c49399198715804d65fb72ed1537c..97d7e94f3266b513407225c5541a5bc34beab6db 100644 (file)
--- 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.31 2010/02/14 18:42:15 rhaas Exp $
+ *   $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.32 2010/02/25 20:59:53 tgl Exp $
  *
  *-------------------------------------------------------------------------
  */
@@ -95,6 +95,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);
@@ -468,6 +469,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().
  *----------
@@ -651,21 +654,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)
            {
@@ -1178,6 +1178,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