1/*-------------------------------------------------------------------------
4 * Routines to attempt to prove logical implications between predicate
7 * Portions Copyright (c) 1996-2025, PostgreSQL Global Development Group
8 * Portions Copyright (c) 1994, Regents of the University of California
12 * src/backend/optimizer/util/predtest.c
14 *-------------------------------------------------------------------------
34 * Proof attempts involving large arrays in ScalarArrayOpExpr nodes are
35 * likely to require O(N^2) time, and more often than not fail anyway.
36 * So we set an arbitrary limit on the number of array elements that
37 * we will allow to be treated as an AND or OR clause.
38 * XXX is it worth exposing this as a GUC knob?
40 #define MAX_SAOP_ARRAY_SIZE 100
43 * To avoid redundant coding in predicate_implied_by_recurse and
44 * predicate_refuted_by_recurse, we need to abstract out the notion of
45 * iterating over the components of an expression that is logically an AND
46 * or OR structure. There are multiple sorts of expression nodes that can
47 * be treated as ANDs or ORs, and we don't want to code each one separately.
48 * Hence, these types and support routines.
61 /* node-type-specific iteration state */
64 /* initialize to do the iteration */
66 /* next-component iteration function */
68 /* release resources when done with iteration */
72 #define iterate_begin(item, clause, info) \
75 (info).startup_fn((clause), &(info)); \
76 while ((item = (info).next_fn(&(info))) != NULL)
78 #define iterate_end(info) \
79 (info).cleanup_fn(&(info)); \
106 bool refute_it,
bool weak);
116 * predicate_implied_by
117 * Recursively checks whether the clauses in clause_list imply that the
118 * given predicate is true.
120 * We support two definitions of implication:
122 * "Strong" implication: A implies B means that truth of A implies truth of B.
123 * We use this to prove that a row satisfying one WHERE clause or index
124 * predicate must satisfy another one.
126 * "Weak" implication: A implies B means that non-falsity of A implies
127 * non-falsity of B ("non-false" means "either true or NULL"). We use this to
128 * prove that a row satisfying one CHECK constraint must satisfy another one.
130 * Strong implication can also be used to prove that a WHERE clause implies a
131 * CHECK constraint, although it will fail to prove a few cases where we could
132 * safely conclude that the implication holds. There's no support for proving
133 * the converse case, since only a few kinds of CHECK constraint would allow
136 * The top-level List structure of each list corresponds to an AND list.
137 * We assume that eval_const_expressions() has been applied and so there
138 * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
139 * including AND just below the top-level List structure).
140 * If this is not true we might fail to prove an implication that is
141 * valid, but no worse consequences will ensue.
143 * We assume the predicate has already been checked to contain only
144 * immutable functions and operators. (In many current uses this is known
145 * true because the predicate is part of an index predicate that has passed
146 * CheckPredicate(); otherwise, the caller must check it.) We dare not make
147 * deductions based on non-immutable functions, because they might change
148 * answers between the time we make the plan and the time we execute the plan.
149 * Immutability of functions in the clause_list is checked here, if necessary.
158 if (predicate_list ==
NIL)
159 return true;
/* no predicate: implication is vacuous */
160 if (clause_list ==
NIL)
161 return false;
/* no restriction: implication must fail */
164 * If either input is a single-element list, replace it with its lone
165 * member; this avoids one useless level of AND-recursion. We only need
166 * to worry about this at top level, since eval_const_expressions should
167 * have gotten rid of any trivial ANDs or ORs below that.
172 p = (
Node *) predicate_list;
176 c = (
Node *) clause_list;
178 /* And away we go ... */
183 * predicate_refuted_by
184 * Recursively checks whether the clauses in clause_list refute the given
185 * predicate (that is, prove it false).
187 * This is NOT the same as !(predicate_implied_by), though it is similar
188 * in the technique and structure of the code.
190 * We support two definitions of refutation:
192 * "Strong" refutation: A refutes B means truth of A implies falsity of B.
193 * We use this to disprove a CHECK constraint given a WHERE clause, i.e.,
194 * prove that any row satisfying the WHERE clause would violate the CHECK
195 * constraint. (Observe we must prove B yields false, not just not-true.)
197 * "Weak" refutation: A refutes B means truth of A implies non-truth of B
198 * (i.e., B must yield false or NULL). We use this to detect mutually
199 * contradictory WHERE clauses.
201 * Weak refutation can be proven in some cases where strong refutation doesn't
202 * hold, so it's useful to use it when possible. We don't currently have
203 * support for disproving one CHECK constraint based on another one, nor for
204 * disproving WHERE based on CHECK. (As with implication, the last case
205 * doesn't seem very practical. CHECK-vs-CHECK might be useful, but isn't
206 * currently needed anywhere.)
208 * The top-level List structure of each list corresponds to an AND list.
209 * We assume that eval_const_expressions() has been applied and so there
210 * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
211 * including AND just below the top-level List structure).
212 * If this is not true we might fail to prove an implication that is
213 * valid, but no worse consequences will ensue.
215 * We assume the predicate has already been checked to contain only
216 * immutable functions and operators. We dare not make deductions based on
217 * non-immutable functions, because they might change answers between the
218 * time we make the plan and the time we execute the plan.
219 * Immutability of functions in the clause_list is checked here, if necessary.
228 if (predicate_list ==
NIL)
229 return false;
/* no predicate: no refutation is possible */
230 if (clause_list ==
NIL)
231 return false;
/* no restriction: refutation must fail */
234 * If either input is a single-element list, replace it with its lone
235 * member; this avoids one useless level of AND-recursion. We only need
236 * to worry about this at top level, since eval_const_expressions should
237 * have gotten rid of any trivial ANDs or ORs below that.
242 p = (
Node *) predicate_list;
246 c = (
Node *) clause_list;
248 /* And away we go ... */
253 * predicate_implied_by_recurse
254 * Does the predicate implication test for non-NULL restriction and
257 * The logic followed here is ("=>" means "implies"):
258 * atom A => atom B iff: predicate_implied_by_simple_clause says so
259 * atom A => AND-expr B iff: A => each of B's components
260 * atom A => OR-expr B iff: A => any of B's components
261 * AND-expr A => atom B iff: any of A's components => B
262 * AND-expr A => AND-expr B iff: A => each of B's components
263 * AND-expr A => OR-expr B iff: A => any of B's components,
264 * *or* any of A's components => B
265 * OR-expr A => atom B iff: each of A's components => B
266 * OR-expr A => AND-expr B iff: A => each of B's components
267 * OR-expr A => OR-expr B iff: each of A's components => any of B's
269 * An "atom" is anything other than an AND or OR node. Notice that we don't
270 * have any special logic to handle NOT nodes; these should have been pushed
271 * down or eliminated where feasible during eval_const_expressions().
273 * All of these rules apply equally to strong or weak implication.
275 * We can't recursively expand either side first, but have to interleave
276 * the expansions per the above rules, to be sure we handle all of these
278 * (x OR y) => (x OR y OR z)
279 * (x AND y AND z) => (x AND y)
280 * (x AND y) => ((x AND y) OR z)
281 * ((x OR y) AND z) => (x OR y)
282 * This is still not an exhaustive test, but it handles most normal cases
283 * under the assumption that both inputs have been AND/OR flattened.
285 * We have to be prepared to handle RestrictInfo nodes in the restrictinfo
286 * tree, though not in the predicate tree.
298 /* skip through RestrictInfo */
313 * AND-clause => AND-clause if A implies each of B's items
331 * AND-clause => OR-clause if A implies any of B's items
333 * Needed to handle (x AND y) => ((x AND y) OR z)
350 * Also check if any of A's items implies B
352 * Needed to handle ((x OR y) AND z) => (x OR y)
369 * AND-clause => atom if any of A's items implies B
392 * OR-clause => OR-clause if each of A's items implies any
393 * of B's items. Messy but can't do it any more simply.
398 bool presult =
false;
412 result =
false;
/* doesn't imply any of B's */
423 * OR-clause => AND-clause if each of A's items implies B
425 * OR-clause => atom if each of A's items implies B
448 * atom => AND-clause if A implies each of B's items
466 * atom => OR-clause if A implies any of B's items
484 * atom => atom is the base case
495 elog(
ERROR,
"predicate_classify returned a bogus value");
500 * predicate_refuted_by_recurse
501 * Does the predicate refutation test for non-NULL restriction and
504 * The logic followed here is ("R=>" means "refutes"):
505 * atom A R=> atom B iff: predicate_refuted_by_simple_clause says so
506 * atom A R=> AND-expr B iff: A R=> any of B's components
507 * atom A R=> OR-expr B iff: A R=> each of B's components
508 * AND-expr A R=> atom B iff: any of A's components R=> B
509 * AND-expr A R=> AND-expr B iff: A R=> any of B's components,
510 * *or* any of A's components R=> B
511 * AND-expr A R=> OR-expr B iff: A R=> each of B's components
512 * OR-expr A R=> atom B iff: each of A's components R=> B
513 * OR-expr A R=> AND-expr B iff: each of A's components R=> any of B's
514 * OR-expr A R=> OR-expr B iff: A R=> each of B's components
516 * All of the above rules apply equally to strong or weak refutation.
518 * In addition, if the predicate is a NOT-clause then we can use
519 * A R=> NOT B if: A => B
520 * This works for several different SQL constructs that assert the non-truth
521 * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN, although some
522 * of them require that we prove strong implication. Likewise, we can use
523 * NOT A R=> B if: B => A
524 * but here we must be careful about strong vs. weak refutation and make
525 * the appropriate type of implication proof (weak or strong respectively).
527 * Other comments are as for predicate_implied_by_recurse().
540 /* skip through RestrictInfo */
555 * AND-clause R=> AND-clause if A refutes any of B's items
557 * Needed to handle (x AND y) R=> ((!x OR !y) AND z)
574 * Also check if any of A's items refutes B
576 * Needed to handle ((x OR y) AND z) R=> (!x AND !y)
593 * AND-clause R=> OR-clause if A refutes each of B's items
611 * If B is a NOT-type clause, A R=> B if A => B's arg
613 * Since, for either type of refutation, we are starting
614 * with the premise that A is true, we can use a strong
615 * implication test in all cases. That proves B's arg is
616 * true, which is more than we need for weak refutation if
617 * B is a simple NOT, but it allows not worrying about
618 * exactly which kind of negation clause we have.
627 * AND-clause R=> atom if any of A's items refutes B
650 * OR-clause R=> OR-clause if A refutes each of B's items
668 * OR-clause R=> AND-clause if each of A's items refutes
674 bool presult =
false;
688 result =
false;
/* citem refutes nothing */
698 * If B is a NOT-type clause, A R=> B if A => B's arg
700 * Same logic as for the AND-clause case above.
709 * OR-clause R=> atom if each of A's items refutes B
729 * If A is a strong NOT-clause, A R=> B if B => A's arg
731 * Since A is strong, we may assume A's arg is false (not just
732 * not-true). If B weakly implies A's arg, then B can be neither
733 * true nor null, so that strong refutation is proven. If B
734 * strongly implies A's arg, then B cannot be true, so that weak
735 * refutation is proven.
748 * atom R=> AND-clause if A refutes any of B's items
766 * atom R=> OR-clause if A refutes each of B's items
784 * If B is a NOT-type clause, A R=> B if A => B's arg
786 * Same logic as for the AND-clause case above.
795 * atom R=> atom is the base case
806 elog(
ERROR,
"predicate_classify returned a bogus value");
813 * Classify an expression node as AND-type, OR-type, or neither (an atom).
815 * If the expression is classified as AND- or OR-type, then *info is filled
816 * in with the functions needed to iterate over its components.
818 * This function also implements enforcement of MAX_SAOP_ARRAY_SIZE: if a
819 * ScalarArrayOpExpr's array has too many elements, we just classify it as an
820 * atom. (This will result in its being passed as-is to the simple_clause
821 * functions, many of which will fail to prove anything about it.) Note that we
822 * cannot just stop after considering MAX_SAOP_ARRAY_SIZE elements; in general
823 * that would result in wrong proofs, rather than failing to prove anything.
828 /* Caller should not pass us NULL, nor a RestrictInfo clause */
833 * If we see a List, assume it's an implicit-AND list; this is the correct
834 * semantics for lists of RestrictInfo nodes.
844 /* Handle normal AND and OR boolean clauses */
860 /* Handle ScalarArrayOpExpr */
867 * We can break this down into an AND or OR structure, but only if we
868 * know how to iterate through expressions for the array's elements.
869 * We can do that if the array operand is a non-null constant or a
872 if (arraynode &&
IsA(arraynode,
Const) &&
873 !((
Const *) arraynode)->constisnull)
899 /* None of the above, so it's an atom */
904 * PredIterInfo routines for iterating over regular Lists. The iteration
905 * state variable is the next ListCell to visit.
930 /* Nothing to clean up */
934 * BoolExpr needs its own startup function, but can use list_next_fn and
945 * PredIterInfo routines for iterating over a ScalarArrayOpExpr with a
946 * constant array operand.
969 /* Create working state struct */
973 /* Deconstruct the array literal */
977 &elmlen, &elmbyval, &elmalign);
980 elmlen, elmbyval, elmalign,
984 /* Set up a dummy OpExpr to return as the per-item node */
985 state->opexpr.xpr.type = T_OpExpr;
987 state->opexpr.opfuncid = saop->opfuncid;
988 state->opexpr.opresulttype = BOOLOID;
989 state->opexpr.opretset =
false;
991 state->opexpr.inputcollid = saop->inputcollid;
994 /* Set up a dummy Const node to hold the per-element values */
995 state->const_expr.xpr.type = T_Const;
997 state->const_expr.consttypmod = -1;
998 state->const_expr.constcollid = arrayconst->constcollid;
999 state->const_expr.constlen = elmlen;
1000 state->const_expr.constbyval = elmbyval;
1003 /* Initialize iteration state */
1004 state->next_elem = 0;
1032 * PredIterInfo routines for iterating over a ScalarArrayOpExpr with a
1033 * one-dimensional ArrayExpr array operand.
1048 /* Create working state struct */
1052 /* Set up a dummy OpExpr to return as the per-item node */
1053 state->opexpr.xpr.type = T_OpExpr;
1055 state->opexpr.opfuncid = saop->opfuncid;
1056 state->opexpr.opresulttype = BOOLOID;
1057 state->opexpr.opretset =
false;
1059 state->opexpr.inputcollid = saop->inputcollid;
1062 /* Initialize iteration variable to first member of ArrayExpr */
1091 * predicate_implied_by_simple_clause
1092 * Does the predicate implication test for a "simple clause" predicate
1093 * and a "simple clause" restriction.
1095 * We return true if able to prove the implication, false if not.
1101 /* Allow interrupting long proof attempts */
1105 * A simple and general rule is that a clause implies itself, hence we
1106 * check if they are equal(); this works for any kind of expression, and
1107 * for either implication definition. (Actually, there is an implied
1108 * assumption that the functions in the expression are immutable --- but
1109 * this was checked for the predicate by the caller.)
1114 /* Next we have some clause-type-specific strategies */
1122 * For boolean x, "x = TRUE" is equivalent to "x", likewise
1123 * "x = FALSE" is equivalent to "NOT x". These can be worth
1124 * checking because, while we preferentially simplify boolean
1125 * comparisons down to "x" and "NOT x", the other form has to
1126 * be dealt with anyway in the context of index conditions.
1128 * We could likewise check whether the predicate is boolean
1129 * equality to a constant; but there are no known use-cases
1130 * for that at the moment, assuming that the predicate has
1131 * been through constant-folding.
1134 if (op->
opno == BooleanEqualOperator)
1140 /* We might never see null Consts here, but better check */
1141 if (rightop &&
IsA(rightop,
Const) &&
1142 !((
Const *) rightop)->constisnull)
1148 /* X = true implies X */
1149 if (
equal(predicate, leftop))
1154 /* X = false implies NOT X */
1167 /* ... and some predicate-type-specific ones */
1179 * If the predicate is of the form "foo IS NOT NULL",
1180 * and we are considering strong implication, we can
1181 * conclude that the predicate is implied if the
1182 * clause is strict for "foo", i.e., it must yield
1183 * false or NULL when "foo" is NULL. In that case
1184 * truth of the clause ensures that "foo" isn't NULL.
1185 * (Again, this is a safe conclusion because "foo"
1186 * must be immutable.) This doesn't work for weak
1187 * implication, though. Also, "row IS NOT NULL" does
1188 * not act in the simple way we have in mind.
1191 !predntest->argisrow &&
1207 * Finally, if both clauses are binary operator expressions, we may be
1208 * able to prove something using the system's knowledge about operators;
1209 * those proof rules are encapsulated in operator_predicate_proof().
1215 * predicate_refuted_by_simple_clause
1216 * Does the predicate refutation test for a "simple clause" predicate
1217 * and a "simple clause" restriction.
1219 * We return true if able to prove the refutation, false if not.
1221 * The main motivation for covering IS [NOT] NULL cases is to support using
1222 * IS NULL/IS NOT NULL as partition-defining constraints.
1228 /* Allow interrupting long proof attempts */
1232 * A simple clause can't refute itself, so unlike the implication case,
1233 * checking for equal() clauses isn't helpful.
1235 * But relation_excluded_by_constraints() checks for self-contradictions
1236 * in a list of clauses, so that we may get here with predicate and clause
1237 * being actually pointer-equal, and that is worth eliminating quickly.
1239 if ((
Node *) predicate == clause)
1242 /* Next we have some clause-type-specific strategies */
1249 /* row IS NULL does not act in the simple way we have in mind */
1250 if (clausentest->argisrow)
1264 * row IS NULL does not act in the
1265 * simple way we have in mind
1267 if (predntest->argisrow)
1271 * foo IS NULL refutes foo IS NOT
1272 * NULL, at least in the non-row case,
1273 * for both strong and weak refutation
1285 * foo IS NULL weakly refutes any predicate that
1286 * is strict for foo, since then the predicate
1287 * must yield false or NULL (and since foo appears
1288 * in the predicate, it's known immutable).
1296 return false;
/* we can't succeed below... */
1308 /* ... and some predicate-type-specific ones */
1315 /* row IS NULL does not act in the simple way we have in mind */
1316 if (predntest->argisrow)
1330 * row IS NULL does not act in the
1331 * simple way we have in mind
1333 if (clausentest->argisrow)
1337 * foo IS NOT NULL refutes foo IS NULL
1338 * for both strong and weak refutation
1350 * When the predicate is of the form "foo IS
1351 * NULL", we can conclude that the predicate is
1352 * refuted if the clause is strict for "foo" (see
1353 * notes for implication case). That works for
1354 * either strong or weak refutation.
1366 return false;
/* we can't succeed below... */
1374 * Finally, if both clauses are binary operator expressions, we may be
1375 * able to prove something using the system's knowledge about operators.
1382 * If clause asserts the non-truth of a subclause, return that subclause;
1383 * otherwise return NULL.
1410 * If clause asserts the falsity of a subclause, return that subclause;
1411 * otherwise return NULL.
1437 * Can we prove that "clause" returns NULL (or FALSE) if "subexpr" is
1438 * assumed to yield NULL?
1440 * In most places in the planner, "strictness" refers to a guarantee that
1441 * an expression yields NULL output for a NULL input, and that's mostly what
1442 * we're looking for here. However, at top level where the clause is known
1443 * to yield boolean, it may be sufficient to prove that it cannot return TRUE
1444 * when "subexpr" is NULL. The caller should pass allow_false = true when
1445 * this weaker property is acceptable. (When this function recurses
1446 * internally, we pass down allow_false = false since we need to prove actual
1447 * nullness of the subexpression.)
1449 * We assume that the caller checked that least one of the input expressions
1450 * is immutable. All of the proof rules here involve matching "subexpr" to
1451 * some portion of "clause", so that this allows assuming that "subexpr" is
1452 * immutable without a separate check.
1454 * The base case is that clause and subexpr are equal().
1456 * We can also report success if the subexpr appears as a subexpression
1457 * of "clause" in a place where it'd force nullness of the overall result.
1465 if (clause == NULL || subexpr == NULL)
1469 * Look through any RelabelType nodes, so that we can match, say,
1470 * varcharcol with lower(varcharcol::text). (In general we could recurse
1471 * through any nullness-preserving, immutable operation.) We should not
1472 * see stacked RelabelTypes here.
1480 if (
equal(clause, subexpr))
1484 * If we have a strict operator or function, a NULL result is guaranteed
1485 * if any input is forced NULL by subexpr. This is OK even if the op or
1486 * func isn't immutable, since it won't even be called on NULL input.
1491 foreach(lc, ((
OpExpr *) clause)->args)
1501 foreach(lc, ((
FuncExpr *) clause)->args)
1510 * CoerceViaIO is strict (whether or not the I/O functions it calls are).
1511 * Likewise, ArrayCoerceExpr is strict for its array argument (regardless
1512 * of what the per-element expression is), ConvertRowtypeExpr is strict at
1513 * the row level, and CoerceToDomain is strict too. These are worth
1514 * checking mainly because it saves us having to explain to users why some
1515 * type coercions are known strict and others aren't.
1531 * ScalarArrayOpExpr is a special case. Note that we'd only reach here
1532 * with a ScalarArrayOpExpr clause if we failed to deconstruct it into an
1533 * AND or OR tree, as for example if it has too many array elements.
1542 * If we can prove the scalar input to be null, and the operator is
1543 * strict, then the SAOP result has to be null --- unless the array is
1544 * empty. For an empty array, we'd get either false (for ANY) or true
1545 * (for ALL). So if allow_false = true then the proof succeeds anyway
1546 * for the ANY case; otherwise we can only make the proof if we can
1547 * prove the array non-empty.
1554 if (allow_false && saop->
useOr)
1555 return true;
/* can succeed even if array is empty */
1557 if (arraynode &&
IsA(arraynode,
Const))
1563 * If array is constant NULL then we can succeed, as in the
1566 if (arrayconst->constisnull)
1569 /* Otherwise, we can compute the number of elements. */
1577 * We can also reliably count the number of array elements if
1578 * the input is a non-multidim ARRAY[] expression.
1583 /* Proof succeeds if array is definitely non-empty */
1589 * If we can prove the array input to be null, the proof succeeds in
1590 * all cases, since ScalarArrayOpExpr will always return NULL for a
1591 * NULL array. Otherwise, we're done here.
1597 * When recursing into an expression, we might find a NULL constant.
1598 * That's certainly NULL, whether it matches subexpr or not.
1601 return ((
Const *) clause)->constisnull;
1608 * Define "operator implication tables" for index operators ("cmptypes"),
1609 * and similar tables for refutation.
1611 * The row compare numbers defined by indexes (see access/cmptype.h) are:
1612 * 1 < 2 <= 3 = 4 >= 5 > 6 <>
1613 * and in addition we use 6 to represent <>. <> is not a btree-indexable
1614 * operator, but we assume here that if an equality operator of a btree
1615 * opfamily has a negator operator, the negator behaves as <> for the opfamily.
1616 * (This convention is also known to get_op_index_interpretation().)
1618 * RC_implies_table[] and RC_refutes_table[] are used for cases where we have
1619 * two identical subexpressions and we want to know whether one operator
1620 * expression implies or refutes the other. That is, if the "clause" is
1621 * EXPR1 clause_op EXPR2 and the "predicate" is EXPR1 pred_op EXPR2 for the
1622 * same two (immutable) subexpressions:
1623 * RC_implies_table[clause_op-1][pred_op-1]
1624 * is true if the clause implies the predicate
1625 * RC_refutes_table[clause_op-1][pred_op-1]
1626 * is true if the clause refutes the predicate
1627 * where clause_op and pred_op are cmptype numbers (from 1 to 6) in the
1628 * same opfamily. For example, "x < y" implies "x <= y" and refutes
1631 * RC_implic_table[] and RC_refute_table[] are used where we have two
1632 * constants that we need to compare. The interpretation of:
1634 * test_op = RC_implic_table[clause_op-1][pred_op-1]
1636 * where test_op, clause_op and pred_op are cmptypes (from 1 to 6)
1637 * of index operators, is as follows:
1639 * If you know, for some EXPR, that "EXPR clause_op CONST1" is true, and you
1640 * want to determine whether "EXPR pred_op CONST2" must also be true, then
1641 * you can use "CONST2 test_op CONST1" as a test. If this test returns true,
1642 * then the predicate expression must be true; if the test returns false,
1643 * then the predicate expression may be false.
1645 * For example, if clause is "Quantity > 10" and pred is "Quantity > 5"
1646 * then we test "5 <= 10" which evals to true, so clause implies pred.
1648 * Similarly, the interpretation of a RC_refute_table entry is:
1650 * If you know, for some EXPR, that "EXPR clause_op CONST1" is true, and you
1651 * want to determine whether "EXPR pred_op CONST2" must be false, then
1652 * you can use "CONST2 test_op CONST1" as a test. If this test returns true,
1653 * then the predicate expression must be false; if the test returns false,
1654 * then the predicate expression may be true.
1656 * For example, if clause is "Quantity > 10" and pred is "Quantity < 5"
1657 * then we test "5 <= 10" which evals to true, so clause refutes pred.
1659 * An entry where test_op == 0 means the implication cannot be determined.
1662 #define RCLT COMPARE_LT
1663 #define RCLE COMPARE_LE
1664 #define RCEQ COMPARE_EQ
1665 #define RCGE COMPARE_GE
1666 #define RCGT COMPARE_GT
1667 #define RCNE COMPARE_NE
1669/* We use "none" for 0/false to make the tables align nicely */
1674 * The predicate operator:
1687 * The predicate operator:
1700 * The predicate operator:
1713 * The predicate operator:
1726 * operator_predicate_proof
1727 * Does the predicate implication or refutation test for a "simple clause"
1728 * predicate and a "simple clause" restriction, when both are operator
1729 * clauses using related operators and identical input expressions.
1731 * When refute_it == false, we want to prove the predicate true;
1732 * when refute_it == true, we want to prove the predicate false.
1733 * (There is enough common code to justify handling these two cases
1734 * in one routine.) We return true if able to make the proof, false
1735 * if not able to prove it.
1737 * We mostly need not distinguish strong vs. weak implication/refutation here.
1738 * This depends on the assumption that a pair of related operators (i.e.,
1739 * commutators, negators, or btree opfamily siblings) will not return one NULL
1740 * and one non-NULL result for the same inputs. Then, for the proof types
1741 * where we start with an assumption of truth of the clause, the predicate
1742 * operator could not return NULL either, so it doesn't matter whether we are
1743 * trying to make a strong or weak proof. For weak implication, it could be
1744 * that the clause operator returned NULL, but then the predicate operator
1745 * would as well, so that the weak implication still holds. This argument
1746 * doesn't apply in the case where we are considering two different constant
1747 * values, since then the operators aren't being given identical inputs. But
1748 * we only support that for btree operators, for which we can assume that all
1749 * non-null inputs result in non-null outputs, so that it doesn't matter which
1750 * two non-null constants we consider. If either constant is NULL, we have
1751 * to think harder, but sometimes the proof still works, as explained below.
1753 * We can make proofs involving several expression forms (here "foo" and "bar"
1754 * represent subexpressions that are identical according to equal()):
1755 * "foo op1 bar" refutes "foo op2 bar" if op1 is op2's negator
1756 * "foo op1 bar" implies "bar op2 foo" if op1 is op2's commutator
1757 * "foo op1 bar" refutes "bar op2 foo" if op1 is negator of op2's commutator
1758 * "foo op1 bar" can imply/refute "foo op2 bar" based on btree semantics
1759 * "foo op1 bar" can imply/refute "bar op2 foo" based on btree semantics
1760 * "foo op1 const1" can imply/refute "foo op2 const2" based on btree semantics
1762 * For the last three cases, op1 and op2 have to be members of the same btree
1763 * operator family. When both subexpressions are identical, the idea is that,
1764 * for instance, x < y implies x <= y, independently of exactly what x and y
1765 * are. If we have two different constants compared to the same expression
1766 * foo, we have to execute a comparison between the two constant values
1767 * in order to determine the result; for instance, foo < c1 implies foo < c2
1768 * if c1 <= c2. We assume it's safe to compare the constants at plan time
1769 * if the comparison operator is immutable.
1771 * Note: all the operators and subexpressions have to be immutable for the
1772 * proof to be safe. We assume the predicate expression is entirely immutable,
1773 * so no explicit check on the subexpressions is needed here, but in some
1774 * cases we need an extra check of operator immutability. In particular,
1775 * btree opfamilies can contain cross-type operators that are merely stable,
1776 * and we dare not make deductions with those.
1780 bool refute_it,
bool weak)
1803 * Both expressions must be binary opclauses, else we can't do anything.
1805 * Note: in future we might extend this logic to other operator-based
1806 * constructs such as DistinctExpr. But the planner isn't very smart
1807 * about DistinctExpr in general, and this probably isn't the first place
1808 * to fix if you want to improve that.
1812 pred_opexpr = (
OpExpr *) predicate;
1817 clause_opexpr = (
OpExpr *) clause;
1822 * If they're marked with different collations then we can't do anything.
1823 * This is a cheap test so let's get it out of the way early.
1825 pred_collation = pred_opexpr->inputcollid;
1826 clause_collation = clause_opexpr->inputcollid;
1827 if (pred_collation != clause_collation)
1830 /* Grab the operator OIDs now too. We may commute these below. */
1831 pred_op = pred_opexpr->
opno;
1832 clause_op = clause_opexpr->
opno;
1835 * We have to match up at least one pair of input expressions.
1842 if (
equal(pred_leftop, clause_leftop))
1844 if (
equal(pred_rightop, clause_rightop))
1846 /* We have x op1 y and x op2 y */
1851 /* Fail unless rightops are both Consts */
1852 if (pred_rightop == NULL || !
IsA(pred_rightop,
Const))
1854 pred_const = (
Const *) pred_rightop;
1855 if (clause_rightop == NULL || !
IsA(clause_rightop,
Const))
1857 clause_const = (
Const *) clause_rightop;
1860 else if (
equal(pred_rightop, clause_rightop))
1862 /* Fail unless leftops are both Consts */
1863 if (pred_leftop == NULL || !
IsA(pred_leftop,
Const))
1865 pred_const = (
Const *) pred_leftop;
1866 if (clause_leftop == NULL || !
IsA(clause_leftop,
Const))
1868 clause_const = (
Const *) clause_leftop;
1869 /* Commute both operators so we can assume Consts are on the right */
1877 else if (
equal(pred_leftop, clause_rightop))
1879 if (
equal(pred_rightop, clause_leftop))
1881 /* We have x op1 y and y op2 x */
1882 /* Commute pred_op that we can treat this like a straight match */
1890 /* Fail unless pred_rightop/clause_leftop are both Consts */
1891 if (pred_rightop == NULL || !
IsA(pred_rightop,
Const))
1893 pred_const = (
Const *) pred_rightop;
1894 if (clause_leftop == NULL || !
IsA(clause_leftop,
Const))
1896 clause_const = (
Const *) clause_leftop;
1897 /* Commute clause_op so we can assume Consts are on the right */
1903 else if (
equal(pred_rightop, clause_leftop))
1905 /* Fail unless pred_leftop/clause_rightop are both Consts */
1906 if (pred_leftop == NULL || !
IsA(pred_leftop,
Const))
1908 pred_const = (
Const *) pred_leftop;
1909 if (clause_rightop == NULL || !
IsA(clause_rightop,
Const))
1911 clause_const = (
Const *) clause_rightop;
1912 /* Commute pred_op so we can assume Consts are on the right */
1919 /* Failed to match up any of the subexpressions, so we lose */
1924 * We have two identical subexpressions, and two other subexpressions that
1925 * are not identical but are both Consts; and we have commuted the
1926 * operators if necessary so that the Consts are on the right. We'll need
1927 * to compare the Consts' values. If either is NULL, we can't do that, so
1928 * usually the proof fails ... but in some cases we can claim success.
1930 if (clause_const->constisnull)
1932 /* If clause_op isn't strict, we can't prove anything */
1937 * At this point we know that the clause returns NULL. For proof
1938 * types that assume truth of the clause, this means the proof is
1939 * vacuously true (a/k/a "false implies anything"). That's all proof
1940 * types except weak implication.
1942 if (!(weak && !refute_it))
1946 * For weak implication, it's still possible for the proof to succeed,
1947 * if the predicate can also be proven NULL. In that case we've got
1948 * NULL => NULL which is valid for this proof type.
1950 if (pred_const->constisnull &&
op_strict(pred_op))
1952 /* Else the proof fails */
1955 if (pred_const->constisnull)
1958 * If the pred_op is strict, we know the predicate yields NULL, which
1959 * means the proof succeeds for either weak implication or weak
1964 /* Else the proof fails */
1969 * Lookup the constant-comparison operator using the system catalogs and
1970 * the operator implication tables.
1976 /* couldn't find a suitable comparison operator */
1981 * Evaluate the test. For this we need an EState.
1985 /* We can use the estate's working context to avoid memory leaks. */
1988 /* Build expression tree */
1992 (
Expr *) pred_const,
1993 (
Expr *) clause_const,
1997 /* Fill in opfuncids */
2000 /* Prepare it for execution */
2003 /* And execute it. */
2008 /* Get back to outer memory context */
2011 /* Release all the junk we just created */
2016 /* Treat a null result as non-proof ... but it's a tad fishy ... */
2025 * operator_same_subexprs_proof
2026 * Assuming that EXPR1 clause_op EXPR2 is true, try to prove or refute
2027 * EXPR1 pred_op EXPR2.
2029 * Return true if able to make the proof, false if not able to prove it.
2035 * A simple and general rule is that the predicate is proven if clause_op
2036 * and pred_op are the same, or refuted if they are each other's negators.
2037 * We need not check immutability since the pred_op is already known
2038 * immutable. (Actually, by this point we may have the commutator of a
2039 * known-immutable pred_op, but that should certainly be immutable too.
2040 * Likewise we don't worry whether the pred_op's negator is immutable.)
2042 * Note: the "same" case won't get here if we actually had EXPR1 clause_op
2043 * EXPR2 and EXPR1 pred_op EXPR2, because the overall-expression-equality
2044 * test in predicate_implied_by_simple_clause would have caught it. But
2045 * we can see the same operator after having commuted the pred_op.
2054 if (pred_op == clause_op)
2059 * Otherwise, see if we can determine the implication by finding the
2060 * operators' relationship via some btree opfamily.
2067 * We use a lookaside table to cache the result of btree proof operator
2068 * lookups, since the actual lookup is pretty expensive and doesn't change
2069 * for any given pair of operators (at least as long as pg_amop doesn't
2070 * change). A single hash entry stores both implication and refutation
2071 * results for a given pair of operators; but note we may have determined
2072 * only one of those sets of results as yet.
2082 /* the hash lookup key MUST BE FIRST */
2097 * lookup_proof_cache
2098 * Get, and fill in if necessary, the appropriate cache entry.
2106 bool same_subexprs =
false;
2109 List *pred_op_infos,
2115 * Find or make a cache entry for this pair of operators.
2119 /* First time through: initialize the hash table */
2127 /* Arrange to flush cache on pg_amop changes */
2133 key.pred_op = pred_op;
2134 key.clause_op = clause_op;
2140 /* new cache entry, set it invalid */
2146 /* pre-existing cache entry, see if we know the answer yet */
2152 * Try to find a btree opfamily containing the given operators.
2154 * We must find a btree opfamily that contains both operators, else the
2155 * implication can't be determined. Also, the opfamily must contain a
2156 * suitable test operator taking the operators' righthand datatypes.
2158 * If there are multiple matching opfamilies, assume we can use any one to
2159 * determine the logical relationship of the two operators and the correct
2160 * corresponding test operator. This should work for any logically
2161 * consistent opfamilies.
2163 * Note that we can determine the operators' relationship for
2164 * same-subexprs cases even from an opfamily that lacks a usable test
2165 * operator. This can happen in cases with incomplete sets of cross-type
2166 * comparison operators.
2169 if (clause_op_infos)
2171 else /* no point in looking */
2172 pred_op_infos =
NIL;
2174 foreach(lcp, pred_op_infos)
2179 foreach(lcc, clause_op_infos)
2186 /* Must find them in same opfamily */
2189 /* Lefttypes should match */
2192 pred_cmptype = pred_op_info->
cmptype;
2193 clause_cmptype = clause_op_info->
cmptype;
2196 * Check to see if we can make a proof for same-subexpressions
2197 * cases based on the operators' relationship in this opfamily.
2205 * Look up the "test" cmptype number in the implication table
2212 if (test_cmptype == 0)
2214 /* Can't determine implication using this interpretation */
2219 * See if opfamily has an operator for the test cmptype and the
2222 if (test_cmptype ==
RCNE)
2243 * Last check: test_op must be immutable.
2245 * Note that we require only the test_op to be immutable, not the
2246 * original clause_op. (pred_op is assumed to have been checked
2247 * immutable by the caller.) Essentially we are assuming that the
2248 * opfamily is consistent even if it contains operators that are
2251 if (
op_volatile(test_op) == PROVOLATILE_IMMUTABLE)
2267 /* couldn't find a suitable comparison operator */
2272 * If we think we were able to prove something about same-subexpressions
2273 * cases, check to make sure the clause_op is immutable before believing
2274 * it completely. (Usually, the clause_op would be immutable if the
2275 * pred_op is, but it's not entirely clear that this must be true in all
2276 * cases, so let's check.)
2278 if (same_subexprs &&
2280 same_subexprs =
false;
2282 /* Cache the results, whether positive or negative */
2300 * operator_same_subexprs_lookup
2301 * Convenience subroutine to look up the cached answer for
2302 * same-subexpressions cases.
2318 * Identify the comparison operator needed for a btree-operator
2319 * proof or refutation involving comparison of constants.
2321 * Given the truth of a clause "var clause_op const1", we are attempting to
2322 * prove or refute a predicate "var pred_op const2". The identities of the
2323 * two operators are sufficient to determine the operator (if any) to compare
2324 * const2 to const1 with.
2326 * Returns the OID of the operator to use, or InvalidOid if no proof is
2343 * Callback for pg_amop inval events
2353 /* Currently we just reset all entries; hard to be smarter ... */
#define DatumGetArrayTypeP(X)
void deconstruct_array(ArrayType *array, Oid elmtype, int elmlen, bool elmbyval, char elmalign, Datum **elemsp, bool **nullsp, int *nelemsp)
int ArrayGetNItems(int ndim, const int *dims)
#define OidIsValid(objectId)
void * hash_search(HTAB *hashp, const void *keyPtr, HASHACTION action, bool *foundPtr)
HTAB * hash_create(const char *tabname, int64 nelem, const HASHCTL *info, int flags)
void * hash_seq_search(HASH_SEQ_STATUS *status)
void hash_seq_init(HASH_SEQ_STATUS *status, HTAB *hashp)
bool equal(const void *a, const void *b)
ExprState * ExecInitExpr(Expr *node, PlanState *parent)
void FreeExecutorState(EState *estate)
EState * CreateExecutorState(void)
#define GetPerTupleExprContext(estate)
static Datum ExecEvalExprSwitchContext(ExprState *state, ExprContext *econtext, bool *isNull)
Assert(PointerIsAligned(start, uint64))
void CacheRegisterSyscacheCallback(int cacheid, SyscacheCallbackFunction func, Datum arg)
if(TABLE==NULL||TABLE_index==NULL)
List * list_copy(const List *oldlist)
void list_free(List *list)
void list_free_deep(List *list)
Oid get_opfamily_member_for_cmptype(Oid opfamily, Oid lefttype, Oid righttype, CompareType cmptype)
void get_typlenbyvalalign(Oid typid, int16 *typlen, bool *typbyval, char *typalign)
bool func_strict(Oid funcid)
List * get_op_index_interpretation(Oid opno)
char op_volatile(Oid opno)
Oid get_negator(Oid opno)
Oid get_commutator(Oid opno)
Expr * make_opclause(Oid opno, Oid opresulttype, bool opretset, Expr *leftop, Expr *rightop, Oid opcollid, Oid inputcollid)
void pfree(void *pointer)
#define CHECK_FOR_INTERRUPTS()
void fix_opfuncids(Node *node)
static bool is_andclause(const void *clause)
static bool is_orclause(const void *clause)
static bool is_opclause(const void *clause)
static bool is_funcclause(const void *clause)
static bool is_notclause(const void *clause)
static Expr * get_notclausearg(const void *notclause)
#define IsA(nodeptr, _type_)
static MemoryContext MemoryContextSwitchTo(MemoryContext context)
static int list_length(const List *l)
static ListCell * list_head(const List *l)
static ListCell * lnext(const List *l, const ListCell *c)
static bool DatumGetBool(Datum X)
static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, bool weak)
static Node * arrayconst_next_fn(PredIterInfo info)
struct PredIterInfoData * PredIterInfo
static Node * arrayexpr_next_fn(PredIterInfo info)
bool predicate_refuted_by(List *predicate_list, List *clause_list, bool weak)
static const CompareType RC_implic_table[6][6]
static bool operator_same_subexprs_proof(Oid pred_op, Oid clause_op, bool refute_it)
static HTAB * OprProofCacheHash
#define iterate_end(info)
static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, uint32 hashvalue)
static const bool RC_refutes_table[6][6]
static const bool RC_implies_table[6][6]
static bool predicate_implied_by_recurse(Node *clause, Node *predicate, bool weak)
static OprProofCacheEntry * lookup_proof_cache(Oid pred_op, Oid clause_op, bool refute_it)
static void arrayexpr_startup_fn(Node *clause, PredIterInfo info)
struct OprProofCacheEntry OprProofCacheEntry
static Node * extract_strong_not_arg(Node *clause)
static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause, bool weak)
static Node * extract_not_arg(Node *clause)
static PredClass predicate_classify(Node *clause, PredIterInfo info)
static bool predicate_refuted_by_recurse(Node *clause, Node *predicate, bool weak)
static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
static bool operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it, bool weak)
bool predicate_implied_by(List *predicate_list, List *clause_list, bool weak)
static void boolexpr_startup_fn(Node *clause, PredIterInfo info)
static void arrayconst_startup_fn(Node *clause, PredIterInfo info)
#define MAX_SAOP_ARRAY_SIZE
static void list_cleanup_fn(PredIterInfo info)
struct PredIterInfoData PredIterInfoData
struct OprProofCacheKey OprProofCacheKey
static Node * list_next_fn(PredIterInfo info)
static void arrayconst_cleanup_fn(PredIterInfo info)
static Oid get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it)
#define iterate_begin(item, clause, info)
static void list_startup_fn(Node *clause, PredIterInfo info)
static void arrayexpr_cleanup_fn(PredIterInfo info)
static bool operator_same_subexprs_lookup(Oid pred_op, Oid clause_op, bool refute_it)
static const CompareType RC_refute_table[6][6]
BoolTestType booltesttype
MemoryContext es_query_cxt
NullTestType nulltesttype
bool same_subexprs_refutes
bool same_subexprs_implies
void(* startup_fn)(Node *clause, PredIterInfo info)
void(* cleanup_fn)(PredIterInfo info)
Node *(* next_fn)(PredIterInfo info)