LCOV - code coverage report
Current view: top level - src/backend/optimizer/util - predtest.c (source / functions) Hit Total Coverage
Test: PostgreSQL 17devel Lines: 661 702 94.2 %
Date: 2024-03-28 23:11:20 Functions: 26 26 100.0 %
Legend: Lines: hit not hit

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

Generated by: LCOV version 1.14