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);
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,
/*
* 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
- * clauses in clause_list are CHECK constraints (where null is
- * effectively true) rather than WHERE clauses (where null is effectively
- * false).
+ * given predicate is true.
+ *
+ * We support two definitions of implication:
+ *
+ * "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
* 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
- * because the predicate is part of an index predicate that has passed
- * CheckPredicate().) 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.
+ * immutable functions and operators. (In many current uses this is known
+ * true because the predicate is part of an index predicate that has passed
+ * CheckPredicate(); otherwise, the caller must check it.) 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_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 */
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
- * that the clauses in clause_list are CHECK constraints (where null is
- * effectively true) rather than WHERE clauses (where null is effectively
- * false).
+ * predicate (that is, prove it 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
- * 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".)
+ * We support two definitions of refutation:
+ *
+ * "Strong" refutation: A refutes B means truth of A implies falsity of B.
+ * We use this to disprove a CHECK constraint given a WHERE clause, i.e.,
+ * prove that any row satisfying the WHERE clause would violate the CHECK
+ * constraint. (Observe we must prove B yields false, not just not-true.)
+ *
+ * "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
* 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 */
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);
}
/*----------
*
* 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
*/
static bool
predicate_implied_by_recurse(Node *clause, Node *predicate,
- bool clause_is_check)
+ bool weak)
{
PredIterInfoData clause_info;
PredIterInfoData pred_info;
iterate_begin(pitem, predicate, pred_info)
{
if (!predicate_implied_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = false;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (predicate_implied_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(citem, clause, clause_info)
{
if (predicate_implied_by_recurse(citem, predicate,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(citem, clause, clause_info)
{
if (predicate_implied_by_recurse(citem, predicate,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (predicate_implied_by_recurse(citem, pitem,
- clause_is_check))
+ weak))
{
presult = true;
break;
iterate_begin(citem, clause, clause_info)
{
if (!predicate_implied_by_recurse(citem, predicate,
- clause_is_check))
+ weak))
{
result = false;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (!predicate_implied_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = false;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (predicate_implied_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = true;
break;
return
predicate_implied_by_simple_clause((Expr *) predicate,
clause,
- clause_is_check);
+ weak);
}
break;
}
* 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.
- * Unfortunately we *cannot* use
+ * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN, although some
+ * 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.
- * We can however make the more limited deduction that
- * NOT A R=> A
+ * but here we must be careful about strong vs. weak refutation and make
+ * the appropriate type of implication proof (weak or strong respectively).
*
* 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;
iterate_begin(pitem, predicate, pred_info)
{
if (predicate_refuted_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(citem, clause, clause_info)
{
if (predicate_refuted_by_recurse(citem, predicate,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (!predicate_refuted_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = false;
break;
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;
/*
iterate_begin(citem, clause, clause_info)
{
if (predicate_refuted_by_recurse(citem, predicate,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (!predicate_refuted_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = false;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (predicate_refuted_by_recurse(citem, pitem,
- clause_is_check))
+ weak))
{
presult = true;
break;
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;
/*
iterate_begin(citem, clause, clause_info)
{
if (!predicate_refuted_by_recurse(citem, predicate,
- clause_is_check))
+ weak))
{
result = false;
break;
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
- * 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.
+ * Since A is strong, we may assume A's arg is false (not just
+ * not-true). If B weakly implies A's arg, then B can be neither
+ * true nor null, so that strong refutation is proven. If B
+ * strongly implies A's arg, then B cannot be true, so that weak
+ * 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)
iterate_begin(pitem, predicate, pred_info)
{
if (predicate_refuted_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = true;
break;
iterate_begin(pitem, predicate, pred_info)
{
if (!predicate_refuted_by_recurse(clause, pitem,
- clause_is_check))
+ weak))
{
result = false;
break;
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;
/*
return
predicate_refuted_by_simple_clause((Expr *) predicate,
clause,
- clause_is_check);
+ weak);
}
break;
}
* 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
- * functions in the expression are immutable, ie dependent only on their input
- * arguments --- but this was checked for the predicate by the caller.)
+ * kind of expression, and for either implication definition. (Actually,
+ * there is an implied assumption that the functions in the expression are
+ * 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
- * subtree of a WHERE clause. So, if the predicate is of the form "foo IS
- * NOT NULL", we can conclude that the predicate is implied if the clause is
- * a strict operator or function that has "foo" as an input. In this case
- * the clause must yield NULL when "foo" is NULL, which we can take as
- * equivalent to FALSE given the context. (Again, "foo" is already known
- * 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.
+ * If the predicate is of the form "foo IS NOT NULL", and we are considering
+ * strong implication, we can conclude that the predicate is implied if the
+ * clause is strict for "foo", i.e., it must yield NULL when "foo" is NULL.
+ * In that case truth of the clause requires that "foo" isn't NULL.
+ * (Again, this is a safe conclusion because "foo" must be immutable.)
+ * This doesn't work for weak implication, though.
*
* Finally, if both clauses are binary operator expressions, we may be able
* to prove something using the system's knowledge about operators; those
*/
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();
return true;
/* Next try the IS NOT NULL case */
- if (predicate && IsA(predicate, NullTest) &&
- ((NullTest *) predicate)->nulltesttype == IS_NOT_NULL)
+ if (!weak &&
+ 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) &&
- list_member_strip(((OpExpr *) clause)->args, nonnullarg) &&
- 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))
+ /* strictness of clause for foo implies foo IS NOT NULL */
+ if (clause_is_strict_for(clause, (Node *) ntest->arg))
return true;
}
return false; /* we can't succeed below... */
*
* We return true if able to prove the refutation, false if not.
*
- * Unlike the implication case, checking for equal() clauses isn't
- * helpful.
+ * Unlike the implication case, checking for equal() clauses isn't 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
- * that has "foo" as an input (see notes for implication case), or if the
- * 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.)
+ * the predicate is refuted if the clause is strict for "foo" (see notes for
+ * implication case), or is "foo IS NOT NULL". That works for either strong
+ * or weak refutation.
+ *
+ * A clause "foo IS NULL" refutes a predicate "foo IS NOT NULL" in all cases.
+ * If we are considering weak refutation, it also refutes a predicate that
+ * 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
*/
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();
{
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 */
- if (is_opclause(clause) &&
- 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))
+ /* strictness of clause for foo refutes foo IS NULL */
+ if (clause_is_strict_for(clause, (Node *) isnullarg))
return true;
/* foo IS NOT NULL refutes foo IS NULL */
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... */
}
/*
- * Check whether an Expr is equal() to any member of a list, ignoring
- * any top-level RelabelType nodes. This is legitimate for the purposes
- * we use it for (matching IS [NOT] NULL arguments to arguments of strict
- * functions) because RelabelType doesn't change null-ness. It's helpful
- * for cases such as a varchar argument of a strict function on text.
+ * Can we prove that "clause" returns NULL if "subexpr" does?
+ *
+ * The base case is that clause and subexpr are equal(). (We assume that
+ * the caller knows at least one of the input expressions is immutable,
+ * 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))
- datum = ((RelabelType *) datum)->arg;
+ /* safety checks */
+ if (clause == NULL || subexpr == NULL)
+ return false;
- foreach(cell, list)
- {
- Expr *elem = (Expr *) lfirst(cell);
+ /*
+ * Look through any RelabelType nodes, so that we can match, say,
+ * 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))
- elem = ((RelabelType *) elem)->arg;
+ /* Base case */
+ if (equal(clause, subexpr))
+ return true;
- 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;
* 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
* 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;
projects / postgresql / commitdiff