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

Generated by: LCOV version 1.13