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