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