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