Location via proxy:   [ UP ]  
[Report a bug]   [Manage cookies]                
Skip to content

Commit 99419d3

Browse files
committed
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 parent 1951c97 commit 99419d3

File tree

1 file changed

+38
-12
lines changed

1 file changed

+38
-12
lines changed

src/backend/optimizer/util/predtest.c

Lines changed: 38 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
*
1010
*
1111
* IDENTIFICATION
12-
* $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.31 2010/02/14 18:42:15 rhaas Exp $
12+
* $PostgreSQL: pgsql/src/backend/optimizer/util/predtest.c,v 1.32 2010/02/25 20:59:53 tgl Exp $
1313
*
1414
*-------------------------------------------------------------------------
1515
*/
@@ -95,6 +95,7 @@ static void arrayexpr_cleanup_fn(PredIterInfo info);
9595
static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause);
9696
static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause);
9797
static Node *extract_not_arg(Node *clause);
98+
static Node *extract_strong_not_arg(Node *clause);
9899
static bool list_member_strip(List *list, Expr *datum);
99100
static bool btree_predicate_proof(Expr *predicate, Node *clause,
100101
bool refute_it);
@@ -468,6 +469,8 @@ predicate_implied_by_recurse(Node *clause, Node *predicate)
468469
* Unfortunately we *cannot* use
469470
* NOT A R=> B if: B => A
470471
* because this type of reasoning fails to prove that B doesn't yield NULL.
472+
* We can however make the more limited deduction that
473+
* NOT A R=> A
471474
*
472475
* Other comments are as for predicate_implied_by_recurse().
473476
*----------
@@ -651,21 +654,18 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate)
651654

652655
case CLASS_ATOM:
653656

654-
#ifdef NOT_USED
655-
656657
/*
657-
* If A is a NOT-clause, A R=> B if B => A's arg
658+
* If A is a strong NOT-clause, A R=> B if B equals A's arg
658659
*
659-
* Unfortunately not: this would only prove that B is not-TRUE,
660-
* not that it's not NULL either. Keep this code as a comment
661-
* because it would be useful if we ever had a need for the weak
662-
* form of refutation.
660+
* We cannot make the stronger conclusion that B is refuted if
661+
* B implies A's arg; that would only prove that B is not-TRUE,
662+
* not that it's not NULL either. Hence use equal() rather than
663+
* predicate_implied_by_recurse(). We could do the latter if we
664+
* ever had a need for the weak form of refutation.
663665
*/
664-
not_arg = extract_not_arg(clause);
665-
if (not_arg &&
666-
predicate_implied_by_recurse(predicate, not_arg))
666+
not_arg = extract_strong_not_arg(clause);
667+
if (not_arg && equal(predicate, not_arg))
667668
return true;
668-
#endif
669669

670670
switch (pclass)
671671
{
@@ -1178,6 +1178,32 @@ extract_not_arg(Node *clause)
11781178
return NULL;
11791179
}
11801180

1181+
/*
1182+
* If clause asserts the falsity of a subclause, return that subclause;
1183+
* otherwise return NULL.
1184+
*/
1185+
static Node *
1186+
extract_strong_not_arg(Node *clause)
1187+
{
1188+
if (clause == NULL)
1189+
return NULL;
1190+
if (IsA(clause, BoolExpr))
1191+
{
1192+
BoolExpr *bexpr = (BoolExpr *) clause;
1193+
1194+
if (bexpr->boolop == NOT_EXPR)
1195+
return (Node *) linitial(bexpr->args);
1196+
}
1197+
else if (IsA(clause, BooleanTest))
1198+
{
1199+
BooleanTest *btest = (BooleanTest *) clause;
1200+
1201+
if (btest->booltesttype == IS_FALSE)
1202+
return (Node *) btest->arg;
1203+
}
1204+
return NULL;
1205+
}
1206+
11811207

11821208
/*
11831209
* Check whether an Expr is equal() to any member of a list, ignoring

0 commit comments

Comments
 (0)