Line data Source code
1 : /*-------------------------------------------------------------------------
2 : *
3 : * predtest.c
4 : * Routines to attempt to prove logical implications between predicate
5 : * expressions.
6 : *
7 : * Portions Copyright (c) 1996-2026, PostgreSQL Global Development Group
8 : * Portions Copyright (c) 1994, Regents of the University of California
9 : *
10 : *
11 : * IDENTIFICATION
12 : * src/backend/optimizer/util/predtest.c
13 : *
14 : *-------------------------------------------------------------------------
15 : */
16 : #include "postgres.h"
17 :
18 : #include "catalog/pg_operator.h"
19 : #include "catalog/pg_proc.h"
20 : #include "catalog/pg_type.h"
21 : #include "executor/executor.h"
22 : #include "miscadmin.h"
23 : #include "nodes/makefuncs.h"
24 : #include "nodes/nodeFuncs.h"
25 : #include "nodes/pathnodes.h"
26 : #include "optimizer/optimizer.h"
27 : #include "utils/array.h"
28 : #include "utils/hsearch.h"
29 : #include "utils/inval.h"
30 : #include "utils/lsyscache.h"
31 : #include "utils/syscache.h"
32 :
33 :
34 : /*
35 : * Proof attempts involving large arrays in ScalarArrayOpExpr nodes are
36 : * likely to require O(N^2) time, and more often than not fail anyway.
37 : * So we set an arbitrary limit on the number of array elements that
38 : * we will allow to be treated as an AND or OR clause.
39 : * XXX is it worth exposing this as a GUC knob?
40 : */
41 : #define MAX_SAOP_ARRAY_SIZE 100
42 :
43 : /*
44 : * To avoid redundant coding in predicate_implied_by_recurse and
45 : * predicate_refuted_by_recurse, we need to abstract out the notion of
46 : * iterating over the components of an expression that is logically an AND
47 : * or OR structure. There are multiple sorts of expression nodes that can
48 : * be treated as ANDs or ORs, and we don't want to code each one separately.
49 : * Hence, these types and support routines.
50 : */
51 : typedef enum
52 : {
53 : CLASS_ATOM, /* expression that's not AND or OR */
54 : CLASS_AND, /* expression with AND semantics */
55 : CLASS_OR, /* expression with OR semantics */
56 : } PredClass;
57 :
58 : typedef struct PredIterInfoData *PredIterInfo;
59 :
60 : typedef struct PredIterInfoData
61 : {
62 : /* node-type-specific iteration state */
63 : void *state;
64 : List *state_list;
65 : /* initialize to do the iteration */
66 : void (*startup_fn) (Node *clause, PredIterInfo info);
67 : /* next-component iteration function */
68 : Node *(*next_fn) (PredIterInfo info);
69 : /* release resources when done with iteration */
70 : void (*cleanup_fn) (PredIterInfo info);
71 : } PredIterInfoData;
72 :
73 : #define iterate_begin(item, clause, info) \
74 : do { \
75 : Node *item; \
76 : (info).startup_fn((clause), &(info)); \
77 : while ((item = (info).next_fn(&(info))) != NULL)
78 :
79 : #define iterate_end(info) \
80 : (info).cleanup_fn(&(info)); \
81 : } while (0)
82 :
83 :
84 : static bool predicate_implied_by_recurse(Node *clause, Node *predicate,
85 : bool weak);
86 : static bool predicate_refuted_by_recurse(Node *clause, Node *predicate,
87 : bool weak);
88 : static PredClass predicate_classify(Node *clause, PredIterInfo info);
89 : static void list_startup_fn(Node *clause, PredIterInfo info);
90 : static Node *list_next_fn(PredIterInfo info);
91 : static void list_cleanup_fn(PredIterInfo info);
92 : static void boolexpr_startup_fn(Node *clause, PredIterInfo info);
93 : static void arrayconst_startup_fn(Node *clause, PredIterInfo info);
94 : static Node *arrayconst_next_fn(PredIterInfo info);
95 : static void arrayconst_cleanup_fn(PredIterInfo info);
96 : static void arrayexpr_startup_fn(Node *clause, PredIterInfo info);
97 : static Node *arrayexpr_next_fn(PredIterInfo info);
98 : static void arrayexpr_cleanup_fn(PredIterInfo info);
99 : static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
100 : bool weak);
101 : static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
102 : bool weak);
103 : static Node *extract_not_arg(Node *clause);
104 : static Node *extract_strong_not_arg(Node *clause);
105 : static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false);
106 : static bool operator_predicate_proof(Expr *predicate, Node *clause,
107 : bool refute_it, bool weak);
108 : static bool operator_same_subexprs_proof(Oid pred_op, Oid clause_op,
109 : bool refute_it);
110 : static bool operator_same_subexprs_lookup(Oid pred_op, Oid clause_op,
111 : bool refute_it);
112 : static Oid get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it);
113 : static void InvalidateOprProofCacheCallBack(Datum arg, SysCacheIdentifier cacheid,
114 : uint32 hashvalue);
115 :
116 :
117 : /*
118 : * predicate_implied_by
119 : * Recursively checks whether the clauses in clause_list imply that the
120 : * given predicate is true.
121 : *
122 : * We support two definitions of implication:
123 : *
124 : * "Strong" implication: A implies B means that truth of A implies truth of B.
125 : * We use this to prove that a row satisfying one WHERE clause or index
126 : * predicate must satisfy another one.
127 : *
128 : * "Weak" implication: A implies B means that non-falsity of A implies
129 : * non-falsity of B ("non-false" means "either true or NULL"). We use this to
130 : * prove that a row satisfying one CHECK constraint must satisfy another one.
131 : *
132 : * Strong implication can also be used to prove that a WHERE clause implies a
133 : * CHECK constraint, although it will fail to prove a few cases where we could
134 : * safely conclude that the implication holds. There's no support for proving
135 : * the converse case, since only a few kinds of CHECK constraint would allow
136 : * deducing anything.
137 : *
138 : * The top-level List structure of each list corresponds to an AND list.
139 : * We assume that eval_const_expressions() has been applied and so there
140 : * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
141 : * including AND just below the top-level List structure).
142 : * If this is not true we might fail to prove an implication that is
143 : * valid, but no worse consequences will ensue.
144 : *
145 : * We assume the predicate has already been checked to contain only
146 : * immutable functions and operators. (In many current uses this is known
147 : * true because the predicate is part of an index predicate that has passed
148 : * CheckPredicate(); otherwise, the caller must check it.) We dare not make
149 : * deductions based on non-immutable functions, because they might change
150 : * answers between the time we make the plan and the time we execute the plan.
151 : * Immutability of functions in the clause_list is checked here, if necessary.
152 : */
153 : bool
154 63107 : predicate_implied_by(List *predicate_list, List *clause_list,
155 : bool weak)
156 : {
157 : Node *p,
158 : *c;
159 :
160 63107 : if (predicate_list == NIL)
161 1258 : return true; /* no predicate: implication is vacuous */
162 61849 : if (clause_list == NIL)
163 3328 : return false; /* no restriction: implication must fail */
164 :
165 : /*
166 : * If either input is a single-element list, replace it with its lone
167 : * member; this avoids one useless level of AND-recursion. We only need
168 : * to worry about this at top level, since eval_const_expressions should
169 : * have gotten rid of any trivial ANDs or ORs below that.
170 : */
171 58521 : if (list_length(predicate_list) == 1)
172 58333 : p = (Node *) linitial(predicate_list);
173 : else
174 188 : p = (Node *) predicate_list;
175 58521 : if (list_length(clause_list) == 1)
176 48979 : c = (Node *) linitial(clause_list);
177 : else
178 9542 : c = (Node *) clause_list;
179 :
180 : /* And away we go ... */
181 58521 : return predicate_implied_by_recurse(c, p, weak);
182 : }
183 :
184 : /*
185 : * predicate_refuted_by
186 : * Recursively checks whether the clauses in clause_list refute the given
187 : * predicate (that is, prove it false).
188 : *
189 : * This is NOT the same as !(predicate_implied_by), though it is similar
190 : * in the technique and structure of the code.
191 : *
192 : * We support two definitions of refutation:
193 : *
194 : * "Strong" refutation: A refutes B means truth of A implies falsity of B.
195 : * We use this to disprove a CHECK constraint given a WHERE clause, i.e.,
196 : * prove that any row satisfying the WHERE clause would violate the CHECK
197 : * constraint. (Observe we must prove B yields false, not just not-true.)
198 : *
199 : * "Weak" refutation: A refutes B means truth of A implies non-truth of B
200 : * (i.e., B must yield false or NULL). We use this to detect mutually
201 : * contradictory WHERE clauses.
202 : *
203 : * Weak refutation can be proven in some cases where strong refutation doesn't
204 : * hold, so it's useful to use it when possible. We don't currently have
205 : * support for disproving one CHECK constraint based on another one, nor for
206 : * disproving WHERE based on CHECK. (As with implication, the last case
207 : * doesn't seem very practical. CHECK-vs-CHECK might be useful, but isn't
208 : * currently needed anywhere.)
209 : *
210 : * The top-level List structure of each list corresponds to an AND list.
211 : * We assume that eval_const_expressions() has been applied and so there
212 : * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
213 : * including AND just below the top-level List structure).
214 : * If this is not true we might fail to prove an implication that is
215 : * valid, but no worse consequences will ensue.
216 : *
217 : * We assume the predicate has already been checked to contain only
218 : * immutable functions and operators. We dare not make deductions based on
219 : * non-immutable functions, because they might change answers between the
220 : * time we make the plan and the time we execute the plan.
221 : * Immutability of functions in the clause_list is checked here, if necessary.
222 : */
223 : bool
224 40681 : predicate_refuted_by(List *predicate_list, List *clause_list,
225 : bool weak)
226 : {
227 : Node *p,
228 : *c;
229 :
230 40681 : if (predicate_list == NIL)
231 15515 : return false; /* no predicate: no refutation is possible */
232 25166 : if (clause_list == NIL)
233 0 : return false; /* no restriction: refutation must fail */
234 :
235 : /*
236 : * If either input is a single-element list, replace it with its lone
237 : * member; this avoids one useless level of AND-recursion. We only need
238 : * to worry about this at top level, since eval_const_expressions should
239 : * have gotten rid of any trivial ANDs or ORs below that.
240 : */
241 25166 : if (list_length(predicate_list) == 1)
242 18883 : p = (Node *) linitial(predicate_list);
243 : else
244 6283 : p = (Node *) predicate_list;
245 25166 : if (list_length(clause_list) == 1)
246 18559 : c = (Node *) linitial(clause_list);
247 : else
248 6607 : c = (Node *) clause_list;
249 :
250 : /* And away we go ... */
251 25166 : return predicate_refuted_by_recurse(c, p, weak);
252 : }
253 :
254 : /*----------
255 : * predicate_implied_by_recurse
256 : * Does the predicate implication test for non-NULL restriction and
257 : * predicate clauses.
258 : *
259 : * The logic followed here is ("=>" means "implies"):
260 : * atom A => atom B iff: predicate_implied_by_simple_clause says so
261 : * atom A => AND-expr B iff: A => each of B's components
262 : * atom A => OR-expr B iff: A => any of B's components
263 : * AND-expr A => atom B iff: any of A's components => B
264 : * AND-expr A => AND-expr B iff: A => each of B's components
265 : * AND-expr A => OR-expr B iff: A => any of B's components,
266 : * *or* any of A's components => B
267 : * OR-expr A => atom B iff: each of A's components => B
268 : * OR-expr A => AND-expr B iff: A => each of B's components
269 : * OR-expr A => OR-expr B iff: each of A's components => any of B's
270 : *
271 : * An "atom" is anything other than an AND or OR node. Notice that we don't
272 : * have any special logic to handle NOT nodes; these should have been pushed
273 : * down or eliminated where feasible during eval_const_expressions().
274 : *
275 : * All of these rules apply equally to strong or weak implication.
276 : *
277 : * We can't recursively expand either side first, but have to interleave
278 : * the expansions per the above rules, to be sure we handle all of these
279 : * examples:
280 : * (x OR y) => (x OR y OR z)
281 : * (x AND y AND z) => (x AND y)
282 : * (x AND y) => ((x AND y) OR z)
283 : * ((x OR y) AND z) => (x OR y)
284 : * This is still not an exhaustive test, but it handles most normal cases
285 : * under the assumption that both inputs have been AND/OR flattened.
286 : *
287 : * We have to be prepared to handle RestrictInfo nodes in the restrictinfo
288 : * tree, though not in the predicate tree.
289 : *----------
290 : */
291 : static bool
292 109399 : predicate_implied_by_recurse(Node *clause, Node *predicate,
293 : bool weak)
294 : {
295 : PredIterInfoData clause_info;
296 : PredIterInfoData pred_info;
297 : PredClass pclass;
298 : bool result;
299 :
300 : /* skip through RestrictInfo */
301 : Assert(clause != NULL);
302 109399 : if (IsA(clause, RestrictInfo))
303 2712 : clause = (Node *) ((RestrictInfo *) clause)->clause;
304 :
305 109399 : pclass = predicate_classify(predicate, &pred_info);
306 :
307 109399 : switch (predicate_classify(clause, &clause_info))
308 : {
309 12827 : case CLASS_AND:
310 12827 : switch (pclass)
311 : {
312 386 : case CLASS_AND:
313 :
314 : /*
315 : * AND-clause => AND-clause if A implies each of B's items
316 : */
317 386 : result = true;
318 717 : iterate_begin(pitem, predicate, pred_info)
319 : {
320 661 : if (!predicate_implied_by_recurse(clause, pitem,
321 : weak))
322 : {
323 330 : result = false;
324 330 : break;
325 : }
326 : }
327 386 : iterate_end(pred_info);
328 386 : return result;
329 :
330 729 : case CLASS_OR:
331 :
332 : /*
333 : * AND-clause => OR-clause if A implies any of B's items
334 : *
335 : * Needed to handle (x AND y) => ((x AND y) OR z)
336 : */
337 729 : result = false;
338 2468 : iterate_begin(pitem, predicate, pred_info)
339 : {
340 1786 : if (predicate_implied_by_recurse(clause, pitem,
341 : weak))
342 : {
343 47 : result = true;
344 47 : break;
345 : }
346 : }
347 729 : iterate_end(pred_info);
348 729 : if (result)
349 47 : return result;
350 :
351 : /*
352 : * Also check if any of A's items implies B
353 : *
354 : * Needed to handle ((x OR y) AND z) => (x OR y)
355 : */
356 1954 : iterate_begin(citem, clause, clause_info)
357 : {
358 1359 : if (predicate_implied_by_recurse(citem, predicate,
359 : weak))
360 : {
361 87 : result = true;
362 87 : break;
363 : }
364 : }
365 682 : iterate_end(clause_info);
366 682 : return result;
367 :
368 11712 : case CLASS_ATOM:
369 :
370 : /*
371 : * AND-clause => atom if any of A's items implies B
372 : */
373 11712 : result = false;
374 34616 : iterate_begin(citem, clause, clause_info)
375 : {
376 23813 : if (predicate_implied_by_recurse(citem, predicate,
377 : weak))
378 : {
379 909 : result = true;
380 909 : break;
381 : }
382 : }
383 11712 : iterate_end(clause_info);
384 11712 : return result;
385 : }
386 0 : break;
387 :
388 2006 : case CLASS_OR:
389 2006 : switch (pclass)
390 : {
391 539 : case CLASS_OR:
392 :
393 : /*
394 : * OR-clause => OR-clause if each of A's items implies any
395 : * of B's items. Messy but can't do it any more simply.
396 : */
397 539 : result = true;
398 910 : iterate_begin(citem, clause, clause_info)
399 : {
400 751 : bool presult = false;
401 :
402 1894 : iterate_begin(pitem, predicate, pred_info)
403 : {
404 1514 : if (predicate_implied_by_recurse(citem, pitem,
405 : weak))
406 : {
407 371 : presult = true;
408 371 : break;
409 : }
410 : }
411 751 : iterate_end(pred_info);
412 751 : if (!presult)
413 : {
414 380 : result = false; /* doesn't imply any of B's */
415 380 : break;
416 : }
417 : }
418 539 : iterate_end(clause_info);
419 539 : return result;
420 :
421 1467 : case CLASS_AND:
422 : case CLASS_ATOM:
423 :
424 : /*
425 : * OR-clause => AND-clause if each of A's items implies B
426 : *
427 : * OR-clause => atom if each of A's items implies B
428 : */
429 1467 : result = true;
430 1834 : iterate_begin(citem, clause, clause_info)
431 : {
432 1789 : if (!predicate_implied_by_recurse(citem, predicate,
433 : weak))
434 : {
435 1422 : result = false;
436 1422 : break;
437 : }
438 : }
439 1467 : iterate_end(clause_info);
440 1467 : return result;
441 : }
442 0 : break;
443 :
444 94566 : case CLASS_ATOM:
445 94566 : switch (pclass)
446 : {
447 1488 : case CLASS_AND:
448 :
449 : /*
450 : * atom => AND-clause if A implies each of B's items
451 : */
452 1488 : result = true;
453 1817 : iterate_begin(pitem, predicate, pred_info)
454 : {
455 1800 : if (!predicate_implied_by_recurse(clause, pitem,
456 : weak))
457 : {
458 1471 : result = false;
459 1471 : break;
460 : }
461 : }
462 1488 : iterate_end(pred_info);
463 1488 : return result;
464 :
465 5842 : case CLASS_OR:
466 :
467 : /*
468 : * atom => OR-clause if A implies any of B's items
469 : */
470 5842 : result = false;
471 20519 : iterate_begin(pitem, predicate, pred_info)
472 : {
473 14883 : if (predicate_implied_by_recurse(clause, pitem,
474 : weak))
475 : {
476 206 : result = true;
477 206 : break;
478 : }
479 : }
480 5842 : iterate_end(pred_info);
481 5842 : return result;
482 :
483 87236 : case CLASS_ATOM:
484 :
485 : /*
486 : * atom => atom is the base case
487 : */
488 : return
489 87236 : predicate_implied_by_simple_clause((Expr *) predicate,
490 : clause,
491 : weak);
492 : }
493 0 : break;
494 : }
495 :
496 : /* can't get here */
497 0 : elog(ERROR, "predicate_classify returned a bogus value");
498 : return false;
499 : }
500 :
501 : /*----------
502 : * predicate_refuted_by_recurse
503 : * Does the predicate refutation test for non-NULL restriction and
504 : * predicate clauses.
505 : *
506 : * The logic followed here is ("R=>" means "refutes"):
507 : * atom A R=> atom B iff: predicate_refuted_by_simple_clause says so
508 : * atom A R=> AND-expr B iff: A R=> any of B's components
509 : * atom A R=> OR-expr B iff: A R=> each of B's components
510 : * AND-expr A R=> atom B iff: any of A's components R=> B
511 : * AND-expr A R=> AND-expr B iff: A R=> any of B's components,
512 : * *or* any of A's components R=> B
513 : * AND-expr A R=> OR-expr B iff: A R=> each of B's components
514 : * OR-expr A R=> atom B iff: each of A's components R=> B
515 : * OR-expr A R=> AND-expr B iff: each of A's components R=> any of B's
516 : * OR-expr A R=> OR-expr B iff: A R=> each of B's components
517 : *
518 : * All of the above rules apply equally to strong or weak refutation.
519 : *
520 : * In addition, if the predicate is a NOT-clause then we can use
521 : * A R=> NOT B if: A => B
522 : * This works for several different SQL constructs that assert the non-truth
523 : * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN, although some
524 : * of them require that we prove strong implication. Likewise, we can use
525 : * NOT A R=> B if: B => A
526 : * but here we must be careful about strong vs. weak refutation and make
527 : * the appropriate type of implication proof (weak or strong respectively).
528 : *
529 : * Other comments are as for predicate_implied_by_recurse().
530 : *----------
531 : */
532 : static bool
533 189567 : predicate_refuted_by_recurse(Node *clause, Node *predicate,
534 : bool weak)
535 : {
536 : PredIterInfoData clause_info;
537 : PredIterInfoData pred_info;
538 : PredClass pclass;
539 : Node *not_arg;
540 : bool result;
541 :
542 : /* skip through RestrictInfo */
543 : Assert(clause != NULL);
544 189567 : if (IsA(clause, RestrictInfo))
545 15465 : clause = (Node *) ((RestrictInfo *) clause)->clause;
546 :
547 189567 : pclass = predicate_classify(predicate, &pred_info);
548 :
549 189567 : switch (predicate_classify(clause, &clause_info))
550 : {
551 28501 : case CLASS_AND:
552 28501 : switch (pclass)
553 : {
554 6500 : case CLASS_AND:
555 :
556 : /*
557 : * AND-clause R=> AND-clause if A refutes any of B's items
558 : *
559 : * Needed to handle (x AND y) R=> ((!x OR !y) AND z)
560 : */
561 6500 : result = false;
562 22630 : iterate_begin(pitem, predicate, pred_info)
563 : {
564 16297 : if (predicate_refuted_by_recurse(clause, pitem,
565 : weak))
566 : {
567 167 : result = true;
568 167 : break;
569 : }
570 : }
571 6500 : iterate_end(pred_info);
572 6500 : if (result)
573 167 : return result;
574 :
575 : /*
576 : * Also check if any of A's items refutes B
577 : *
578 : * Needed to handle ((x OR y) AND z) R=> (!x AND !y)
579 : */
580 22941 : iterate_begin(citem, clause, clause_info)
581 : {
582 16610 : if (predicate_refuted_by_recurse(citem, predicate,
583 : weak))
584 : {
585 2 : result = true;
586 2 : break;
587 : }
588 : }
589 6333 : iterate_end(clause_info);
590 6333 : return result;
591 :
592 2666 : case CLASS_OR:
593 :
594 : /*
595 : * AND-clause R=> OR-clause if A refutes each of B's items
596 : */
597 2666 : result = true;
598 3560 : iterate_begin(pitem, predicate, pred_info)
599 : {
600 3558 : if (!predicate_refuted_by_recurse(clause, pitem,
601 : weak))
602 : {
603 2664 : result = false;
604 2664 : break;
605 : }
606 : }
607 2666 : iterate_end(pred_info);
608 2666 : return result;
609 :
610 19335 : case CLASS_ATOM:
611 :
612 : /*
613 : * If B is a NOT-type clause, A R=> B if A => B's arg
614 : *
615 : * Since, for either type of refutation, we are starting
616 : * with the premise that A is true, we can use a strong
617 : * implication test in all cases. That proves B's arg is
618 : * true, which is more than we need for weak refutation if
619 : * B is a simple NOT, but it allows not worrying about
620 : * exactly which kind of negation clause we have.
621 : */
622 19335 : not_arg = extract_not_arg(predicate);
623 19592 : if (not_arg &&
624 257 : predicate_implied_by_recurse(clause, not_arg,
625 : false))
626 13 : return true;
627 :
628 : /*
629 : * AND-clause R=> atom if any of A's items refutes B
630 : */
631 19322 : result = false;
632 70395 : iterate_begin(citem, clause, clause_info)
633 : {
634 52245 : if (predicate_refuted_by_recurse(citem, predicate,
635 : weak))
636 : {
637 1172 : result = true;
638 1172 : break;
639 : }
640 : }
641 19322 : iterate_end(clause_info);
642 19322 : return result;
643 : }
644 0 : break;
645 :
646 11832 : case CLASS_OR:
647 11832 : switch (pclass)
648 : {
649 1077 : case CLASS_OR:
650 :
651 : /*
652 : * OR-clause R=> OR-clause if A refutes each of B's items
653 : */
654 1077 : result = true;
655 1108 : iterate_begin(pitem, predicate, pred_info)
656 : {
657 1108 : if (!predicate_refuted_by_recurse(clause, pitem,
658 : weak))
659 : {
660 1077 : result = false;
661 1077 : break;
662 : }
663 : }
664 1077 : iterate_end(pred_info);
665 1077 : return result;
666 :
667 2546 : case CLASS_AND:
668 :
669 : /*
670 : * OR-clause R=> AND-clause if each of A's items refutes
671 : * any of B's items.
672 : */
673 2546 : result = true;
674 3000 : iterate_begin(citem, clause, clause_info)
675 : {
676 2968 : bool presult = false;
677 :
678 11413 : iterate_begin(pitem, predicate, pred_info)
679 : {
680 8899 : if (predicate_refuted_by_recurse(citem, pitem,
681 : weak))
682 : {
683 454 : presult = true;
684 454 : break;
685 : }
686 : }
687 2968 : iterate_end(pred_info);
688 2968 : if (!presult)
689 : {
690 2514 : result = false; /* citem refutes nothing */
691 2514 : break;
692 : }
693 : }
694 2546 : iterate_end(clause_info);
695 2546 : return result;
696 :
697 8209 : case CLASS_ATOM:
698 :
699 : /*
700 : * If B is a NOT-type clause, A R=> B if A => B's arg
701 : *
702 : * Same logic as for the AND-clause case above.
703 : */
704 8209 : not_arg = extract_not_arg(predicate);
705 8213 : if (not_arg &&
706 4 : predicate_implied_by_recurse(clause, not_arg,
707 : false))
708 0 : return true;
709 :
710 : /*
711 : * OR-clause R=> atom if each of A's items refutes B
712 : */
713 8209 : result = true;
714 8906 : iterate_begin(citem, clause, clause_info)
715 : {
716 8905 : if (!predicate_refuted_by_recurse(citem, predicate,
717 : weak))
718 : {
719 8208 : result = false;
720 8208 : break;
721 : }
722 : }
723 8209 : iterate_end(clause_info);
724 8209 : return result;
725 : }
726 0 : break;
727 :
728 149234 : case CLASS_ATOM:
729 :
730 : /*
731 : * If A is a strong NOT-clause, A R=> B if B => A's arg
732 : *
733 : * Since A is strong, we may assume A's arg is false (not just
734 : * not-true). If B weakly implies A's arg, then B can be neither
735 : * true nor null, so that strong refutation is proven. If B
736 : * strongly implies A's arg, then B cannot be true, so that weak
737 : * refutation is proven.
738 : */
739 149234 : not_arg = extract_strong_not_arg(clause);
740 150768 : if (not_arg &&
741 1534 : predicate_implied_by_recurse(predicate, not_arg,
742 1534 : !weak))
743 11 : return true;
744 :
745 149223 : switch (pclass)
746 : {
747 15972 : case CLASS_AND:
748 :
749 : /*
750 : * atom R=> AND-clause if A refutes any of B's items
751 : */
752 15972 : result = false;
753 59840 : iterate_begin(pitem, predicate, pred_info)
754 : {
755 44122 : if (predicate_refuted_by_recurse(clause, pitem,
756 : weak))
757 : {
758 254 : result = true;
759 254 : break;
760 : }
761 : }
762 15972 : iterate_end(pred_info);
763 15972 : return result;
764 :
765 9917 : case CLASS_OR:
766 :
767 : /*
768 : * atom R=> OR-clause if A refutes each of B's items
769 : */
770 9917 : result = true;
771 12827 : iterate_begin(pitem, predicate, pred_info)
772 : {
773 12657 : if (!predicate_refuted_by_recurse(clause, pitem,
774 : weak))
775 : {
776 9747 : result = false;
777 9747 : break;
778 : }
779 : }
780 9917 : iterate_end(pred_info);
781 9917 : return result;
782 :
783 123334 : case CLASS_ATOM:
784 :
785 : /*
786 : * If B is a NOT-type clause, A R=> B if A => B's arg
787 : *
788 : * Same logic as for the AND-clause case above.
789 : */
790 123334 : not_arg = extract_not_arg(predicate);
791 124812 : if (not_arg &&
792 1478 : predicate_implied_by_recurse(clause, not_arg,
793 : false))
794 16 : return true;
795 :
796 : /*
797 : * atom R=> atom is the base case
798 : */
799 : return
800 123318 : predicate_refuted_by_simple_clause((Expr *) predicate,
801 : clause,
802 : weak);
803 : }
804 0 : break;
805 : }
806 :
807 : /* can't get here */
808 0 : elog(ERROR, "predicate_classify returned a bogus value");
809 : return false;
810 : }
811 :
812 :
813 : /*
814 : * predicate_classify
815 : * Classify an expression node as AND-type, OR-type, or neither (an atom).
816 : *
817 : * If the expression is classified as AND- or OR-type, then *info is filled
818 : * in with the functions needed to iterate over its components.
819 : *
820 : * This function also implements enforcement of MAX_SAOP_ARRAY_SIZE: if a
821 : * ScalarArrayOpExpr's array has too many elements, we just classify it as an
822 : * atom. (This will result in its being passed as-is to the simple_clause
823 : * functions, many of which will fail to prove anything about it.) Note that we
824 : * cannot just stop after considering MAX_SAOP_ARRAY_SIZE elements; in general
825 : * that would result in wrong proofs, rather than failing to prove anything.
826 : */
827 : static PredClass
828 597932 : predicate_classify(Node *clause, PredIterInfo info)
829 : {
830 : /* Caller should not pass us NULL, nor a RestrictInfo clause */
831 : Assert(clause != NULL);
832 : Assert(!IsA(clause, RestrictInfo));
833 :
834 : /*
835 : * If we see a List, assume it's an implicit-AND list; this is the correct
836 : * semantics for lists of RestrictInfo nodes.
837 : */
838 597932 : if (IsA(clause, List))
839 : {
840 57132 : info->startup_fn = list_startup_fn;
841 57132 : info->next_fn = list_next_fn;
842 57132 : info->cleanup_fn = list_cleanup_fn;
843 57132 : return CLASS_AND;
844 : }
845 :
846 : /* Handle normal AND and OR boolean clauses */
847 540800 : if (is_andclause(clause))
848 : {
849 9811 : info->startup_fn = boolexpr_startup_fn;
850 9811 : info->next_fn = list_next_fn;
851 9811 : info->cleanup_fn = list_cleanup_fn;
852 9811 : return CLASS_AND;
853 : }
854 530989 : if (is_orclause(clause))
855 : {
856 24347 : info->startup_fn = boolexpr_startup_fn;
857 24347 : info->next_fn = list_next_fn;
858 24347 : info->cleanup_fn = list_cleanup_fn;
859 24347 : return CLASS_OR;
860 : }
861 :
862 : /* Handle ScalarArrayOpExpr */
863 506642 : if (IsA(clause, ScalarArrayOpExpr))
864 : {
865 11687 : ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
866 11687 : Node *arraynode = (Node *) lsecond(saop->args);
867 :
868 : /*
869 : * We can break this down into an AND or OR structure, but only if we
870 : * know how to iterate through expressions for the array's elements.
871 : * We can do that if the array operand is a non-null constant or a
872 : * simple ArrayExpr.
873 : */
874 11687 : if (arraynode && IsA(arraynode, Const) &&
875 10112 : !((Const *) arraynode)->constisnull)
876 8 : {
877 : ArrayType *arrayval;
878 : int nelems;
879 :
880 10112 : arrayval = DatumGetArrayTypeP(((Const *) arraynode)->constvalue);
881 10112 : nelems = ArrayGetNItems(ARR_NDIM(arrayval), ARR_DIMS(arrayval));
882 10112 : if (nelems <= MAX_SAOP_ARRAY_SIZE)
883 : {
884 10104 : info->startup_fn = arrayconst_startup_fn;
885 10104 : info->next_fn = arrayconst_next_fn;
886 10104 : info->cleanup_fn = arrayconst_cleanup_fn;
887 10104 : return saop->useOr ? CLASS_OR : CLASS_AND;
888 : }
889 : }
890 1575 : else if (arraynode && IsA(arraynode, ArrayExpr) &&
891 2992 : !((ArrayExpr *) arraynode)->multidims &&
892 1496 : list_length(((ArrayExpr *) arraynode)->elements) <= MAX_SAOP_ARRAY_SIZE)
893 : {
894 1492 : info->startup_fn = arrayexpr_startup_fn;
895 1492 : info->next_fn = arrayexpr_next_fn;
896 1492 : info->cleanup_fn = arrayexpr_cleanup_fn;
897 1492 : return saop->useOr ? CLASS_OR : CLASS_AND;
898 : }
899 : }
900 :
901 : /* None of the above, so it's an atom */
902 495046 : return CLASS_ATOM;
903 : }
904 :
905 : /*
906 : * PredIterInfo routines for iterating over regular Lists. The iteration
907 : * state variable is the next ListCell to visit.
908 : */
909 : static void
910 54795 : list_startup_fn(Node *clause, PredIterInfo info)
911 : {
912 54795 : info->state_list = (List *) clause;
913 54795 : info->state = list_head(info->state_list);
914 54795 : }
915 :
916 : static Node *
917 257363 : list_next_fn(PredIterInfo info)
918 : {
919 257363 : ListCell *l = (ListCell *) info->state;
920 : Node *n;
921 :
922 257363 : if (l == NULL)
923 62407 : return NULL;
924 194956 : n = lfirst(l);
925 194956 : info->state = lnext(info->state_list, l);
926 194956 : return n;
927 : }
928 :
929 : static void
930 87833 : list_cleanup_fn(PredIterInfo info)
931 : {
932 : /* Nothing to clean up */
933 87833 : }
934 :
935 : /*
936 : * BoolExpr needs its own startup function, but can use list_next_fn and
937 : * list_cleanup_fn.
938 : */
939 : static void
940 33038 : boolexpr_startup_fn(Node *clause, PredIterInfo info)
941 : {
942 33038 : info->state_list = ((BoolExpr *) clause)->args;
943 33038 : info->state = list_head(info->state_list);
944 33038 : }
945 :
946 : /*
947 : * PredIterInfo routines for iterating over a ScalarArrayOpExpr with a
948 : * constant array operand.
949 : */
950 : typedef struct
951 : {
952 : OpExpr opexpr;
953 : Const const_expr;
954 : int next_elem;
955 : int num_elems;
956 : Datum *elem_values;
957 : bool *elem_nulls;
958 : } ArrayConstIterState;
959 :
960 : static void
961 9826 : arrayconst_startup_fn(Node *clause, PredIterInfo info)
962 : {
963 9826 : ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
964 : ArrayConstIterState *state;
965 : Const *arrayconst;
966 : ArrayType *arrayval;
967 : int16 elmlen;
968 : bool elmbyval;
969 : char elmalign;
970 :
971 : /* Create working state struct */
972 9826 : state = palloc_object(ArrayConstIterState);
973 9826 : info->state = state;
974 :
975 : /* Deconstruct the array literal */
976 9826 : arrayconst = (Const *) lsecond(saop->args);
977 9826 : arrayval = DatumGetArrayTypeP(arrayconst->constvalue);
978 9826 : get_typlenbyvalalign(ARR_ELEMTYPE(arrayval),
979 : &elmlen, &elmbyval, &elmalign);
980 9826 : deconstruct_array(arrayval,
981 : ARR_ELEMTYPE(arrayval),
982 : elmlen, elmbyval, elmalign,
983 : &state->elem_values, &state->elem_nulls,
984 : &state->num_elems);
985 :
986 : /* Set up a dummy OpExpr to return as the per-item node */
987 9826 : state->opexpr.xpr.type = T_OpExpr;
988 9826 : state->opexpr.opno = saop->opno;
989 9826 : state->opexpr.opfuncid = saop->opfuncid;
990 9826 : state->opexpr.opresulttype = BOOLOID;
991 9826 : state->opexpr.opretset = false;
992 9826 : state->opexpr.opcollid = InvalidOid;
993 9826 : state->opexpr.inputcollid = saop->inputcollid;
994 9826 : state->opexpr.args = list_copy(saop->args);
995 :
996 : /* Set up a dummy Const node to hold the per-element values */
997 9826 : state->const_expr.xpr.type = T_Const;
998 9826 : state->const_expr.consttype = ARR_ELEMTYPE(arrayval);
999 9826 : state->const_expr.consttypmod = -1;
1000 9826 : state->const_expr.constcollid = arrayconst->constcollid;
1001 9826 : state->const_expr.constlen = elmlen;
1002 9826 : state->const_expr.constbyval = elmbyval;
1003 9826 : lsecond(state->opexpr.args) = &state->const_expr;
1004 :
1005 : /* Initialize iteration state */
1006 9826 : state->next_elem = 0;
1007 9826 : }
1008 :
1009 : static Node *
1010 24529 : arrayconst_next_fn(PredIterInfo info)
1011 : {
1012 24529 : ArrayConstIterState *state = (ArrayConstIterState *) info->state;
1013 :
1014 24529 : if (state->next_elem >= state->num_elems)
1015 5212 : return NULL;
1016 19317 : state->const_expr.constvalue = state->elem_values[state->next_elem];
1017 19317 : state->const_expr.constisnull = state->elem_nulls[state->next_elem];
1018 19317 : state->next_elem++;
1019 19317 : return (Node *) &(state->opexpr);
1020 : }
1021 :
1022 : static void
1023 9826 : arrayconst_cleanup_fn(PredIterInfo info)
1024 : {
1025 9826 : ArrayConstIterState *state = (ArrayConstIterState *) info->state;
1026 :
1027 9826 : pfree(state->elem_values);
1028 9826 : pfree(state->elem_nulls);
1029 9826 : list_free(state->opexpr.args);
1030 9826 : pfree(state);
1031 9826 : }
1032 :
1033 : /*
1034 : * PredIterInfo routines for iterating over a ScalarArrayOpExpr with a
1035 : * one-dimensional ArrayExpr array operand.
1036 : */
1037 : typedef struct
1038 : {
1039 : OpExpr opexpr;
1040 : ListCell *next;
1041 : } ArrayExprIterState;
1042 :
1043 : static void
1044 1447 : arrayexpr_startup_fn(Node *clause, PredIterInfo info)
1045 : {
1046 1447 : ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
1047 : ArrayExprIterState *state;
1048 : ArrayExpr *arrayexpr;
1049 :
1050 : /* Create working state struct */
1051 1447 : state = palloc_object(ArrayExprIterState);
1052 1447 : info->state = state;
1053 :
1054 : /* Set up a dummy OpExpr to return as the per-item node */
1055 1447 : state->opexpr.xpr.type = T_OpExpr;
1056 1447 : state->opexpr.opno = saop->opno;
1057 1447 : state->opexpr.opfuncid = saop->opfuncid;
1058 1447 : state->opexpr.opresulttype = BOOLOID;
1059 1447 : state->opexpr.opretset = false;
1060 1447 : state->opexpr.opcollid = InvalidOid;
1061 1447 : state->opexpr.inputcollid = saop->inputcollid;
1062 1447 : state->opexpr.args = list_copy(saop->args);
1063 :
1064 : /* Initialize iteration variable to first member of ArrayExpr */
1065 1447 : arrayexpr = (ArrayExpr *) lsecond(saop->args);
1066 1447 : info->state_list = arrayexpr->elements;
1067 1447 : state->next = list_head(arrayexpr->elements);
1068 1447 : }
1069 :
1070 : static Node *
1071 1457 : arrayexpr_next_fn(PredIterInfo info)
1072 : {
1073 1457 : ArrayExprIterState *state = (ArrayExprIterState *) info->state;
1074 :
1075 1457 : if (state->next == NULL)
1076 5 : return NULL;
1077 1452 : lsecond(state->opexpr.args) = lfirst(state->next);
1078 1452 : state->next = lnext(info->state_list, state->next);
1079 1452 : return (Node *) &(state->opexpr);
1080 : }
1081 :
1082 : static void
1083 1447 : arrayexpr_cleanup_fn(PredIterInfo info)
1084 : {
1085 1447 : ArrayExprIterState *state = (ArrayExprIterState *) info->state;
1086 :
1087 1447 : list_free(state->opexpr.args);
1088 1447 : pfree(state);
1089 1447 : }
1090 :
1091 :
1092 : /*
1093 : * predicate_implied_by_simple_clause
1094 : * Does the predicate implication test for a "simple clause" predicate
1095 : * and a "simple clause" restriction.
1096 : *
1097 : * We return true if able to prove the implication, false if not.
1098 : */
1099 : static bool
1100 87236 : predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
1101 : bool weak)
1102 : {
1103 : /* Allow interrupting long proof attempts */
1104 87236 : CHECK_FOR_INTERRUPTS();
1105 :
1106 : /*
1107 : * A simple and general rule is that a clause implies itself, hence we
1108 : * check if they are equal(); this works for any kind of expression, and
1109 : * for either implication definition. (Actually, there is an implied
1110 : * assumption that the functions in the expression are immutable --- but
1111 : * this was checked for the predicate by the caller.)
1112 : */
1113 87236 : if (equal((Node *) predicate, clause))
1114 1965 : return true;
1115 :
1116 : /* Next we have some clause-type-specific strategies */
1117 85271 : switch (nodeTag(clause))
1118 : {
1119 81434 : case T_OpExpr:
1120 : {
1121 81434 : OpExpr *op = (OpExpr *) clause;
1122 :
1123 : /*----------
1124 : * For boolean x, "x = TRUE" is equivalent to "x", likewise
1125 : * "x = FALSE" is equivalent to "NOT x". These can be worth
1126 : * checking because, while we preferentially simplify boolean
1127 : * comparisons down to "x" and "NOT x", the other form has to
1128 : * be dealt with anyway in the context of index conditions.
1129 : *
1130 : * We could likewise check whether the predicate is boolean
1131 : * equality to a constant; but there are no known use-cases
1132 : * for that at the moment, assuming that the predicate has
1133 : * been through constant-folding.
1134 : *----------
1135 : */
1136 81434 : if (op->opno == BooleanEqualOperator)
1137 : {
1138 : Node *rightop;
1139 :
1140 : Assert(list_length(op->args) == 2);
1141 129 : rightop = lsecond(op->args);
1142 : /* We might never see null Consts here, but better check */
1143 129 : if (rightop && IsA(rightop, Const) &&
1144 129 : !((Const *) rightop)->constisnull)
1145 : {
1146 129 : Node *leftop = linitial(op->args);
1147 :
1148 129 : if (DatumGetBool(((Const *) rightop)->constvalue))
1149 : {
1150 : /* X = true implies X */
1151 2 : if (equal(predicate, leftop))
1152 2 : return true;
1153 : }
1154 : else
1155 : {
1156 : /* X = false implies NOT X */
1157 254 : if (is_notclause(predicate) &&
1158 127 : equal(get_notclausearg(predicate), leftop))
1159 127 : return true;
1160 : }
1161 : }
1162 : }
1163 : }
1164 81305 : break;
1165 3837 : default:
1166 3837 : break;
1167 : }
1168 :
1169 : /* ... and some predicate-type-specific ones */
1170 85142 : switch (nodeTag(predicate))
1171 : {
1172 758 : case T_NullTest:
1173 : {
1174 758 : NullTest *predntest = (NullTest *) predicate;
1175 :
1176 758 : switch (predntest->nulltesttype)
1177 : {
1178 419 : case IS_NOT_NULL:
1179 :
1180 : /*
1181 : * If the predicate is of the form "foo IS NOT NULL",
1182 : * and we are considering strong implication, we can
1183 : * conclude that the predicate is implied if the
1184 : * clause is strict for "foo", i.e., it must yield
1185 : * false or NULL when "foo" is NULL. In that case
1186 : * truth of the clause ensures that "foo" isn't NULL.
1187 : * (Again, this is a safe conclusion because "foo"
1188 : * must be immutable.) This doesn't work for weak
1189 : * implication, though. Also, "row IS NOT NULL" does
1190 : * not act in the simple way we have in mind.
1191 : */
1192 419 : if (!weak &&
1193 274 : !predntest->argisrow &&
1194 137 : clause_is_strict_for(clause,
1195 137 : (Node *) predntest->arg,
1196 : true))
1197 11 : return true;
1198 408 : break;
1199 339 : case IS_NULL:
1200 339 : break;
1201 : }
1202 : }
1203 747 : break;
1204 84384 : default:
1205 84384 : break;
1206 : }
1207 :
1208 : /*
1209 : * Finally, if both clauses are binary operator expressions, we may be
1210 : * able to prove something using the system's knowledge about operators;
1211 : * those proof rules are encapsulated in operator_predicate_proof().
1212 : */
1213 85131 : return operator_predicate_proof(predicate, clause, false, weak);
1214 : }
1215 :
1216 : /*
1217 : * predicate_refuted_by_simple_clause
1218 : * Does the predicate refutation test for a "simple clause" predicate
1219 : * and a "simple clause" restriction.
1220 : *
1221 : * We return true if able to prove the refutation, false if not.
1222 : *
1223 : * The main motivation for covering IS [NOT] NULL cases is to support using
1224 : * IS NULL/IS NOT NULL as partition-defining constraints.
1225 : */
1226 : static bool
1227 123318 : predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
1228 : bool weak)
1229 : {
1230 : /* Allow interrupting long proof attempts */
1231 123318 : CHECK_FOR_INTERRUPTS();
1232 :
1233 : /*
1234 : * A simple clause can't refute itself, so unlike the implication case,
1235 : * checking for equal() clauses isn't helpful.
1236 : *
1237 : * But relation_excluded_by_constraints() checks for self-contradictions
1238 : * in a list of clauses, so that we may get here with predicate and clause
1239 : * being actually pointer-equal, and that is worth eliminating quickly.
1240 : */
1241 123318 : if ((Node *) predicate == clause)
1242 38565 : return false;
1243 :
1244 : /* Next we have some clause-type-specific strategies */
1245 84753 : switch (nodeTag(clause))
1246 : {
1247 6502 : case T_NullTest:
1248 : {
1249 6502 : NullTest *clausentest = (NullTest *) clause;
1250 :
1251 : /* row IS NULL does not act in the simple way we have in mind */
1252 6502 : if (clausentest->argisrow)
1253 0 : return false;
1254 :
1255 6502 : switch (clausentest->nulltesttype)
1256 : {
1257 3530 : case IS_NULL:
1258 : {
1259 3530 : switch (nodeTag(predicate))
1260 : {
1261 1055 : case T_NullTest:
1262 : {
1263 1055 : NullTest *predntest = (NullTest *) predicate;
1264 :
1265 : /*
1266 : * row IS NULL does not act in the
1267 : * simple way we have in mind
1268 : */
1269 1055 : if (predntest->argisrow)
1270 0 : return false;
1271 :
1272 : /*
1273 : * foo IS NULL refutes foo IS NOT
1274 : * NULL, at least in the non-row case,
1275 : * for both strong and weak refutation
1276 : */
1277 1090 : if (predntest->nulltesttype == IS_NOT_NULL &&
1278 35 : equal(predntest->arg, clausentest->arg))
1279 12 : return true;
1280 : }
1281 1043 : break;
1282 2475 : default:
1283 2475 : break;
1284 : }
1285 :
1286 : /*
1287 : * foo IS NULL weakly refutes any predicate that
1288 : * is strict for foo, since then the predicate
1289 : * must yield false or NULL (and since foo appears
1290 : * in the predicate, it's known immutable).
1291 : */
1292 5643 : if (weak &&
1293 2125 : clause_is_strict_for((Node *) predicate,
1294 2125 : (Node *) clausentest->arg,
1295 : true))
1296 24 : return true;
1297 :
1298 3494 : return false; /* we can't succeed below... */
1299 : }
1300 : break;
1301 2972 : case IS_NOT_NULL:
1302 2972 : break;
1303 : }
1304 : }
1305 2972 : break;
1306 78251 : default:
1307 78251 : break;
1308 : }
1309 :
1310 : /* ... and some predicate-type-specific ones */
1311 81223 : switch (nodeTag(predicate))
1312 : {
1313 22214 : case T_NullTest:
1314 : {
1315 22214 : NullTest *predntest = (NullTest *) predicate;
1316 :
1317 : /* row IS NULL does not act in the simple way we have in mind */
1318 22214 : if (predntest->argisrow)
1319 0 : return false;
1320 :
1321 22214 : switch (predntest->nulltesttype)
1322 : {
1323 2500 : case IS_NULL:
1324 : {
1325 2500 : switch (nodeTag(clause))
1326 : {
1327 12 : case T_NullTest:
1328 : {
1329 12 : NullTest *clausentest = (NullTest *) clause;
1330 :
1331 : /*
1332 : * row IS NULL does not act in the
1333 : * simple way we have in mind
1334 : */
1335 12 : if (clausentest->argisrow)
1336 0 : return false;
1337 :
1338 : /*
1339 : * foo IS NOT NULL refutes foo IS NULL
1340 : * for both strong and weak refutation
1341 : */
1342 24 : if (clausentest->nulltesttype == IS_NOT_NULL &&
1343 12 : equal(clausentest->arg, predntest->arg))
1344 12 : return true;
1345 : }
1346 0 : break;
1347 2488 : default:
1348 2488 : break;
1349 : }
1350 :
1351 : /*
1352 : * When the predicate is of the form "foo IS
1353 : * NULL", we can conclude that the predicate is
1354 : * refuted if the clause is strict for "foo" (see
1355 : * notes for implication case). That works for
1356 : * either strong or weak refutation.
1357 : */
1358 2488 : if (clause_is_strict_for(clause,
1359 2488 : (Node *) predntest->arg,
1360 : true))
1361 1362 : return true;
1362 : }
1363 1126 : break;
1364 19714 : case IS_NOT_NULL:
1365 19714 : break;
1366 : }
1367 :
1368 20840 : return false; /* we can't succeed below... */
1369 : }
1370 : break;
1371 59009 : default:
1372 59009 : break;
1373 : }
1374 :
1375 : /*
1376 : * Finally, if both clauses are binary operator expressions, we may be
1377 : * able to prove something using the system's knowledge about operators.
1378 : */
1379 59009 : return operator_predicate_proof(predicate, clause, true, weak);
1380 : }
1381 :
1382 :
1383 : /*
1384 : * If clause asserts the non-truth of a subclause, return that subclause;
1385 : * otherwise return NULL.
1386 : */
1387 : static Node *
1388 150878 : extract_not_arg(Node *clause)
1389 : {
1390 150878 : if (clause == NULL)
1391 0 : return NULL;
1392 150878 : if (IsA(clause, BoolExpr))
1393 : {
1394 1058 : BoolExpr *bexpr = (BoolExpr *) clause;
1395 :
1396 1058 : if (bexpr->boolop == NOT_EXPR)
1397 1058 : return (Node *) linitial(bexpr->args);
1398 : }
1399 149820 : else if (IsA(clause, BooleanTest))
1400 : {
1401 1351 : BooleanTest *btest = (BooleanTest *) clause;
1402 :
1403 1351 : if (btest->booltesttype == IS_NOT_TRUE ||
1404 714 : btest->booltesttype == IS_FALSE ||
1405 712 : btest->booltesttype == IS_UNKNOWN)
1406 681 : return (Node *) btest->arg;
1407 : }
1408 149139 : return NULL;
1409 : }
1410 :
1411 : /*
1412 : * If clause asserts the falsity of a subclause, return that subclause;
1413 : * otherwise return NULL.
1414 : */
1415 : static Node *
1416 149234 : extract_strong_not_arg(Node *clause)
1417 : {
1418 149234 : if (clause == NULL)
1419 0 : return NULL;
1420 149234 : if (IsA(clause, BoolExpr))
1421 : {
1422 1530 : BoolExpr *bexpr = (BoolExpr *) clause;
1423 :
1424 1530 : if (bexpr->boolop == NOT_EXPR)
1425 1530 : return (Node *) linitial(bexpr->args);
1426 : }
1427 147704 : else if (IsA(clause, BooleanTest))
1428 : {
1429 1288 : BooleanTest *btest = (BooleanTest *) clause;
1430 :
1431 1288 : if (btest->booltesttype == IS_FALSE)
1432 4 : return (Node *) btest->arg;
1433 : }
1434 147700 : return NULL;
1435 : }
1436 :
1437 :
1438 : /*
1439 : * Can we prove that "clause" returns NULL (or FALSE) if "subexpr" is
1440 : * assumed to yield NULL?
1441 : *
1442 : * In most places in the planner, "strictness" refers to a guarantee that
1443 : * an expression yields NULL output for a NULL input, and that's mostly what
1444 : * we're looking for here. However, at top level where the clause is known
1445 : * to yield boolean, it may be sufficient to prove that it cannot return TRUE
1446 : * when "subexpr" is NULL. The caller should pass allow_false = true when
1447 : * this weaker property is acceptable. (When this function recurses
1448 : * internally, we pass down allow_false = false since we need to prove actual
1449 : * nullness of the subexpression.)
1450 : *
1451 : * We assume that the caller checked that least one of the input expressions
1452 : * is immutable. All of the proof rules here involve matching "subexpr" to
1453 : * some portion of "clause", so that this allows assuming that "subexpr" is
1454 : * immutable without a separate check.
1455 : *
1456 : * The base case is that clause and subexpr are equal().
1457 : *
1458 : * We can also report success if the subexpr appears as a subexpression
1459 : * of "clause" in a place where it'd force nullness of the overall result.
1460 : */
1461 : static bool
1462 10882 : clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
1463 : {
1464 : ListCell *lc;
1465 :
1466 : /* safety checks */
1467 10882 : if (clause == NULL || subexpr == NULL)
1468 0 : return false;
1469 :
1470 : /*
1471 : * Look through any RelabelType nodes, so that we can match, say,
1472 : * varcharcol with lower(varcharcol::text). (In general we could recurse
1473 : * through any nullness-preserving, immutable operation.) We should not
1474 : * see stacked RelabelTypes here.
1475 : */
1476 10882 : if (IsA(clause, RelabelType))
1477 21 : clause = (Node *) ((RelabelType *) clause)->arg;
1478 10882 : if (IsA(subexpr, RelabelType))
1479 0 : subexpr = (Node *) ((RelabelType *) subexpr)->arg;
1480 :
1481 : /* Base case */
1482 10882 : if (equal(clause, subexpr))
1483 1407 : return true;
1484 :
1485 : /*
1486 : * If we have a strict operator or function, a NULL result is guaranteed
1487 : * if any input is forced NULL by subexpr. This is OK even if the op or
1488 : * func isn't immutable, since it won't even be called on NULL input.
1489 : */
1490 13196 : if (is_opclause(clause) &&
1491 3721 : op_strict(((OpExpr *) clause)->opno))
1492 : {
1493 8415 : foreach(lc, ((OpExpr *) clause)->args)
1494 : {
1495 6068 : if (clause_is_strict_for((Node *) lfirst(lc), subexpr, false))
1496 1374 : return true;
1497 : }
1498 2347 : return false;
1499 : }
1500 5782 : if (is_funcclause(clause) &&
1501 28 : func_strict(((FuncExpr *) clause)->funcid))
1502 : {
1503 44 : foreach(lc, ((FuncExpr *) clause)->args)
1504 : {
1505 31 : if (clause_is_strict_for((Node *) lfirst(lc), subexpr, false))
1506 15 : return true;
1507 : }
1508 13 : return false;
1509 : }
1510 :
1511 : /*
1512 : * CoerceViaIO is strict (whether or not the I/O functions it calls are).
1513 : * Likewise, ArrayCoerceExpr is strict for its array argument (regardless
1514 : * of what the per-element expression is), ConvertRowtypeExpr is strict at
1515 : * the row level, and CoerceToDomain is strict too. These are worth
1516 : * checking mainly because it saves us having to explain to users why some
1517 : * type coercions are known strict and others aren't.
1518 : */
1519 5726 : if (IsA(clause, CoerceViaIO))
1520 0 : return clause_is_strict_for((Node *) ((CoerceViaIO *) clause)->arg,
1521 : subexpr, false);
1522 5726 : if (IsA(clause, ArrayCoerceExpr))
1523 0 : return clause_is_strict_for((Node *) ((ArrayCoerceExpr *) clause)->arg,
1524 : subexpr, false);
1525 5726 : if (IsA(clause, ConvertRowtypeExpr))
1526 0 : return clause_is_strict_for((Node *) ((ConvertRowtypeExpr *) clause)->arg,
1527 : subexpr, false);
1528 5726 : if (IsA(clause, CoerceToDomain))
1529 0 : return clause_is_strict_for((Node *) ((CoerceToDomain *) clause)->arg,
1530 : subexpr, false);
1531 :
1532 : /*
1533 : * ScalarArrayOpExpr is a special case. Note that we'd only reach here
1534 : * with a ScalarArrayOpExpr clause if we failed to deconstruct it into an
1535 : * AND or OR tree, as for example if it has too many array elements.
1536 : */
1537 5726 : if (IsA(clause, ScalarArrayOpExpr))
1538 : {
1539 22 : ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
1540 22 : Node *scalarnode = (Node *) linitial(saop->args);
1541 22 : Node *arraynode = (Node *) lsecond(saop->args);
1542 :
1543 : /*
1544 : * If we can prove the scalar input to be null, and the operator is
1545 : * strict, then the SAOP result has to be null --- unless the array is
1546 : * empty. For an empty array, we'd get either false (for ANY) or true
1547 : * (for ALL). So if allow_false = true then the proof succeeds anyway
1548 : * for the ANY case; otherwise we can only make the proof if we can
1549 : * prove the array non-empty.
1550 : */
1551 43 : if (clause_is_strict_for(scalarnode, subexpr, false) &&
1552 21 : op_strict(saop->opno))
1553 : {
1554 21 : int nelems = 0;
1555 :
1556 21 : if (allow_false && saop->useOr)
1557 7 : return true; /* can succeed even if array is empty */
1558 :
1559 14 : if (arraynode && IsA(arraynode, Const))
1560 3 : {
1561 3 : Const *arrayconst = (Const *) arraynode;
1562 : ArrayType *arrval;
1563 :
1564 : /*
1565 : * If array is constant NULL then we can succeed, as in the
1566 : * case below.
1567 : */
1568 3 : if (arrayconst->constisnull)
1569 0 : return true;
1570 :
1571 : /* Otherwise, we can compute the number of elements. */
1572 3 : arrval = DatumGetArrayTypeP(arrayconst->constvalue);
1573 3 : nelems = ArrayGetNItems(ARR_NDIM(arrval), ARR_DIMS(arrval));
1574 : }
1575 11 : else if (arraynode && IsA(arraynode, ArrayExpr) &&
1576 1 : !((ArrayExpr *) arraynode)->multidims)
1577 : {
1578 : /*
1579 : * We can also reliably count the number of array elements if
1580 : * the input is a non-multidim ARRAY[] expression.
1581 : */
1582 1 : nelems = list_length(((ArrayExpr *) arraynode)->elements);
1583 : }
1584 :
1585 : /* Proof succeeds if array is definitely non-empty */
1586 14 : if (nelems > 0)
1587 4 : return true;
1588 : }
1589 :
1590 : /*
1591 : * If we can prove the array input to be null, the proof succeeds in
1592 : * all cases, since ScalarArrayOpExpr will always return NULL for a
1593 : * NULL array. Otherwise, we're done here.
1594 : */
1595 11 : return clause_is_strict_for(arraynode, subexpr, false);
1596 : }
1597 :
1598 : /*
1599 : * When recursing into an expression, we might find a NULL constant.
1600 : * That's certainly NULL, whether it matches subexpr or not.
1601 : */
1602 5704 : if (IsA(clause, Const))
1603 2215 : return ((Const *) clause)->constisnull;
1604 :
1605 3489 : return false;
1606 : }
1607 :
1608 :
1609 : /*
1610 : * Define "operator implication tables" for index operators ("cmptypes"),
1611 : * and similar tables for refutation.
1612 : *
1613 : * The row compare numbers defined by indexes (see access/cmptype.h) are:
1614 : * 1 < 2 <= 3 = 4 >= 5 > 6 <>
1615 : * and in addition we use 6 to represent <>. <> is not a btree-indexable
1616 : * operator, but we assume here that if an equality operator of a btree
1617 : * opfamily has a negator operator, the negator behaves as <> for the opfamily.
1618 : * (This convention is also known to get_op_index_interpretation().)
1619 : *
1620 : * RC_implies_table[] and RC_refutes_table[] are used for cases where we have
1621 : * two identical subexpressions and we want to know whether one operator
1622 : * expression implies or refutes the other. That is, if the "clause" is
1623 : * EXPR1 clause_op EXPR2 and the "predicate" is EXPR1 pred_op EXPR2 for the
1624 : * same two (immutable) subexpressions:
1625 : * RC_implies_table[clause_op-1][pred_op-1]
1626 : * is true if the clause implies the predicate
1627 : * RC_refutes_table[clause_op-1][pred_op-1]
1628 : * is true if the clause refutes the predicate
1629 : * where clause_op and pred_op are cmptype numbers (from 1 to 6) in the
1630 : * same opfamily. For example, "x < y" implies "x <= y" and refutes
1631 : * "x > y".
1632 : *
1633 : * RC_implic_table[] and RC_refute_table[] are used where we have two
1634 : * constants that we need to compare. The interpretation of:
1635 : *
1636 : * test_op = RC_implic_table[clause_op-1][pred_op-1]
1637 : *
1638 : * where test_op, clause_op and pred_op are cmptypes (from 1 to 6)
1639 : * of index operators, is as follows:
1640 : *
1641 : * If you know, for some EXPR, that "EXPR clause_op CONST1" is true, and you
1642 : * want to determine whether "EXPR pred_op CONST2" must also be true, then
1643 : * you can use "CONST2 test_op CONST1" as a test. If this test returns true,
1644 : * then the predicate expression must be true; if the test returns false,
1645 : * then the predicate expression may be false.
1646 : *
1647 : * For example, if clause is "Quantity > 10" and pred is "Quantity > 5"
1648 : * then we test "5 <= 10" which evals to true, so clause implies pred.
1649 : *
1650 : * Similarly, the interpretation of a RC_refute_table entry is:
1651 : *
1652 : * If you know, for some EXPR, that "EXPR clause_op CONST1" is true, and you
1653 : * want to determine whether "EXPR pred_op CONST2" must be false, then
1654 : * you can use "CONST2 test_op CONST1" as a test. If this test returns true,
1655 : * then the predicate expression must be false; if the test returns false,
1656 : * then the predicate expression may be true.
1657 : *
1658 : * For example, if clause is "Quantity > 10" and pred is "Quantity < 5"
1659 : * then we test "5 <= 10" which evals to true, so clause refutes pred.
1660 : *
1661 : * An entry where test_op == 0 means the implication cannot be determined.
1662 : */
1663 :
1664 : #define RCLT COMPARE_LT
1665 : #define RCLE COMPARE_LE
1666 : #define RCEQ COMPARE_EQ
1667 : #define RCGE COMPARE_GE
1668 : #define RCGT COMPARE_GT
1669 : #define RCNE COMPARE_NE
1670 :
1671 : /* We use "none" for 0/false to make the tables align nicely */
1672 : #define none 0
1673 :
1674 : static const bool RC_implies_table[6][6] = {
1675 : /*
1676 : * The predicate operator:
1677 : * LT LE EQ GE GT NE
1678 : */
1679 : {true, true, none, none, none, true}, /* LT */
1680 : {none, true, none, none, none, none}, /* LE */
1681 : {none, true, true, true, none, none}, /* EQ */
1682 : {none, none, none, true, none, none}, /* GE */
1683 : {none, none, none, true, true, true}, /* GT */
1684 : {none, none, none, none, none, true} /* NE */
1685 : };
1686 :
1687 : static const bool RC_refutes_table[6][6] = {
1688 : /*
1689 : * The predicate operator:
1690 : * LT LE EQ GE GT NE
1691 : */
1692 : {none, none, true, true, true, none}, /* LT */
1693 : {none, none, none, none, true, none}, /* LE */
1694 : {true, none, none, none, true, true}, /* EQ */
1695 : {true, none, none, none, none, none}, /* GE */
1696 : {true, true, true, none, none, none}, /* GT */
1697 : {none, none, true, none, none, none} /* NE */
1698 : };
1699 :
1700 : static const CompareType RC_implic_table[6][6] = {
1701 : /*
1702 : * The predicate operator:
1703 : * LT LE EQ GE GT NE
1704 : */
1705 : {RCGE, RCGE, none, none, none, RCGE}, /* LT */
1706 : {RCGT, RCGE, none, none, none, RCGT}, /* LE */
1707 : {RCGT, RCGE, RCEQ, RCLE, RCLT, RCNE}, /* EQ */
1708 : {none, none, none, RCLE, RCLT, RCLT}, /* GE */
1709 : {none, none, none, RCLE, RCLE, RCLE}, /* GT */
1710 : {none, none, none, none, none, RCEQ} /* NE */
1711 : };
1712 :
1713 : static const CompareType RC_refute_table[6][6] = {
1714 : /*
1715 : * The predicate operator:
1716 : * LT LE EQ GE GT NE
1717 : */
1718 : {none, none, RCGE, RCGE, RCGE, none}, /* LT */
1719 : {none, none, RCGT, RCGT, RCGE, none}, /* LE */
1720 : {RCLE, RCLT, RCNE, RCGT, RCGE, RCEQ}, /* EQ */
1721 : {RCLE, RCLT, RCLT, none, none, none}, /* GE */
1722 : {RCLE, RCLE, RCLE, none, none, none}, /* GT */
1723 : {none, none, RCEQ, none, none, none} /* NE */
1724 : };
1725 :
1726 :
1727 : /*
1728 : * operator_predicate_proof
1729 : * Does the predicate implication or refutation test for a "simple clause"
1730 : * predicate and a "simple clause" restriction, when both are operator
1731 : * clauses using related operators and identical input expressions.
1732 : *
1733 : * When refute_it == false, we want to prove the predicate true;
1734 : * when refute_it == true, we want to prove the predicate false.
1735 : * (There is enough common code to justify handling these two cases
1736 : * in one routine.) We return true if able to make the proof, false
1737 : * if not able to prove it.
1738 : *
1739 : * We mostly need not distinguish strong vs. weak implication/refutation here.
1740 : * This depends on the assumption that a pair of related operators (i.e.,
1741 : * commutators, negators, or btree opfamily siblings) will not return one NULL
1742 : * and one non-NULL result for the same inputs. Then, for the proof types
1743 : * where we start with an assumption of truth of the clause, the predicate
1744 : * operator could not return NULL either, so it doesn't matter whether we are
1745 : * trying to make a strong or weak proof. For weak implication, it could be
1746 : * that the clause operator returned NULL, but then the predicate operator
1747 : * would as well, so that the weak implication still holds. This argument
1748 : * doesn't apply in the case where we are considering two different constant
1749 : * values, since then the operators aren't being given identical inputs. But
1750 : * we only support that for btree operators, for which we can assume that all
1751 : * non-null inputs result in non-null outputs, so that it doesn't matter which
1752 : * two non-null constants we consider. If either constant is NULL, we have
1753 : * to think harder, but sometimes the proof still works, as explained below.
1754 : *
1755 : * We can make proofs involving several expression forms (here "foo" and "bar"
1756 : * represent subexpressions that are identical according to equal()):
1757 : * "foo op1 bar" refutes "foo op2 bar" if op1 is op2's negator
1758 : * "foo op1 bar" implies "bar op2 foo" if op1 is op2's commutator
1759 : * "foo op1 bar" refutes "bar op2 foo" if op1 is negator of op2's commutator
1760 : * "foo op1 bar" can imply/refute "foo op2 bar" based on btree semantics
1761 : * "foo op1 bar" can imply/refute "bar op2 foo" based on btree semantics
1762 : * "foo op1 const1" can imply/refute "foo op2 const2" based on btree semantics
1763 : *
1764 : * For the last three cases, op1 and op2 have to be members of the same btree
1765 : * operator family. When both subexpressions are identical, the idea is that,
1766 : * for instance, x < y implies x <= y, independently of exactly what x and y
1767 : * are. If we have two different constants compared to the same expression
1768 : * foo, we have to execute a comparison between the two constant values
1769 : * in order to determine the result; for instance, foo < c1 implies foo < c2
1770 : * if c1 <= c2. We assume it's safe to compare the constants at plan time
1771 : * if the comparison operator is immutable.
1772 : *
1773 : * Note: all the operators and subexpressions have to be immutable for the
1774 : * proof to be safe. We assume the predicate expression is entirely immutable,
1775 : * so no explicit check on the subexpressions is needed here, but in some
1776 : * cases we need an extra check of operator immutability. In particular,
1777 : * btree opfamilies can contain cross-type operators that are merely stable,
1778 : * and we dare not make deductions with those.
1779 : */
1780 : static bool
1781 144140 : operator_predicate_proof(Expr *predicate, Node *clause,
1782 : bool refute_it, bool weak)
1783 : {
1784 : OpExpr *pred_opexpr,
1785 : *clause_opexpr;
1786 : Oid pred_collation,
1787 : clause_collation;
1788 : Oid pred_op,
1789 : clause_op,
1790 : test_op;
1791 : Node *pred_leftop,
1792 : *pred_rightop,
1793 : *clause_leftop,
1794 : *clause_rightop;
1795 : Const *pred_const,
1796 : *clause_const;
1797 : Expr *test_expr;
1798 : ExprState *test_exprstate;
1799 : Datum test_result;
1800 : bool isNull;
1801 : EState *estate;
1802 : MemoryContext oldcontext;
1803 :
1804 : /*
1805 : * Both expressions must be binary opclauses, else we can't do anything.
1806 : *
1807 : * Note: in future we might extend this logic to other operator-based
1808 : * constructs such as DistinctExpr. But the planner isn't very smart
1809 : * about DistinctExpr in general, and this probably isn't the first place
1810 : * to fix if you want to improve that.
1811 : */
1812 144140 : if (!is_opclause(predicate))
1813 26583 : return false;
1814 117557 : pred_opexpr = (OpExpr *) predicate;
1815 117557 : if (list_length(pred_opexpr->args) != 2)
1816 0 : return false;
1817 117557 : if (!is_opclause(clause))
1818 5523 : return false;
1819 112034 : clause_opexpr = (OpExpr *) clause;
1820 112034 : if (list_length(clause_opexpr->args) != 2)
1821 0 : return false;
1822 :
1823 : /*
1824 : * If they're marked with different collations then we can't do anything.
1825 : * This is a cheap test so let's get it out of the way early.
1826 : */
1827 112034 : pred_collation = pred_opexpr->inputcollid;
1828 112034 : clause_collation = clause_opexpr->inputcollid;
1829 112034 : if (pred_collation != clause_collation)
1830 13386 : return false;
1831 :
1832 : /* Grab the operator OIDs now too. We may commute these below. */
1833 98648 : pred_op = pred_opexpr->opno;
1834 98648 : clause_op = clause_opexpr->opno;
1835 :
1836 : /*
1837 : * We have to match up at least one pair of input expressions.
1838 : */
1839 98648 : pred_leftop = (Node *) linitial(pred_opexpr->args);
1840 98648 : pred_rightop = (Node *) lsecond(pred_opexpr->args);
1841 98648 : clause_leftop = (Node *) linitial(clause_opexpr->args);
1842 98648 : clause_rightop = (Node *) lsecond(clause_opexpr->args);
1843 :
1844 98648 : if (equal(pred_leftop, clause_leftop))
1845 : {
1846 35077 : if (equal(pred_rightop, clause_rightop))
1847 : {
1848 : /* We have x op1 y and x op2 y */
1849 3953 : return operator_same_subexprs_proof(pred_op, clause_op, refute_it);
1850 : }
1851 : else
1852 : {
1853 : /* Fail unless rightops are both Consts */
1854 31124 : if (pred_rightop == NULL || !IsA(pred_rightop, Const))
1855 1344 : return false;
1856 29780 : pred_const = (Const *) pred_rightop;
1857 29780 : if (clause_rightop == NULL || !IsA(clause_rightop, Const))
1858 25 : return false;
1859 29755 : clause_const = (Const *) clause_rightop;
1860 : }
1861 : }
1862 63571 : else if (equal(pred_rightop, clause_rightop))
1863 : {
1864 : /* Fail unless leftops are both Consts */
1865 2838 : if (pred_leftop == NULL || !IsA(pred_leftop, Const))
1866 2834 : return false;
1867 4 : pred_const = (Const *) pred_leftop;
1868 4 : if (clause_leftop == NULL || !IsA(clause_leftop, Const))
1869 0 : return false;
1870 4 : clause_const = (Const *) clause_leftop;
1871 : /* Commute both operators so we can assume Consts are on the right */
1872 4 : pred_op = get_commutator(pred_op);
1873 4 : if (!OidIsValid(pred_op))
1874 0 : return false;
1875 4 : clause_op = get_commutator(clause_op);
1876 4 : if (!OidIsValid(clause_op))
1877 0 : return false;
1878 : }
1879 60733 : else if (equal(pred_leftop, clause_rightop))
1880 : {
1881 657 : if (equal(pred_rightop, clause_leftop))
1882 : {
1883 : /* We have x op1 y and y op2 x */
1884 : /* Commute pred_op that we can treat this like a straight match */
1885 568 : pred_op = get_commutator(pred_op);
1886 568 : if (!OidIsValid(pred_op))
1887 0 : return false;
1888 568 : return operator_same_subexprs_proof(pred_op, clause_op, refute_it);
1889 : }
1890 : else
1891 : {
1892 : /* Fail unless pred_rightop/clause_leftop are both Consts */
1893 89 : if (pred_rightop == NULL || !IsA(pred_rightop, Const))
1894 80 : return false;
1895 9 : pred_const = (Const *) pred_rightop;
1896 9 : if (clause_leftop == NULL || !IsA(clause_leftop, Const))
1897 5 : return false;
1898 4 : clause_const = (Const *) clause_leftop;
1899 : /* Commute clause_op so we can assume Consts are on the right */
1900 4 : clause_op = get_commutator(clause_op);
1901 4 : if (!OidIsValid(clause_op))
1902 0 : return false;
1903 : }
1904 : }
1905 60076 : else if (equal(pred_rightop, clause_leftop))
1906 : {
1907 : /* Fail unless pred_leftop/clause_rightop are both Consts */
1908 115 : if (pred_leftop == NULL || !IsA(pred_leftop, Const))
1909 87 : return false;
1910 28 : pred_const = (Const *) pred_leftop;
1911 28 : if (clause_rightop == NULL || !IsA(clause_rightop, Const))
1912 0 : return false;
1913 28 : clause_const = (Const *) clause_rightop;
1914 : /* Commute pred_op so we can assume Consts are on the right */
1915 28 : pred_op = get_commutator(pred_op);
1916 28 : if (!OidIsValid(pred_op))
1917 0 : return false;
1918 : }
1919 : else
1920 : {
1921 : /* Failed to match up any of the subexpressions, so we lose */
1922 59961 : return false;
1923 : }
1924 :
1925 : /*
1926 : * We have two identical subexpressions, and two other subexpressions that
1927 : * are not identical but are both Consts; and we have commuted the
1928 : * operators if necessary so that the Consts are on the right. We'll need
1929 : * to compare the Consts' values. If either is NULL, we can't do that, so
1930 : * usually the proof fails ... but in some cases we can claim success.
1931 : */
1932 29791 : if (clause_const->constisnull)
1933 : {
1934 : /* If clause_op isn't strict, we can't prove anything */
1935 2 : if (!op_strict(clause_op))
1936 0 : return false;
1937 :
1938 : /*
1939 : * At this point we know that the clause returns NULL. For proof
1940 : * types that assume truth of the clause, this means the proof is
1941 : * vacuously true (a/k/a "false implies anything"). That's all proof
1942 : * types except weak implication.
1943 : */
1944 2 : if (!(weak && !refute_it))
1945 1 : return true;
1946 :
1947 : /*
1948 : * For weak implication, it's still possible for the proof to succeed,
1949 : * if the predicate can also be proven NULL. In that case we've got
1950 : * NULL => NULL which is valid for this proof type.
1951 : */
1952 1 : if (pred_const->constisnull && op_strict(pred_op))
1953 0 : return true;
1954 : /* Else the proof fails */
1955 1 : return false;
1956 : }
1957 29789 : if (pred_const->constisnull)
1958 : {
1959 : /*
1960 : * If the pred_op is strict, we know the predicate yields NULL, which
1961 : * means the proof succeeds for either weak implication or weak
1962 : * refutation.
1963 : */
1964 10 : if (weak && op_strict(pred_op))
1965 6 : return true;
1966 : /* Else the proof fails */
1967 4 : return false;
1968 : }
1969 :
1970 : /*
1971 : * Lookup the constant-comparison operator using the system catalogs and
1972 : * the operator implication tables.
1973 : */
1974 29779 : test_op = get_btree_test_op(pred_op, clause_op, refute_it);
1975 :
1976 29779 : if (!OidIsValid(test_op))
1977 : {
1978 : /* couldn't find a suitable comparison operator */
1979 13244 : return false;
1980 : }
1981 :
1982 : /*
1983 : * Evaluate the test. For this we need an EState.
1984 : */
1985 16535 : estate = CreateExecutorState();
1986 :
1987 : /* We can use the estate's working context to avoid memory leaks. */
1988 16535 : oldcontext = MemoryContextSwitchTo(estate->es_query_cxt);
1989 :
1990 : /* Build expression tree */
1991 16535 : test_expr = make_opclause(test_op,
1992 : BOOLOID,
1993 : false,
1994 : (Expr *) pred_const,
1995 : (Expr *) clause_const,
1996 : InvalidOid,
1997 : pred_collation);
1998 :
1999 : /* Fill in opfuncids */
2000 16535 : fix_opfuncids((Node *) test_expr);
2001 :
2002 : /* Prepare it for execution */
2003 16535 : test_exprstate = ExecInitExpr(test_expr, NULL);
2004 :
2005 : /* And execute it. */
2006 16535 : test_result = ExecEvalExprSwitchContext(test_exprstate,
2007 16535 : GetPerTupleExprContext(estate),
2008 : &isNull);
2009 :
2010 : /* Get back to outer memory context */
2011 16535 : MemoryContextSwitchTo(oldcontext);
2012 :
2013 : /* Release all the junk we just created */
2014 16535 : FreeExecutorState(estate);
2015 :
2016 16535 : if (isNull)
2017 : {
2018 : /* Treat a null result as non-proof ... but it's a tad fishy ... */
2019 0 : elog(DEBUG2, "null predicate test result");
2020 0 : return false;
2021 : }
2022 16535 : return DatumGetBool(test_result);
2023 : }
2024 :
2025 :
2026 : /*
2027 : * operator_same_subexprs_proof
2028 : * Assuming that EXPR1 clause_op EXPR2 is true, try to prove or refute
2029 : * EXPR1 pred_op EXPR2.
2030 : *
2031 : * Return true if able to make the proof, false if not able to prove it.
2032 : */
2033 : static bool
2034 4521 : operator_same_subexprs_proof(Oid pred_op, Oid clause_op, bool refute_it)
2035 : {
2036 : /*
2037 : * A simple and general rule is that the predicate is proven if clause_op
2038 : * and pred_op are the same, or refuted if they are each other's negators.
2039 : * We need not check immutability since the pred_op is already known
2040 : * immutable. (Actually, by this point we may have the commutator of a
2041 : * known-immutable pred_op, but that should certainly be immutable too.
2042 : * Likewise we don't worry whether the pred_op's negator is immutable.)
2043 : *
2044 : * Note: the "same" case won't get here if we actually had EXPR1 clause_op
2045 : * EXPR2 and EXPR1 pred_op EXPR2, because the overall-expression-equality
2046 : * test in predicate_implied_by_simple_clause would have caught it. But
2047 : * we can see the same operator after having commuted the pred_op.
2048 : */
2049 4521 : if (refute_it)
2050 : {
2051 3853 : if (get_negator(pred_op) == clause_op)
2052 1533 : return true;
2053 : }
2054 : else
2055 : {
2056 668 : if (pred_op == clause_op)
2057 542 : return true;
2058 : }
2059 :
2060 : /*
2061 : * Otherwise, see if we can determine the implication by finding the
2062 : * operators' relationship via some btree opfamily.
2063 : */
2064 2446 : return operator_same_subexprs_lookup(pred_op, clause_op, refute_it);
2065 : }
2066 :
2067 :
2068 : /*
2069 : * We use a lookaside table to cache the result of btree proof operator
2070 : * lookups, since the actual lookup is pretty expensive and doesn't change
2071 : * for any given pair of operators (at least as long as pg_amop doesn't
2072 : * change). A single hash entry stores both implication and refutation
2073 : * results for a given pair of operators; but note we may have determined
2074 : * only one of those sets of results as yet.
2075 : */
2076 : typedef struct OprProofCacheKey
2077 : {
2078 : Oid pred_op; /* predicate operator */
2079 : Oid clause_op; /* clause operator */
2080 : } OprProofCacheKey;
2081 :
2082 : typedef struct OprProofCacheEntry
2083 : {
2084 : /* the hash lookup key MUST BE FIRST */
2085 : OprProofCacheKey key;
2086 :
2087 : bool have_implic; /* do we know the implication result? */
2088 : bool have_refute; /* do we know the refutation result? */
2089 : bool same_subexprs_implies; /* X clause_op Y implies X pred_op Y? */
2090 : bool same_subexprs_refutes; /* X clause_op Y refutes X pred_op Y? */
2091 : Oid implic_test_op; /* OID of the test operator, or 0 if none */
2092 : Oid refute_test_op; /* OID of the test operator, or 0 if none */
2093 : } OprProofCacheEntry;
2094 :
2095 : static HTAB *OprProofCacheHash = NULL;
2096 :
2097 :
2098 : /*
2099 : * lookup_proof_cache
2100 : * Get, and fill in if necessary, the appropriate cache entry.
2101 : */
2102 : static OprProofCacheEntry *
2103 32225 : lookup_proof_cache(Oid pred_op, Oid clause_op, bool refute_it)
2104 : {
2105 : OprProofCacheKey key;
2106 : OprProofCacheEntry *cache_entry;
2107 : bool cfound;
2108 32225 : bool same_subexprs = false;
2109 32225 : Oid test_op = InvalidOid;
2110 32225 : bool found = false;
2111 : List *pred_op_infos,
2112 : *clause_op_infos;
2113 : ListCell *lcp,
2114 : *lcc;
2115 :
2116 : /*
2117 : * Find or make a cache entry for this pair of operators.
2118 : */
2119 32225 : if (OprProofCacheHash == NULL)
2120 : {
2121 : /* First time through: initialize the hash table */
2122 : HASHCTL ctl;
2123 :
2124 222 : ctl.keysize = sizeof(OprProofCacheKey);
2125 222 : ctl.entrysize = sizeof(OprProofCacheEntry);
2126 222 : OprProofCacheHash = hash_create("Btree proof lookup cache", 256,
2127 : &ctl, HASH_ELEM | HASH_BLOBS);
2128 :
2129 : /* Arrange to flush cache on pg_amop changes */
2130 222 : CacheRegisterSyscacheCallback(AMOPOPID,
2131 : InvalidateOprProofCacheCallBack,
2132 : (Datum) 0);
2133 : }
2134 :
2135 32225 : key.pred_op = pred_op;
2136 32225 : key.clause_op = clause_op;
2137 32225 : cache_entry = (OprProofCacheEntry *) hash_search(OprProofCacheHash,
2138 : &key,
2139 : HASH_ENTER, &cfound);
2140 32225 : if (!cfound)
2141 : {
2142 : /* new cache entry, set it invalid */
2143 823 : cache_entry->have_implic = false;
2144 823 : cache_entry->have_refute = false;
2145 : }
2146 : else
2147 : {
2148 : /* pre-existing cache entry, see if we know the answer yet */
2149 31402 : if (refute_it ? cache_entry->have_refute : cache_entry->have_implic)
2150 31338 : return cache_entry;
2151 : }
2152 :
2153 : /*
2154 : * Try to find a btree opfamily containing the given operators.
2155 : *
2156 : * We must find a btree opfamily that contains both operators, else the
2157 : * implication can't be determined. Also, the opfamily must contain a
2158 : * suitable test operator taking the operators' righthand datatypes.
2159 : *
2160 : * If there are multiple matching opfamilies, assume we can use any one to
2161 : * determine the logical relationship of the two operators and the correct
2162 : * corresponding test operator. This should work for any logically
2163 : * consistent opfamilies.
2164 : *
2165 : * Note that we can determine the operators' relationship for
2166 : * same-subexprs cases even from an opfamily that lacks a usable test
2167 : * operator. This can happen in cases with incomplete sets of cross-type
2168 : * comparison operators.
2169 : */
2170 887 : clause_op_infos = get_op_index_interpretation(clause_op);
2171 887 : if (clause_op_infos)
2172 879 : pred_op_infos = get_op_index_interpretation(pred_op);
2173 : else /* no point in looking */
2174 8 : pred_op_infos = NIL;
2175 :
2176 1035 : foreach(lcp, pred_op_infos)
2177 : {
2178 605 : OpIndexInterpretation *pred_op_info = lfirst(lcp);
2179 605 : Oid opfamily_id = pred_op_info->opfamily_id;
2180 :
2181 769 : foreach(lcc, clause_op_infos)
2182 : {
2183 621 : OpIndexInterpretation *clause_op_info = lfirst(lcc);
2184 : CompareType pred_cmptype,
2185 : clause_cmptype,
2186 : test_cmptype;
2187 :
2188 : /* Must find them in same opfamily */
2189 621 : if (opfamily_id != clause_op_info->opfamily_id)
2190 16 : continue;
2191 : /* Lefttypes should match */
2192 : Assert(clause_op_info->oplefttype == pred_op_info->oplefttype);
2193 :
2194 605 : pred_cmptype = pred_op_info->cmptype;
2195 605 : clause_cmptype = clause_op_info->cmptype;
2196 :
2197 : /*
2198 : * Check to see if we can make a proof for same-subexpressions
2199 : * cases based on the operators' relationship in this opfamily.
2200 : */
2201 605 : if (refute_it)
2202 366 : same_subexprs |= RC_refutes_table[clause_cmptype - 1][pred_cmptype - 1];
2203 : else
2204 239 : same_subexprs |= RC_implies_table[clause_cmptype - 1][pred_cmptype - 1];
2205 :
2206 : /*
2207 : * Look up the "test" cmptype number in the implication table
2208 : */
2209 605 : if (refute_it)
2210 366 : test_cmptype = RC_refute_table[clause_cmptype - 1][pred_cmptype - 1];
2211 : else
2212 239 : test_cmptype = RC_implic_table[clause_cmptype - 1][pred_cmptype - 1];
2213 :
2214 605 : if (test_cmptype == 0)
2215 : {
2216 : /* Can't determine implication using this interpretation */
2217 148 : continue;
2218 : }
2219 :
2220 : /*
2221 : * See if opfamily has an operator for the test cmptype and the
2222 : * datatypes.
2223 : */
2224 457 : if (test_cmptype == RCNE)
2225 : {
2226 63 : test_op = get_opfamily_member_for_cmptype(opfamily_id,
2227 : pred_op_info->oprighttype,
2228 : clause_op_info->oprighttype,
2229 : COMPARE_EQ);
2230 63 : if (OidIsValid(test_op))
2231 63 : test_op = get_negator(test_op);
2232 : }
2233 : else
2234 : {
2235 394 : test_op = get_opfamily_member_for_cmptype(opfamily_id,
2236 : pred_op_info->oprighttype,
2237 : clause_op_info->oprighttype,
2238 : test_cmptype);
2239 : }
2240 :
2241 457 : if (!OidIsValid(test_op))
2242 0 : continue;
2243 :
2244 : /*
2245 : * Last check: test_op must be immutable.
2246 : *
2247 : * Note that we require only the test_op to be immutable, not the
2248 : * original clause_op. (pred_op is assumed to have been checked
2249 : * immutable by the caller.) Essentially we are assuming that the
2250 : * opfamily is consistent even if it contains operators that are
2251 : * merely stable.
2252 : */
2253 457 : if (op_volatile(test_op) == PROVOLATILE_IMMUTABLE)
2254 : {
2255 457 : found = true;
2256 457 : break;
2257 : }
2258 : }
2259 :
2260 605 : if (found)
2261 457 : break;
2262 : }
2263 :
2264 887 : list_free_deep(pred_op_infos);
2265 887 : list_free_deep(clause_op_infos);
2266 :
2267 887 : if (!found)
2268 : {
2269 : /* couldn't find a suitable comparison operator */
2270 430 : test_op = InvalidOid;
2271 : }
2272 :
2273 : /*
2274 : * If we think we were able to prove something about same-subexpressions
2275 : * cases, check to make sure the clause_op is immutable before believing
2276 : * it completely. (Usually, the clause_op would be immutable if the
2277 : * pred_op is, but it's not entirely clear that this must be true in all
2278 : * cases, so let's check.)
2279 : */
2280 1160 : if (same_subexprs &&
2281 273 : op_volatile(clause_op) != PROVOLATILE_IMMUTABLE)
2282 0 : same_subexprs = false;
2283 :
2284 : /* Cache the results, whether positive or negative */
2285 887 : if (refute_it)
2286 : {
2287 366 : cache_entry->refute_test_op = test_op;
2288 366 : cache_entry->same_subexprs_refutes = same_subexprs;
2289 366 : cache_entry->have_refute = true;
2290 : }
2291 : else
2292 : {
2293 521 : cache_entry->implic_test_op = test_op;
2294 521 : cache_entry->same_subexprs_implies = same_subexprs;
2295 521 : cache_entry->have_implic = true;
2296 : }
2297 :
2298 887 : return cache_entry;
2299 : }
2300 :
2301 : /*
2302 : * operator_same_subexprs_lookup
2303 : * Convenience subroutine to look up the cached answer for
2304 : * same-subexpressions cases.
2305 : */
2306 : static bool
2307 2446 : operator_same_subexprs_lookup(Oid pred_op, Oid clause_op, bool refute_it)
2308 : {
2309 : OprProofCacheEntry *cache_entry;
2310 :
2311 2446 : cache_entry = lookup_proof_cache(pred_op, clause_op, refute_it);
2312 2446 : if (refute_it)
2313 2320 : return cache_entry->same_subexprs_refutes;
2314 : else
2315 126 : return cache_entry->same_subexprs_implies;
2316 : }
2317 :
2318 : /*
2319 : * get_btree_test_op
2320 : * Identify the comparison operator needed for a btree-operator
2321 : * proof or refutation involving comparison of constants.
2322 : *
2323 : * Given the truth of a clause "var clause_op const1", we are attempting to
2324 : * prove or refute a predicate "var pred_op const2". The identities of the
2325 : * two operators are sufficient to determine the operator (if any) to compare
2326 : * const2 to const1 with.
2327 : *
2328 : * Returns the OID of the operator to use, or InvalidOid if no proof is
2329 : * possible.
2330 : */
2331 : static Oid
2332 29779 : get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it)
2333 : {
2334 : OprProofCacheEntry *cache_entry;
2335 :
2336 29779 : cache_entry = lookup_proof_cache(pred_op, clause_op, refute_it);
2337 29779 : if (refute_it)
2338 26720 : return cache_entry->refute_test_op;
2339 : else
2340 3059 : return cache_entry->implic_test_op;
2341 : }
2342 :
2343 :
2344 : /*
2345 : * Callback for pg_amop inval events
2346 : */
2347 : static void
2348 466 : InvalidateOprProofCacheCallBack(Datum arg, SysCacheIdentifier cacheid,
2349 : uint32 hashvalue)
2350 : {
2351 : HASH_SEQ_STATUS status;
2352 : OprProofCacheEntry *hentry;
2353 :
2354 : Assert(OprProofCacheHash != NULL);
2355 :
2356 : /* Currently we just reset all entries; hard to be smarter ... */
2357 466 : hash_seq_init(&status, OprProofCacheHash);
2358 :
2359 3161 : while ((hentry = (OprProofCacheEntry *) hash_seq_search(&status)) != NULL)
2360 : {
2361 2695 : hentry->have_implic = false;
2362 2695 : hentry->have_refute = false;
2363 : }
2364 466 : }
|
