LCOV - code coverage report
Current view: top level - src/backend/optimizer/util - predtest.c (source / functions) Coverage Total Hit
Test: PostgreSQL 20devel Lines: 94.5 % 706 667
Test Date: 2026-07-15 11:15:40 Functions: 100.0 % 26 26
Legend: Lines:     hit not hit
Branches: + taken - not taken # not executed
Branches: 82.0 % 500 410

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

Generated by: LCOV version 2.0-1