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