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