src/backend/optimizer/util/predtest.c

   1 /*-------------------------------------------------------------------------
   2  *
   3  * predtest.c
   4  *        Routines to attempt to prove logical implications between predicate
   5  *        expressions.
   6  *
   7  * Portions Copyright (c) 1996-2011, 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_amop.h"
  19 #include "catalog/pg_proc.h"
  20 #include "catalog/pg_type.h"
  21 #include "executor/executor.h"
  22 #include "miscadmin.h"
  23 #include "nodes/nodeFuncs.h"
  24 #include "optimizer/clauses.h"
  25 #include "optimizer/planmain.h"
  26 #include "optimizer/predtest.h"
  27 #include "utils/array.h"
  28 #include "utils/inval.h"
  29 #include "utils/lsyscache.h"
  30 #include "utils/syscache.h"
  31
  32
  33 /*
  34  * Proof attempts involving large arrays in ScalarArrayOpExpr nodes are
  35  * likely to require O(N^2) time, and more often than not fail anyway.
  36  * So we set an arbitrary limit on the number of array elements that
  37  * we will allow to be treated as an AND or OR clause.
  38  * XXX is it worth exposing this as a GUC knob?
  39  */
  40 #define MAX_SAOP_ARRAY_SIZE             100
  41
  42 /*
  43  * To avoid redundant coding in predicate_implied_by_recurse and
  44  * predicate_refuted_by_recurse, we need to abstract out the notion of
  45  * iterating over the components of an expression that is logically an AND
  46  * or OR structure.  There are multiple sorts of expression nodes that can
  47  * be treated as ANDs or ORs, and we don't want to code each one separately.
  48  * Hence, these types and support routines.
  49  */
  50 typedef enum
  51 {
  52         CLASS_ATOM,                                     /* expression that's not AND or OR */
  53         CLASS_AND,                                      /* expression with AND semantics */
  54         CLASS_OR                                        /* expression with OR semantics */
  55 } PredClass;
  56
  57 typedef struct PredIterInfoData *PredIterInfo;
  58
  59 typedef struct PredIterInfoData
  60 {
  61         /* node-type-specific iteration state */
  62         void       *state;
  63         /* 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 static bool predicate_refuted_by_recurse(Node *clause, Node *predicate);
  84 static PredClass predicate_classify(Node *clause, PredIterInfo info);
  85 static void list_startup_fn(Node *clause, PredIterInfo info);
  86 static Node *list_next_fn(PredIterInfo info);
  87 static void list_cleanup_fn(PredIterInfo info);
  88 static void boolexpr_startup_fn(Node *clause, PredIterInfo info);
  89 static void arrayconst_startup_fn(Node *clause, PredIterInfo info);
  90 static Node *arrayconst_next_fn(PredIterInfo info);
  91 static void arrayconst_cleanup_fn(PredIterInfo info);
  92 static void arrayexpr_startup_fn(Node *clause, PredIterInfo info);
  93 static Node *arrayexpr_next_fn(PredIterInfo info);
  94 static void arrayexpr_cleanup_fn(PredIterInfo info);
  95 static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause);
  96 static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause);
  97 static Node *extract_not_arg(Node *clause);
  98 static Node *extract_strong_not_arg(Node *clause);
  99 static bool list_member_strip(List *list, Expr *datum);
 100 static bool btree_predicate_proof(Expr *predicate, Node *clause,
 101                                           bool refute_it);
 102 static Oid      get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it);
 103 static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, ItemPointer tuplePtr);
 104
 105
 106 /*
 107  * predicate_implied_by
 108  *        Recursively checks whether the clauses in restrictinfo_list imply
 109  *        that the given predicate is true.
 110  *
 111  * The top-level List structure of each list corresponds to an AND list.
 112  * We assume that eval_const_expressions() has been applied and so there
 113  * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
 114  * including AND just below the top-level List structure).
 115  * If this is not true we might fail to prove an implication that is
 116  * valid, but no worse consequences will ensue.
 117  *
 118  * We assume the predicate has already been checked to contain only
 119  * immutable functions and operators.  (In most current uses this is true
 120  * because the predicate is part of an index predicate that has passed
 121  * CheckPredicate().)  We dare not make deductions based on non-immutable
 122  * functions, because they might change answers between the time we make
 123  * the plan and the time we execute the plan.
 124  */
 125 bool
 126 predicate_implied_by(List *predicate_list, List *restrictinfo_list)
 127 {
 128         Node       *p,
 129                            *r;
 130
 131         if (predicate_list == NIL)
 132                 return true;                    /* no predicate: implication is vacuous */
 133         if (restrictinfo_list == NIL)
 134                 return false;                   /* no restriction: implication must fail */
 135
 136         /*
 137          * If either input is a single-element list, replace it with its lone
 138          * member; this avoids one useless level of AND-recursion.      We only need
 139          * to worry about this at top level, since eval_const_expressions should
 140          * have gotten rid of any trivial ANDs or ORs below that.
 141          */
 142         if (list_length(predicate_list) == 1)
 143                 p = (Node *) linitial(predicate_list);
 144         else
 145                 p = (Node *) predicate_list;
 146         if (list_length(restrictinfo_list) == 1)
 147                 r = (Node *) linitial(restrictinfo_list);
 148         else
 149                 r = (Node *) restrictinfo_list;
 150
 151         /* And away we go ... */
 152         return predicate_implied_by_recurse(r, p);
 153 }
 154
 155 /*
 156  * predicate_refuted_by
 157  *        Recursively checks whether the clauses in restrictinfo_list refute
 158  *        the given predicate (that is, prove it false).
 159  *
 160  * This is NOT the same as !(predicate_implied_by), though it is similar
 161  * in the technique and structure of the code.
 162  *
 163  * An important fine point is that truth of the clauses must imply that
 164  * the predicate returns FALSE, not that it does not return TRUE.  This
 165  * is normally used to try to refute CHECK constraints, and the only
 166  * thing we can assume about a CHECK constraint is that it didn't return
 167  * FALSE --- a NULL result isn't a violation per the SQL spec.  (Someday
 168  * perhaps this code should be extended to support both "strong" and
 169  * "weak" refutation, but for now we only need "strong".)
 170  *
 171  * The top-level List structure of each list corresponds to an AND list.
 172  * We assume that eval_const_expressions() has been applied and so there
 173  * are no un-flattened ANDs or ORs (e.g., no AND immediately within an AND,
 174  * including AND just below the top-level List structure).
 175  * If this is not true we might fail to prove an implication that is
 176  * valid, but no worse consequences will ensue.
 177  *
 178  * We assume the predicate has already been checked to contain only
 179  * immutable functions and operators.  We dare not make deductions based on
 180  * non-immutable functions, because they might change answers between the
 181  * time we make the plan and the time we execute the plan.
 182  */
 183 bool
 184 predicate_refuted_by(List *predicate_list, List *restrictinfo_list)
 185 {
 186         Node       *p,
 187                            *r;
 188
 189         if (predicate_list == NIL)
 190                 return false;                   /* no predicate: no refutation is possible */
 191         if (restrictinfo_list == NIL)
 192                 return false;                   /* no restriction: refutation must fail */
 193
 194         /*
 195          * If either input is a single-element list, replace it with its lone
 196          * member; this avoids one useless level of AND-recursion.      We only need
 197          * to worry about this at top level, since eval_const_expressions should
 198          * have gotten rid of any trivial ANDs or ORs below that.
 199          */
 200         if (list_length(predicate_list) == 1)
 201                 p = (Node *) linitial(predicate_list);
 202         else
 203                 p = (Node *) predicate_list;
 204         if (list_length(restrictinfo_list) == 1)
 205                 r = (Node *) linitial(restrictinfo_list);
 206         else
 207                 r = (Node *) restrictinfo_list;
 208
 209         /* And away we go ... */
 210         return predicate_refuted_by_recurse(r, p);
 211 }
 212
 213 /*----------
 214  * predicate_implied_by_recurse
 215  *        Does the predicate implication test for non-NULL restriction and
 216  *        predicate clauses.
 217  *
 218  * The logic followed here is ("=>" means "implies"):
 219  *      atom A => atom B iff:                   predicate_implied_by_simple_clause says so
 220  *      atom A => AND-expr B iff:               A => each of B's components
 221  *      atom A => OR-expr B iff:                A => any of B's components
 222  *      AND-expr A => atom B iff:               any of A's components => B
 223  *      AND-expr A => AND-expr B iff:   A => each of B's components
 224  *      AND-expr A => OR-expr B iff:    A => any of B's components,
 225  *                                                                      *or* any of A's components => B
 226  *      OR-expr A => atom B iff:                each of A's components => B
 227  *      OR-expr A => AND-expr B iff:    A => each of B's components
 228  *      OR-expr A => OR-expr B iff:             each of A's components => any of B's
 229  *
 230  * An "atom" is anything other than an AND or OR node.  Notice that we don't
 231  * have any special logic to handle NOT nodes; these should have been pushed
 232  * down or eliminated where feasible by prepqual.c.
 233  *
 234  * We can't recursively expand either side first, but have to interleave
 235  * the expansions per the above rules, to be sure we handle all of these
 236  * examples:
 237  *              (x OR y) => (x OR y OR z)
 238  *              (x AND y AND z) => (x AND y)
 239  *              (x AND y) => ((x AND y) OR z)
 240  *              ((x OR y) AND z) => (x OR y)
 241  * This is still not an exhaustive test, but it handles most normal cases
 242  * under the assumption that both inputs have been AND/OR flattened.
 243  *
 244  * We have to be prepared to handle RestrictInfo nodes in the restrictinfo
 245  * tree, though not in the predicate tree.
 246  *----------
 247  */
 248 static bool
 249 predicate_implied_by_recurse(Node *clause, Node *predicate)
 250 {
 251         PredIterInfoData clause_info;
 252         PredIterInfoData pred_info;
 253         PredClass       pclass;
 254         bool            result;
 255
 256         /* skip through RestrictInfo */
 257         Assert(clause != NULL);
 258         if (IsA(clause, RestrictInfo))
 259                 clause = (Node *) ((RestrictInfo *) clause)->clause;
 260
 261         pclass = predicate_classify(predicate, &pred_info);
 262
 263         switch (predicate_classify(clause, &clause_info))
 264         {
 265                 case CLASS_AND:
 266                         switch (pclass)
 267                         {
 268                                 case CLASS_AND:
 269
 270                                         /*
 271                                          * AND-clause => AND-clause if A implies each of B's items
 272                                          */
 273                                         result = true;
 274                                         iterate_begin(pitem, predicate, pred_info)
 275                                         {
 276                                                 if (!predicate_implied_by_recurse(clause, pitem))
 277                                                 {
 278                                                         result = false;
 279                                                         break;
 280                                                 }
 281                                         }
 282                                         iterate_end(pred_info);
 283                                         return result;
 284
 285                                 case CLASS_OR:
 286
 287                                         /*
 288                                          * AND-clause => OR-clause if A implies any of B's items
 289                                          *
 290                                          * Needed to handle (x AND y) => ((x AND y) OR z)
 291                                          */
 292                                         result = false;
 293                                         iterate_begin(pitem, predicate, pred_info)
 294                                         {
 295                                                 if (predicate_implied_by_recurse(clause, pitem))
 296                                                 {
 297                                                         result = true;
 298                                                         break;
 299                                                 }
 300                                         }
 301                                         iterate_end(pred_info);
 302                                         if (result)
 303                                                 return result;
 304
 305                                         /*
 306                                          * Also check if any of A's items implies B
 307                                          *
 308                                          * Needed to handle ((x OR y) AND z) => (x OR y)
 309                                          */
 310                                         iterate_begin(citem, clause, clause_info)
 311                                         {
 312                                                 if (predicate_implied_by_recurse(citem, predicate))
 313                                                 {
 314                                                         result = true;
 315                                                         break;
 316                                                 }
 317                                         }
 318                                         iterate_end(clause_info);
 319                                         return result;
 320
 321                                 case CLASS_ATOM:
 322
 323                                         /*
 324                                          * AND-clause => atom if any of A's items implies B
 325                                          */
 326                                         result = false;
 327                                         iterate_begin(citem, clause, clause_info)
 328                                         {
 329                                                 if (predicate_implied_by_recurse(citem, predicate))
 330                                                 {
 331                                                         result = true;
 332                                                         break;
 333                                                 }
 334                                         }
 335                                         iterate_end(clause_info);
 336                                         return result;
 337                         }
 338                         break;
 339
 340                 case CLASS_OR:
 341                         switch (pclass)
 342                         {
 343                                 case CLASS_OR:
 344
 345                                         /*
 346                                          * OR-clause => OR-clause if each of A's items implies any
 347                                          * of B's items.  Messy but can't do it any more simply.
 348                                          */
 349                                         result = true;
 350                                         iterate_begin(citem, clause, clause_info)
 351                                         {
 352                                                 bool            presult = false;
 353
 354                                                 iterate_begin(pitem, predicate, pred_info)
 355                                                 {
 356                                                         if (predicate_implied_by_recurse(citem, pitem))
 357                                                         {
 358                                                                 presult = true;
 359                                                                 break;
 360                                                         }
 361                                                 }
 362                                                 iterate_end(pred_info);
 363                                                 if (!presult)
 364                                                 {
 365                                                         result = false;         /* doesn't imply any of B's */
 366                                                         break;
 367                                                 }
 368                                         }
 369                                         iterate_end(clause_info);
 370                                         return result;
 371
 372                                 case CLASS_AND:
 373                                 case CLASS_ATOM:
 374
 375                                         /*
 376                                          * OR-clause => AND-clause if each of A's items implies B
 377                                          *
 378                                          * OR-clause => atom if each of A's items implies B
 379                                          */
 380                                         result = true;
 381                                         iterate_begin(citem, clause, clause_info)
 382                                         {
 383                                                 if (!predicate_implied_by_recurse(citem, predicate))
 384                                                 {
 385                                                         result = false;
 386                                                         break;
 387                                                 }
 388                                         }
 389                                         iterate_end(clause_info);
 390                                         return result;
 391                         }
 392                         break;
 393
 394                 case CLASS_ATOM:
 395                         switch (pclass)
 396                         {
 397                                 case CLASS_AND:
 398
 399                                         /*
 400                                          * atom => AND-clause if A implies each of B's items
 401                                          */
 402                                         result = true;
 403                                         iterate_begin(pitem, predicate, pred_info)
 404                                         {
 405                                                 if (!predicate_implied_by_recurse(clause, pitem))
 406                                                 {
 407                                                         result = false;
 408                                                         break;
 409                                                 }
 410                                         }
 411                                         iterate_end(pred_info);
 412                                         return result;
 413
 414                                 case CLASS_OR:
 415
 416                                         /*
 417                                          * atom => OR-clause if A implies any of B's items
 418                                          */
 419                                         result = false;
 420                                         iterate_begin(pitem, predicate, pred_info)
 421                                         {
 422                                                 if (predicate_implied_by_recurse(clause, pitem))
 423                                                 {
 424                                                         result = true;
 425                                                         break;
 426                                                 }
 427                                         }
 428                                         iterate_end(pred_info);
 429                                         return result;
 430
 431                                 case CLASS_ATOM:
 432
 433                                         /*
 434                                          * atom => atom is the base case
 435                                          */
 436                                         return
 437                                                 predicate_implied_by_simple_clause((Expr *) predicate,
 438                                                                                                                    clause);
 439                         }
 440                         break;
 441         }
 442
 443         /* can't get here */
 444         elog(ERROR, "predicate_classify returned a bogus value");
 445         return false;
 446 }
 447
 448 /*----------
 449  * predicate_refuted_by_recurse
 450  *        Does the predicate refutation test for non-NULL restriction and
 451  *        predicate clauses.
 452  *
 453  * The logic followed here is ("R=>" means "refutes"):
 454  *      atom A R=> atom B iff:                  predicate_refuted_by_simple_clause says so
 455  *      atom A R=> AND-expr B iff:              A R=> any of B's components
 456  *      atom A R=> OR-expr B iff:               A R=> each of B's components
 457  *      AND-expr A R=> atom B iff:              any of A's components R=> B
 458  *      AND-expr A R=> AND-expr B iff:  A R=> any of B's components,
 459  *                                                                      *or* any of A's components R=> B
 460  *      AND-expr A R=> OR-expr B iff:   A R=> each of B's components
 461  *      OR-expr A R=> atom B iff:               each of A's components R=> B
 462  *      OR-expr A R=> AND-expr B iff:   each of A's components R=> any of B's
 463  *      OR-expr A R=> OR-expr B iff:    A R=> each of B's components
 464  *
 465  * In addition, if the predicate is a NOT-clause then we can use
 466  *      A R=> NOT B if:                                 A => B
 467  * This works for several different SQL constructs that assert the non-truth
 468  * of their argument, ie NOT, IS FALSE, IS NOT TRUE, IS UNKNOWN.
 469  * Unfortunately we *cannot* use
 470  *      NOT A R=> B if:                                 B => A
 471  * because this type of reasoning fails to prove that B doesn't yield NULL.
 472  * We can however make the more limited deduction that
 473  *      NOT A R=> A
 474  *
 475  * Other comments are as for predicate_implied_by_recurse().
 476  *----------
 477  */
 478 static bool
 479 predicate_refuted_by_recurse(Node *clause, Node *predicate)
 480 {
 481         PredIterInfoData clause_info;
 482         PredIterInfoData pred_info;
 483         PredClass       pclass;
 484         Node       *not_arg;
 485         bool            result;
 486
 487         /* skip through RestrictInfo */
 488         Assert(clause != NULL);
 489         if (IsA(clause, RestrictInfo))
 490                 clause = (Node *) ((RestrictInfo *) clause)->clause;
 491
 492         pclass = predicate_classify(predicate, &pred_info);
 493
 494         switch (predicate_classify(clause, &clause_info))
 495         {
 496                 case CLASS_AND:
 497                         switch (pclass)
 498                         {
 499                                 case CLASS_AND:
 500
 501                                         /*
 502                                          * AND-clause R=> AND-clause if A refutes any of B's items
 503                                          *
 504                                          * Needed to handle (x AND y) R=> ((!x OR !y) AND z)
 505                                          */
 506                                         result = false;
 507                                         iterate_begin(pitem, predicate, pred_info)
 508                                         {
 509                                                 if (predicate_refuted_by_recurse(clause, pitem))
 510                                                 {
 511                                                         result = true;
 512                                                         break;
 513                                                 }
 514                                         }
 515                                         iterate_end(pred_info);
 516                                         if (result)
 517                                                 return result;
 518
 519                                         /*
 520                                          * Also check if any of A's items refutes B
 521                                          *
 522                                          * Needed to handle ((x OR y) AND z) R=> (!x AND !y)
 523                                          */
 524                                         iterate_begin(citem, clause, clause_info)
 525                                         {
 526                                                 if (predicate_refuted_by_recurse(citem, predicate))
 527                                                 {
 528                                                         result = true;
 529                                                         break;
 530                                                 }
 531                                         }
 532                                         iterate_end(clause_info);
 533                                         return result;
 534
 535                                 case CLASS_OR:
 536
 537                                         /*
 538                                          * AND-clause R=> OR-clause if A refutes each of B's items
 539                                          */
 540                                         result = true;
 541                                         iterate_begin(pitem, predicate, pred_info)
 542                                         {
 543                                                 if (!predicate_refuted_by_recurse(clause, pitem))
 544                                                 {
 545                                                         result = false;
 546                                                         break;
 547                                                 }
 548                                         }
 549                                         iterate_end(pred_info);
 550                                         return result;
 551
 552                                 case CLASS_ATOM:
 553
 554                                         /*
 555                                          * If B is a NOT-clause, A R=> B if A => B's arg
 556                                          */
 557                                         not_arg = extract_not_arg(predicate);
 558                                         if (not_arg &&
 559                                                 predicate_implied_by_recurse(clause, not_arg))
 560                                                 return true;
 561
 562                                         /*
 563                                          * AND-clause R=> atom if any of A's items refutes B
 564                                          */
 565                                         result = false;
 566                                         iterate_begin(citem, clause, clause_info)
 567                                         {
 568                                                 if (predicate_refuted_by_recurse(citem, predicate))
 569                                                 {
 570                                                         result = true;
 571                                                         break;
 572                                                 }
 573                                         }
 574                                         iterate_end(clause_info);
 575                                         return result;
 576                         }
 577                         break;
 578
 579                 case CLASS_OR:
 580                         switch (pclass)
 581                         {
 582                                 case CLASS_OR:
 583
 584                                         /*
 585                                          * OR-clause R=> OR-clause if A refutes each of B's items
 586                                          */
 587                                         result = true;
 588                                         iterate_begin(pitem, predicate, pred_info)
 589                                         {
 590                                                 if (!predicate_refuted_by_recurse(clause, pitem))
 591                                                 {
 592                                                         result = false;
 593                                                         break;
 594                                                 }
 595                                         }
 596                                         iterate_end(pred_info);
 597                                         return result;
 598
 599                                 case CLASS_AND:
 600
 601                                         /*
 602                                          * OR-clause R=> AND-clause if each of A's items refutes
 603                                          * any of B's items.
 604                                          */
 605                                         result = true;
 606                                         iterate_begin(citem, clause, clause_info)
 607                                         {
 608                                                 bool            presult = false;
 609
 610                                                 iterate_begin(pitem, predicate, pred_info)
 611                                                 {
 612                                                         if (predicate_refuted_by_recurse(citem, pitem))
 613                                                         {
 614                                                                 presult = true;
 615                                                                 break;
 616                                                         }
 617                                                 }
 618                                                 iterate_end(pred_info);
 619                                                 if (!presult)
 620                                                 {
 621                                                         result = false;         /* citem refutes nothing */
 622                                                         break;
 623                                                 }
 624                                         }
 625                                         iterate_end(clause_info);
 626                                         return result;
 627
 628                                 case CLASS_ATOM:
 629
 630                                         /*
 631                                          * If B is a NOT-clause, A R=> B if A => B's arg
 632                                          */
 633                                         not_arg = extract_not_arg(predicate);
 634                                         if (not_arg &&
 635                                                 predicate_implied_by_recurse(clause, not_arg))
 636                                                 return true;
 637
 638                                         /*
 639                                          * OR-clause R=> atom if each of A's items refutes B
 640                                          */
 641                                         result = true;
 642                                         iterate_begin(citem, clause, clause_info)
 643                                         {
 644                                                 if (!predicate_refuted_by_recurse(citem, predicate))
 645                                                 {
 646                                                         result = false;
 647                                                         break;
 648                                                 }
 649                                         }
 650                                         iterate_end(clause_info);
 651                                         return result;
 652                         }
 653                         break;
 654
 655                 case CLASS_ATOM:
 656
 657                         /*
 658                          * If A is a strong NOT-clause, A R=> B if B equals A's arg
 659                          *
 660                          * We cannot make the stronger conclusion that B is refuted if B
 661                          * implies A's arg; that would only prove that B is not-TRUE, not
 662                          * that it's not NULL either.  Hence use equal() rather than
 663                          * predicate_implied_by_recurse().      We could do the latter if we
 664                          * ever had a need for the weak form of refutation.
 665                          */
 666                         not_arg = extract_strong_not_arg(clause);
 667                         if (not_arg && equal(predicate, not_arg))
 668                                 return true;
 669
 670                         switch (pclass)
 671                         {
 672                                 case CLASS_AND:
 673
 674                                         /*
 675                                          * atom R=> AND-clause if A refutes any of B's items
 676                                          */
 677                                         result = false;
 678                                         iterate_begin(pitem, predicate, pred_info)
 679                                         {
 680                                                 if (predicate_refuted_by_recurse(clause, pitem))
 681                                                 {
 682                                                         result = true;
 683                                                         break;
 684                                                 }
 685                                         }
 686                                         iterate_end(pred_info);
 687                                         return result;
 688
 689                                 case CLASS_OR:
 690
 691                                         /*
 692                                          * atom R=> OR-clause if A refutes each of B's items
 693                                          */
 694                                         result = true;
 695                                         iterate_begin(pitem, predicate, pred_info)
 696                                         {
 697                                                 if (!predicate_refuted_by_recurse(clause, pitem))
 698                                                 {
 699                                                         result = false;
 700                                                         break;
 701                                                 }
 702                                         }
 703                                         iterate_end(pred_info);
 704                                         return result;
 705
 706                                 case CLASS_ATOM:
 707
 708                                         /*
 709                                          * If B is a NOT-clause, A R=> B if A => B's arg
 710                                          */
 711                                         not_arg = extract_not_arg(predicate);
 712                                         if (not_arg &&
 713                                                 predicate_implied_by_recurse(clause, not_arg))
 714                                                 return true;
 715
 716                                         /*
 717                                          * atom R=> atom is the base case
 718                                          */
 719                                         return
 720                                                 predicate_refuted_by_simple_clause((Expr *) predicate,
 721                                                                                                                    clause);
 722                         }
 723                         break;
 724         }
 725
 726         /* can't get here */
 727         elog(ERROR, "predicate_classify returned a bogus value");
 728         return false;
 729 }
 730
 731
 732 /*
 733  * predicate_classify
 734  *        Classify an expression node as AND-type, OR-type, or neither (an atom).
 735  *
 736  * If the expression is classified as AND- or OR-type, then *info is filled
 737  * in with the functions needed to iterate over its components.
 738  *
 739  * This function also implements enforcement of MAX_SAOP_ARRAY_SIZE: if a
 740  * ScalarArrayOpExpr's array has too many elements, we just classify it as an
 741  * atom.  (This will result in its being passed as-is to the simple_clause
 742  * functions, which will fail to prove anything about it.)      Note that we
 743  * cannot just stop after considering MAX_SAOP_ARRAY_SIZE elements; in general
 744  * that would result in wrong proofs, rather than failing to prove anything.
 745  */
 746 static PredClass
 747 predicate_classify(Node *clause, PredIterInfo info)
 748 {
 749         /* Caller should not pass us NULL, nor a RestrictInfo clause */
 750         Assert(clause != NULL);
 751         Assert(!IsA(clause, RestrictInfo));
 752
 753         /*
 754          * If we see a List, assume it's an implicit-AND list; this is the correct
 755          * semantics for lists of RestrictInfo nodes.
 756          */
 757         if (IsA(clause, List))
 758         {
 759                 info->startup_fn = list_startup_fn;
 760                 info->next_fn = list_next_fn;
 761                 info->cleanup_fn = list_cleanup_fn;
 762                 return CLASS_AND;
 763         }
 764
 765         /* Handle normal AND and OR boolean clauses */
 766         if (and_clause(clause))
 767         {
 768                 info->startup_fn = boolexpr_startup_fn;
 769                 info->next_fn = list_next_fn;
 770                 info->cleanup_fn = list_cleanup_fn;
 771                 return CLASS_AND;
 772         }
 773         if (or_clause(clause))
 774         {
 775                 info->startup_fn = boolexpr_startup_fn;
 776                 info->next_fn = list_next_fn;
 777                 info->cleanup_fn = list_cleanup_fn;
 778                 return CLASS_OR;
 779         }
 780
 781         /* Handle ScalarArrayOpExpr */
 782         if (IsA(clause, ScalarArrayOpExpr))
 783         {
 784                 ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
 785                 Node       *arraynode = (Node *) lsecond(saop->args);
 786
 787                 /*
 788                  * We can break this down into an AND or OR structure, but only if we
 789                  * know how to iterate through expressions for the array's elements.
 790                  * We can do that if the array operand is a non-null constant or a
 791                  * simple ArrayExpr.
 792                  */
 793                 if (arraynode && IsA(arraynode, Const) &&
 794                         !((Const *) arraynode)->constisnull)
 795                 {
 796                         ArrayType  *arrayval;
 797                         int                     nelems;
 798
 799                         arrayval = DatumGetArrayTypeP(((Const *) arraynode)->constvalue);
 800                         nelems = ArrayGetNItems(ARR_NDIM(arrayval), ARR_DIMS(arrayval));
 801                         if (nelems <= MAX_SAOP_ARRAY_SIZE)
 802                         {
 803                                 info->startup_fn = arrayconst_startup_fn;
 804                                 info->next_fn = arrayconst_next_fn;
 805                                 info->cleanup_fn = arrayconst_cleanup_fn;
 806                                 return saop->useOr ? CLASS_OR : CLASS_AND;
 807                         }
 808                 }
 809                 else if (arraynode && IsA(arraynode, ArrayExpr) &&
 810                                  !((ArrayExpr *) arraynode)->multidims &&
 811                                  list_length(((ArrayExpr *) arraynode)->elements) <= MAX_SAOP_ARRAY_SIZE)
 812                 {
 813                         info->startup_fn = arrayexpr_startup_fn;
 814                         info->next_fn = arrayexpr_next_fn;
 815                         info->cleanup_fn = arrayexpr_cleanup_fn;
 816                         return saop->useOr ? CLASS_OR : CLASS_AND;
 817                 }
 818         }
 819
 820         /* None of the above, so it's an atom */
 821         return CLASS_ATOM;
 822 }
 823
 824 /*
 825  * PredIterInfo routines for iterating over regular Lists.      The iteration
 826  * state variable is the next ListCell to visit.
 827  */
 828 static void
 829 list_startup_fn(Node *clause, PredIterInfo info)
 830 {
 831         info->state = (void *) list_head((List *) clause);
 832 }
 833
 834 static Node *
 835 list_next_fn(PredIterInfo info)
 836 {
 837         ListCell   *l = (ListCell *) info->state;
 838         Node       *n;
 839
 840         if (l == NULL)
 841                 return NULL;
 842         n = lfirst(l);
 843         info->state = (void *) lnext(l);
 844         return n;
 845 }
 846
 847 static void
 848 list_cleanup_fn(PredIterInfo info)
 849 {
 850         /* Nothing to clean up */
 851 }
 852
 853 /*
 854  * BoolExpr needs its own startup function, but can use list_next_fn and
 855  * list_cleanup_fn.
 856  */
 857 static void
 858 boolexpr_startup_fn(Node *clause, PredIterInfo info)
 859 {
 860         info->state = (void *) list_head(((BoolExpr *) clause)->args);
 861 }
 862
 863 /*
 864  * PredIterInfo routines for iterating over a ScalarArrayOpExpr with a
 865  * constant array operand.
 866  */
 867 typedef struct
 868 {
 869         OpExpr          opexpr;
 870         Const           constexpr;
 871         int                     next_elem;
 872         int                     num_elems;
 873         Datum      *elem_values;
 874         bool       *elem_nulls;
 875 } ArrayConstIterState;
 876
 877 static void
 878 arrayconst_startup_fn(Node *clause, PredIterInfo info)
 879 {
 880         ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
 881         ArrayConstIterState *state;
 882         Const      *arrayconst;
 883         ArrayType  *arrayval;
 884         int16           elmlen;
 885         bool            elmbyval;
 886         char            elmalign;
 887
 888         /* Create working state struct */
 889         state = (ArrayConstIterState *) palloc(sizeof(ArrayConstIterState));
 890         info->state = (void *) state;
 891
 892         /* Deconstruct the array literal */
 893         arrayconst = (Const *) lsecond(saop->args);
 894         arrayval = DatumGetArrayTypeP(arrayconst->constvalue);
 895         get_typlenbyvalalign(ARR_ELEMTYPE(arrayval),
 896                                                  &elmlen, &elmbyval, &elmalign);
 897         deconstruct_array(arrayval,
 898                                           ARR_ELEMTYPE(arrayval),
 899                                           elmlen, elmbyval, elmalign,
 900                                           &state->elem_values, &state->elem_nulls,
 901                                           &state->num_elems);
 902
 903         /* Set up a dummy OpExpr to return as the per-item node */
 904         state->opexpr.xpr.type = T_OpExpr;
 905         state->opexpr.opno = saop->opno;
 906         state->opexpr.opfuncid = saop->opfuncid;
 907         state->opexpr.opresulttype = BOOLOID;
 908         state->opexpr.opretset = false;
 909         state->opexpr.args = list_copy(saop->args);
 910
 911         /* Set up a dummy Const node to hold the per-element values */
 912         state->constexpr.xpr.type = T_Const;
 913         state->constexpr.consttype = ARR_ELEMTYPE(arrayval);
 914         state->constexpr.consttypmod = -1;
 915         state->constexpr.constcollid = arrayconst->constcollid;
 916         state->constexpr.constlen = elmlen;
 917         state->constexpr.constbyval = elmbyval;
 918         lsecond(state->opexpr.args) = &state->constexpr;
 919
 920         /* Initialize iteration state */
 921         state->next_elem = 0;
 922 }
 923
 924 static Node *
 925 arrayconst_next_fn(PredIterInfo info)
 926 {
 927         ArrayConstIterState *state = (ArrayConstIterState *) info->state;
 928
 929         if (state->next_elem >= state->num_elems)
 930                 return NULL;
 931         state->constexpr.constvalue = state->elem_values[state->next_elem];
 932         state->constexpr.constisnull = state->elem_nulls[state->next_elem];
 933         state->next_elem++;
 934         return (Node *) &(state->opexpr);
 935 }
 936
 937 static void
 938 arrayconst_cleanup_fn(PredIterInfo info)
 939 {
 940         ArrayConstIterState *state = (ArrayConstIterState *) info->state;
 941
 942         pfree(state->elem_values);
 943         pfree(state->elem_nulls);
 944         list_free(state->opexpr.args);
 945         pfree(state);
 946 }
 947
 948 /*
 949  * PredIterInfo routines for iterating over a ScalarArrayOpExpr with a
 950  * one-dimensional ArrayExpr array operand.
 951  */
 952 typedef struct
 953 {
 954         OpExpr          opexpr;
 955         ListCell   *next;
 956 } ArrayExprIterState;
 957
 958 static void
 959 arrayexpr_startup_fn(Node *clause, PredIterInfo info)
 960 {
 961         ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
 962         ArrayExprIterState *state;
 963         ArrayExpr  *arrayexpr;
 964
 965         /* Create working state struct */
 966         state = (ArrayExprIterState *) palloc(sizeof(ArrayExprIterState));
 967         info->state = (void *) state;
 968
 969         /* Set up a dummy OpExpr to return as the per-item node */
 970         state->opexpr.xpr.type = T_OpExpr;
 971         state->opexpr.opno = saop->opno;
 972         state->opexpr.opfuncid = saop->opfuncid;
 973         state->opexpr.opresulttype = BOOLOID;
 974         state->opexpr.opretset = false;
 975         state->opexpr.args = list_copy(saop->args);
 976
 977         /* Initialize iteration variable to first member of ArrayExpr */
 978         arrayexpr = (ArrayExpr *) lsecond(saop->args);
 979         state->next = list_head(arrayexpr->elements);
 980 }
 981
 982 static Node *
 983 arrayexpr_next_fn(PredIterInfo info)
 984 {
 985         ArrayExprIterState *state = (ArrayExprIterState *) info->state;
 986
 987         if (state->next == NULL)
 988                 return NULL;
 989         lsecond(state->opexpr.args) = lfirst(state->next);
 990         state->next = lnext(state->next);
 991         return (Node *) &(state->opexpr);
 992 }
 993
 994 static void
 995 arrayexpr_cleanup_fn(PredIterInfo info)
 996 {
 997         ArrayExprIterState *state = (ArrayExprIterState *) info->state;
 998
 999         list_free(state->opexpr.args);
1000         pfree(state);
1001 }
1002
1003
1004 /*----------
1005  * predicate_implied_by_simple_clause
1006  *        Does the predicate implication test for a "simple clause" predicate
1007  *        and a "simple clause" restriction.
1008  *
1009  * We return TRUE if able to prove the implication, FALSE if not.
1010  *
1011  * We have three strategies for determining whether one simple clause
1012  * implies another:
1013  *
1014  * A simple and general way is to see if they are equal(); this works for any
1015  * kind of expression.  (Actually, there is an implied assumption that the
1016  * functions in the expression are immutable, ie dependent only on their input
1017  * arguments --- but this was checked for the predicate by the caller.)
1018  *
1019  * When the predicate is of the form "foo IS NOT NULL", we can conclude that
1020  * the predicate is implied if the clause is a strict operator or function
1021  * that has "foo" as an input.  In this case the clause must yield NULL when
1022  * "foo" is NULL, which we can take as equivalent to FALSE because we know
1023  * we are within an AND/OR subtree of a WHERE clause.  (Again, "foo" is
1024  * already known immutable, so the clause will certainly always fail.)
1025  *
1026  * Finally, we may be able to deduce something using knowledge about btree
1027  * operator families; this is encapsulated in btree_predicate_proof().
1028  *----------
1029  */
1030 static bool
1031 predicate_implied_by_simple_clause(Expr *predicate, Node *clause)
1032 {
1033         /* Allow interrupting long proof attempts */
1034         CHECK_FOR_INTERRUPTS();
1035
1036         /* First try the equal() test */
1037         if (equal((Node *) predicate, clause))
1038                 return true;
1039
1040         /* Next try the IS NOT NULL case */
1041         if (predicate && IsA(predicate, NullTest) &&
1042                 ((NullTest *) predicate)->nulltesttype == IS_NOT_NULL)
1043         {
1044                 Expr       *nonnullarg = ((NullTest *) predicate)->arg;
1045
1046                 /* row IS NOT NULL does not act in the simple way we have in mind */
1047                 if (!((NullTest *) predicate)->argisrow)
1048                 {
1049                         if (is_opclause(clause) &&
1050                                 list_member_strip(((OpExpr *) clause)->args, nonnullarg) &&
1051                                 op_strict(((OpExpr *) clause)->opno))
1052                                 return true;
1053                         if (is_funcclause(clause) &&
1054                                 list_member_strip(((FuncExpr *) clause)->args, nonnullarg) &&
1055                                 func_strict(((FuncExpr *) clause)->funcid))
1056                                 return true;
1057                 }
1058                 return false;                   /* we can't succeed below... */
1059         }
1060
1061         /* Else try btree operator knowledge */
1062         return btree_predicate_proof(predicate, clause, false);
1063 }
1064
1065 /*----------
1066  * predicate_refuted_by_simple_clause
1067  *        Does the predicate refutation test for a "simple clause" predicate
1068  *        and a "simple clause" restriction.
1069  *
1070  * We return TRUE if able to prove the refutation, FALSE if not.
1071  *
1072  * Unlike the implication case, checking for equal() clauses isn't
1073  * helpful.
1074  *
1075  * When the predicate is of the form "foo IS NULL", we can conclude that
1076  * the predicate is refuted if the clause is a strict operator or function
1077  * that has "foo" as an input (see notes for implication case), or if the
1078  * clause is "foo IS NOT NULL".  A clause "foo IS NULL" refutes a predicate
1079  * "foo IS NOT NULL", but unfortunately does not refute strict predicates,
1080  * because we are looking for strong refutation.  (The motivation for covering
1081  * these cases is to support using IS NULL/IS NOT NULL as partition-defining
1082  * constraints.)
1083  *
1084  * Finally, we may be able to deduce something using knowledge about btree
1085  * operator families; this is encapsulated in btree_predicate_proof().
1086  *----------
1087  */
1088 static bool
1089 predicate_refuted_by_simple_clause(Expr *predicate, Node *clause)
1090 {
1091         /* Allow interrupting long proof attempts */
1092         CHECK_FOR_INTERRUPTS();
1093
1094         /* A simple clause can't refute itself */
1095         /* Worth checking because of relation_excluded_by_constraints() */
1096         if ((Node *) predicate == clause)
1097                 return false;
1098
1099         /* Try the predicate-IS-NULL case */
1100         if (predicate && IsA(predicate, NullTest) &&
1101                 ((NullTest *) predicate)->nulltesttype == IS_NULL)
1102         {
1103                 Expr       *isnullarg = ((NullTest *) predicate)->arg;
1104
1105                 /* row IS NULL does not act in the simple way we have in mind */
1106                 if (((NullTest *) predicate)->argisrow)
1107                         return false;
1108
1109                 /* Any strict op/func on foo refutes foo IS NULL */
1110                 if (is_opclause(clause) &&
1111                         list_member_strip(((OpExpr *) clause)->args, isnullarg) &&
1112                         op_strict(((OpExpr *) clause)->opno))
1113                         return true;
1114                 if (is_funcclause(clause) &&
1115                         list_member_strip(((FuncExpr *) clause)->args, isnullarg) &&
1116                         func_strict(((FuncExpr *) clause)->funcid))
1117                         return true;
1118
1119                 /* foo IS NOT NULL refutes foo IS NULL */
1120                 if (clause && IsA(clause, NullTest) &&
1121                         ((NullTest *) clause)->nulltesttype == IS_NOT_NULL &&
1122                         !((NullTest *) clause)->argisrow &&
1123                         equal(((NullTest *) clause)->arg, isnullarg))
1124                         return true;
1125
1126                 return false;                   /* we can't succeed below... */
1127         }
1128
1129         /* Try the clause-IS-NULL case */
1130         if (clause && IsA(clause, NullTest) &&
1131                 ((NullTest *) clause)->nulltesttype == IS_NULL)
1132         {
1133                 Expr       *isnullarg = ((NullTest *) clause)->arg;
1134
1135                 /* row IS NULL does not act in the simple way we have in mind */
1136                 if (((NullTest *) clause)->argisrow)
1137                         return false;
1138
1139                 /* foo IS NULL refutes foo IS NOT NULL */
1140                 if (predicate && IsA(predicate, NullTest) &&
1141                         ((NullTest *) predicate)->nulltesttype == IS_NOT_NULL &&
1142                         !((NullTest *) predicate)->argisrow &&
1143                         equal(((NullTest *) predicate)->arg, isnullarg))
1144                         return true;
1145
1146                 return false;                   /* we can't succeed below... */
1147         }
1148
1149         /* Else try btree operator knowledge */
1150         return btree_predicate_proof(predicate, clause, true);
1151 }
1152
1153
1154 /*
1155  * If clause asserts the non-truth of a subclause, return that subclause;
1156  * otherwise return NULL.
1157  */
1158 static Node *
1159 extract_not_arg(Node *clause)
1160 {
1161         if (clause == NULL)
1162                 return NULL;
1163         if (IsA(clause, BoolExpr))
1164         {
1165                 BoolExpr   *bexpr = (BoolExpr *) clause;
1166
1167                 if (bexpr->boolop == NOT_EXPR)
1168                         return (Node *) linitial(bexpr->args);
1169         }
1170         else if (IsA(clause, BooleanTest))
1171         {
1172                 BooleanTest *btest = (BooleanTest *) clause;
1173
1174                 if (btest->booltesttype == IS_NOT_TRUE ||
1175                         btest->booltesttype == IS_FALSE ||
1176                         btest->booltesttype == IS_UNKNOWN)
1177                         return (Node *) btest->arg;
1178         }
1179         return NULL;
1180 }
1181
1182 /*
1183  * If clause asserts the falsity of a subclause, return that subclause;
1184  * otherwise return NULL.
1185  */
1186 static Node *
1187 extract_strong_not_arg(Node *clause)
1188 {
1189         if (clause == NULL)
1190                 return NULL;
1191         if (IsA(clause, BoolExpr))
1192         {
1193                 BoolExpr   *bexpr = (BoolExpr *) clause;
1194
1195                 if (bexpr->boolop == NOT_EXPR)
1196                         return (Node *) linitial(bexpr->args);
1197         }
1198         else if (IsA(clause, BooleanTest))
1199         {
1200                 BooleanTest *btest = (BooleanTest *) clause;
1201
1202                 if (btest->booltesttype == IS_FALSE)
1203                         return (Node *) btest->arg;
1204         }
1205         return NULL;
1206 }
1207
1208
1209 /*
1210  * Check whether an Expr is equal() to any member of a list, ignoring
1211  * any top-level RelabelType nodes.  This is legitimate for the purposes
1212  * we use it for (matching IS [NOT] NULL arguments to arguments of strict
1213  * functions) because RelabelType doesn't change null-ness.  It's helpful
1214  * for cases such as a varchar argument of a strict function on text.
1215  */
1216 static bool
1217 list_member_strip(List *list, Expr *datum)
1218 {
1219         ListCell   *cell;
1220
1221         if (datum && IsA(datum, RelabelType))
1222                 datum = ((RelabelType *) datum)->arg;
1223
1224         foreach(cell, list)
1225         {
1226                 Expr       *elem = (Expr *) lfirst(cell);
1227
1228                 if (elem && IsA(elem, RelabelType))
1229                         elem = ((RelabelType *) elem)->arg;
1230
1231                 if (equal(elem, datum))
1232                         return true;
1233         }
1234
1235         return false;
1236 }
1237
1238
1239 /*
1240  * Define an "operator implication table" for btree operators ("strategies"),
1241  * and a similar table for refutation.
1242  *
1243  * The strategy numbers defined by btree indexes (see access/skey.h) are:
1244  *              (1) <   (2) <=   (3) =   (4) >=   (5) >
1245  * and in addition we use (6) to represent <>.  <> is not a btree-indexable
1246  * operator, but we assume here that if an equality operator of a btree
1247  * opfamily has a negator operator, the negator behaves as <> for the opfamily.
1248  *
1249  * The interpretation of:
1250  *
1251  *              test_op = BT_implic_table[given_op-1][target_op-1]
1252  *
1253  * where test_op, given_op and target_op are strategy numbers (from 1 to 6)
1254  * of btree operators, is as follows:
1255  *
1256  *       If you know, for some ATTR, that "ATTR given_op CONST1" is true, and you
1257  *       want to determine whether "ATTR target_op CONST2" must also be true, then
1258  *       you can use "CONST2 test_op CONST1" as a test.  If this test returns true,
1259  *       then the target expression must be true; if the test returns false, then
1260  *       the target expression may be false.
1261  *
1262  * For example, if clause is "Quantity > 10" and pred is "Quantity > 5"
1263  * then we test "5 <= 10" which evals to true, so clause implies pred.
1264  *
1265  * Similarly, the interpretation of a BT_refute_table entry is:
1266  *
1267  *       If you know, for some ATTR, that "ATTR given_op CONST1" is true, and you
1268  *       want to determine whether "ATTR target_op CONST2" must be false, then
1269  *       you can use "CONST2 test_op CONST1" as a test.  If this test returns true,
1270  *       then the target expression must be false; if the test returns false, then
1271  *       the target expression may be true.
1272  *
1273  * For example, if clause is "Quantity > 10" and pred is "Quantity < 5"
1274  * then we test "5 <= 10" which evals to true, so clause refutes pred.
1275  *
1276  * An entry where test_op == 0 means the implication cannot be determined.
1277  */
1278
1279 #define BTLT BTLessStrategyNumber
1280 #define BTLE BTLessEqualStrategyNumber
1281 #define BTEQ BTEqualStrategyNumber
1282 #define BTGE BTGreaterEqualStrategyNumber
1283 #define BTGT BTGreaterStrategyNumber
1284 #define BTNE 6
1285
1286 static const StrategyNumber BT_implic_table[6][6] = {
1287 /*
1288  *                      The target operator:
1289  *
1290  *       LT    LE        EQ    GE        GT    NE
1291  */
1292         {BTGE, BTGE, 0, 0, 0, BTGE},    /* LT */
1293         {BTGT, BTGE, 0, 0, 0, BTGT},    /* LE */
1294         {BTGT, BTGE, BTEQ, BTLE, BTLT, BTNE},           /* EQ */
1295         {0, 0, 0, BTLE, BTLT, BTLT},    /* GE */
1296         {0, 0, 0, BTLE, BTLE, BTLE},    /* GT */
1297         {0, 0, 0, 0, 0, BTEQ}           /* NE */
1298 };
1299
1300 static const StrategyNumber BT_refute_table[6][6] = {
1301 /*
1302  *                      The target operator:
1303  *
1304  *       LT    LE        EQ    GE        GT    NE
1305  */
1306         {0, 0, BTGE, BTGE, BTGE, 0},    /* LT */
1307         {0, 0, BTGT, BTGT, BTGE, 0},    /* LE */
1308         {BTLE, BTLT, BTNE, BTGT, BTGE, BTEQ},           /* EQ */
1309         {BTLE, BTLT, BTLT, 0, 0, 0},    /* GE */
1310         {BTLE, BTLE, BTLE, 0, 0, 0},    /* GT */
1311         {0, 0, BTEQ, 0, 0, 0}           /* NE */
1312 };
1313
1314
1315 /*
1316  * btree_predicate_proof
1317  *        Does the predicate implication or refutation test for a "simple clause"
1318  *        predicate and a "simple clause" restriction, when both are simple
1319  *        operator clauses using related btree operators.
1320  *
1321  * When refute_it == false, we want to prove the predicate true;
1322  * when refute_it == true, we want to prove the predicate false.
1323  * (There is enough common code to justify handling these two cases
1324  * in one routine.)  We return TRUE if able to make the proof, FALSE
1325  * if not able to prove it.
1326  *
1327  * What we look for here is binary boolean opclauses of the form
1328  * "foo op constant", where "foo" is the same in both clauses.  The operators
1329  * and constants can be different but the operators must be in the same btree
1330  * operator family.  We use the above operator implication tables to
1331  * derive implications between nonidentical clauses.  (Note: "foo" is known
1332  * immutable, and constants are surely immutable, but we have to check that
1333  * the operators are too.  As of 8.0 it's possible for opfamilies to contain
1334  * operators that are merely stable, and we dare not make deductions with
1335  * these.)
1336  */
1337 static bool
1338 btree_predicate_proof(Expr *predicate, Node *clause, bool refute_it)
1339 {
1340         Node       *leftop,
1341                            *rightop;
1342         Node       *pred_var,
1343                            *clause_var;
1344         Const      *pred_const,
1345                            *clause_const;
1346         bool            pred_var_on_left,
1347                                 clause_var_on_left;
1348         Oid                     pred_collation,
1349                                 clause_collation;
1350         Oid                     pred_op,
1351                                 clause_op,
1352                                 test_op;
1353         Expr       *test_expr;
1354         ExprState  *test_exprstate;
1355         Datum           test_result;
1356         bool            isNull;
1357         EState     *estate;
1358         MemoryContext oldcontext;
1359
1360         /*
1361          * Both expressions must be binary opclauses with a Const on one side, and
1362          * identical subexpressions on the other sides. Note we don't have to
1363          * think about binary relabeling of the Const node, since that would have
1364          * been folded right into the Const.
1365          *
1366          * If either Const is null, we also fail right away; this assumes that the
1367          * test operator will always be strict.
1368          */
1369         if (!is_opclause(predicate))
1370                 return false;
1371         leftop = get_leftop(predicate);
1372         rightop = get_rightop(predicate);
1373         if (rightop == NULL)
1374                 return false;                   /* not a binary opclause */
1375         if (IsA(rightop, Const))
1376         {
1377                 pred_var = leftop;
1378                 pred_const = (Const *) rightop;
1379                 pred_var_on_left = true;
1380         }
1381         else if (IsA(leftop, Const))
1382         {
1383                 pred_var = rightop;
1384                 pred_const = (Const *) leftop;
1385                 pred_var_on_left = false;
1386         }
1387         else
1388                 return false;                   /* no Const to be found */
1389         if (pred_const->constisnull)
1390                 return false;
1391
1392         if (!is_opclause(clause))
1393                 return false;
1394         leftop = get_leftop((Expr *) clause);
1395         rightop = get_rightop((Expr *) clause);
1396         if (rightop == NULL)
1397                 return false;                   /* not a binary opclause */
1398         if (IsA(rightop, Const))
1399         {
1400                 clause_var = leftop;
1401                 clause_const = (Const *) rightop;
1402                 clause_var_on_left = true;
1403         }
1404         else if (IsA(leftop, Const))
1405         {
1406                 clause_var = rightop;
1407                 clause_const = (Const *) leftop;
1408                 clause_var_on_left = false;
1409         }
1410         else
1411                 return false;                   /* no Const to be found */
1412         if (clause_const->constisnull)
1413                 return false;
1414
1415         /*
1416          * Check for matching subexpressions on the non-Const sides.  We used to
1417          * only allow a simple Var, but it's about as easy to allow any
1418          * expression.  Remember we already know that the pred expression does not
1419          * contain any non-immutable functions, so identical expressions should
1420          * yield identical results.
1421          */
1422         if (!equal(pred_var, clause_var))
1423                 return false;
1424
1425         /*
1426          * They'd better have the same collation, too.
1427          */
1428         pred_collation = ((OpExpr *) predicate)->inputcollid;
1429         clause_collation = ((OpExpr *) clause)->inputcollid;
1430         if (pred_collation != clause_collation)
1431                 return false;
1432
1433         /*
1434          * Okay, get the operators in the two clauses we're comparing. Commute
1435          * them if needed so that we can assume the variables are on the left.
1436          */
1437         pred_op = ((OpExpr *) predicate)->opno;
1438         if (!pred_var_on_left)
1439         {
1440                 pred_op = get_commutator(pred_op);
1441                 if (!OidIsValid(pred_op))
1442                         return false;
1443         }
1444
1445         clause_op = ((OpExpr *) clause)->opno;
1446         if (!clause_var_on_left)
1447         {
1448                 clause_op = get_commutator(clause_op);
1449                 if (!OidIsValid(clause_op))
1450                         return false;
1451         }
1452
1453         /*
1454          * Lookup the comparison operator using the system catalogs and the
1455          * operator implication tables.
1456          */
1457         test_op = get_btree_test_op(pred_op, clause_op, refute_it);
1458
1459         if (!OidIsValid(test_op))
1460         {
1461                 /* couldn't find a suitable comparison operator */
1462                 return false;
1463         }
1464
1465         /*
1466          * Evaluate the test.  For this we need an EState.
1467          */
1468         estate = CreateExecutorState();
1469
1470         /* We can use the estate's working context to avoid memory leaks. */
1471         oldcontext = MemoryContextSwitchTo(estate->es_query_cxt);
1472
1473         /* Build expression tree */
1474         test_expr = make_opclause(test_op,
1475                                                           BOOLOID,
1476                                                           false,
1477                                                           (Expr *) pred_const,
1478                                                           (Expr *) clause_const,
1479                                                           InvalidOid,
1480                                                           pred_collation);
1481
1482         /* Fill in opfuncids */
1483         fix_opfuncids((Node *) test_expr);
1484
1485         /* Prepare it for execution */
1486         test_exprstate = ExecInitExpr(test_expr, NULL);
1487
1488         /* And execute it. */
1489         test_result = ExecEvalExprSwitchContext(test_exprstate,
1490                                                                                         GetPerTupleExprContext(estate),
1491                                                                                         &isNull, NULL);
1492
1493         /* Get back to outer memory context */
1494         MemoryContextSwitchTo(oldcontext);
1495
1496         /* Release all the junk we just created */
1497         FreeExecutorState(estate);
1498
1499         if (isNull)
1500         {
1501                 /* Treat a null result as non-proof ... but it's a tad fishy ... */
1502                 elog(DEBUG2, "null predicate test result");
1503                 return false;
1504         }
1505         return DatumGetBool(test_result);
1506 }
1507
1508
1509 /*
1510  * We use a lookaside table to cache the result of btree proof operator
1511  * lookups, since the actual lookup is pretty expensive and doesn't change
1512  * for any given pair of operators (at least as long as pg_amop doesn't
1513  * change).  A single hash entry stores both positive and negative results
1514  * for a given pair of operators.
1515  */
1516 typedef struct OprProofCacheKey
1517 {
1518         Oid                     pred_op;                /* predicate operator */
1519         Oid                     clause_op;              /* clause operator */
1520 } OprProofCacheKey;
1521
1522 typedef struct OprProofCacheEntry
1523 {
1524         /* the hash lookup key MUST BE FIRST */
1525         OprProofCacheKey key;
1526
1527         bool            have_implic;    /* do we know the implication result? */
1528         bool            have_refute;    /* do we know the refutation result? */
1529         Oid                     implic_test_op; /* OID of the operator, or 0 if none */
1530         Oid                     refute_test_op; /* OID of the operator, or 0 if none */
1531 } OprProofCacheEntry;
1532
1533 static HTAB *OprProofCacheHash = NULL;
1534
1535
1536 /*
1537  * get_btree_test_op
1538  *        Identify the comparison operator needed for a btree-operator
1539  *        proof or refutation.
1540  *
1541  * Given the truth of a predicate "var pred_op const1", we are attempting to
1542  * prove or refute a clause "var clause_op const2".  The identities of the two
1543  * operators are sufficient to determine the operator (if any) to compare
1544  * const2 to const1 with.
1545  *
1546  * Returns the OID of the operator to use, or InvalidOid if no proof is
1547  * possible.
1548  */
1549 static Oid
1550 get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it)
1551 {
1552         OprProofCacheKey key;
1553         OprProofCacheEntry *cache_entry;
1554         bool            cfound;
1555         bool            pred_op_negated;
1556         Oid                     pred_op_negator,
1557                                 clause_op_negator,
1558                                 test_op = InvalidOid;
1559         Oid                     opfamily_id;
1560         bool            found = false;
1561         StrategyNumber pred_strategy,
1562                                 clause_strategy,
1563                                 test_strategy;
1564         Oid                     clause_righttype;
1565         CatCList   *catlist;
1566         int                     i;
1567
1568         /*
1569          * Find or make a cache entry for this pair of operators.
1570          */
1571         if (OprProofCacheHash == NULL)
1572         {
1573                 /* First time through: initialize the hash table */
1574                 HASHCTL         ctl;
1575
1576                 MemSet(&ctl, 0, sizeof(ctl));
1577                 ctl.keysize = sizeof(OprProofCacheKey);
1578                 ctl.entrysize = sizeof(OprProofCacheEntry);
1579                 ctl.hash = tag_hash;
1580                 OprProofCacheHash = hash_create("Btree proof lookup cache", 256,
1581                                                                                 &ctl, HASH_ELEM | HASH_FUNCTION);
1582
1583                 /* Arrange to flush cache on pg_amop changes */
1584                 CacheRegisterSyscacheCallback(AMOPOPID,
1585                                                                           InvalidateOprProofCacheCallBack,
1586                                                                           (Datum) 0);
1587         }
1588
1589         key.pred_op = pred_op;
1590         key.clause_op = clause_op;
1591         cache_entry = (OprProofCacheEntry *) hash_search(OprProofCacheHash,
1592                                                                                                          (void *) &key,
1593                                                                                                          HASH_ENTER, &cfound);
1594         if (!cfound)
1595         {
1596                 /* new cache entry, set it invalid */
1597                 cache_entry->have_implic = false;
1598                 cache_entry->have_refute = false;
1599         }
1600         else
1601         {
1602                 /* pre-existing cache entry, see if we know the answer */
1603                 if (refute_it)
1604                 {
1605                         if (cache_entry->have_refute)
1606                                 return cache_entry->refute_test_op;
1607                 }
1608                 else
1609                 {
1610                         if (cache_entry->have_implic)
1611                                 return cache_entry->implic_test_op;
1612                 }
1613         }
1614
1615         /*
1616          * Try to find a btree opfamily containing the given operators.
1617          *
1618          * We must find a btree opfamily that contains both operators, else the
1619          * implication can't be determined.  Also, the opfamily must contain a
1620          * suitable test operator taking the operators' righthand datatypes.
1621          *
1622          * If there are multiple matching opfamilies, assume we can use any one to
1623          * determine the logical relationship of the two operators and the correct
1624          * corresponding test operator.  This should work for any logically
1625          * consistent opfamilies.
1626          */
1627         catlist = SearchSysCacheList1(AMOPOPID, ObjectIdGetDatum(pred_op));
1628
1629         /*
1630          * If we couldn't find any opfamily containing the pred_op, perhaps it is
1631          * a <> operator.  See if it has a negator that is in an opfamily.
1632          */
1633         pred_op_negated = false;
1634         if (catlist->n_members == 0)
1635         {
1636                 pred_op_negator = get_negator(pred_op);
1637                 if (OidIsValid(pred_op_negator))
1638                 {
1639                         pred_op_negated = true;
1640                         ReleaseSysCacheList(catlist);
1641                         catlist = SearchSysCacheList1(AMOPOPID,
1642                                                                                   ObjectIdGetDatum(pred_op_negator));
1643                 }
1644         }
1645
1646         /* Also may need the clause_op's negator */
1647         clause_op_negator = get_negator(clause_op);
1648
1649         /* Now search the opfamilies */
1650         for (i = 0; i < catlist->n_members; i++)
1651         {
1652                 HeapTuple       pred_tuple = &catlist->members[i]->tuple;
1653                 Form_pg_amop pred_form = (Form_pg_amop) GETSTRUCT(pred_tuple);
1654                 HeapTuple       clause_tuple;
1655
1656                 /* Must be btree */
1657                 if (pred_form->amopmethod != BTREE_AM_OID)
1658                         continue;
1659
1660                 /* Get the predicate operator's btree strategy number */
1661                 opfamily_id = pred_form->amopfamily;
1662                 pred_strategy = (StrategyNumber) pred_form->amopstrategy;
1663                 Assert(pred_strategy >= 1 && pred_strategy <= 5);
1664
1665                 if (pred_op_negated)
1666                 {
1667                         /* Only consider negators that are = */
1668                         if (pred_strategy != BTEqualStrategyNumber)
1669                                 continue;
1670                         pred_strategy = BTNE;
1671                 }
1672
1673                 /*
1674                  * From the same opfamily, find a strategy number for the clause_op,
1675                  * if possible
1676                  */
1677                 clause_tuple = SearchSysCache3(AMOPOPID,
1678                                                                            ObjectIdGetDatum(clause_op),
1679                                                                            CharGetDatum(AMOP_SEARCH),
1680                                                                            ObjectIdGetDatum(opfamily_id));
1681                 if (HeapTupleIsValid(clause_tuple))
1682                 {
1683                         Form_pg_amop clause_form = (Form_pg_amop) GETSTRUCT(clause_tuple);
1684
1685                         /* Get the restriction clause operator's strategy/datatype */
1686                         clause_strategy = (StrategyNumber) clause_form->amopstrategy;
1687                         Assert(clause_strategy >= 1 && clause_strategy <= 5);
1688                         Assert(clause_form->amoplefttype == pred_form->amoplefttype);
1689                         clause_righttype = clause_form->amoprighttype;
1690                         ReleaseSysCache(clause_tuple);
1691                 }
1692                 else if (OidIsValid(clause_op_negator))
1693                 {
1694                         clause_tuple = SearchSysCache3(AMOPOPID,
1695                                                                                    ObjectIdGetDatum(clause_op_negator),
1696                                                                                    CharGetDatum(AMOP_SEARCH),
1697                                                                                    ObjectIdGetDatum(opfamily_id));
1698                         if (HeapTupleIsValid(clause_tuple))
1699                         {
1700                                 Form_pg_amop clause_form = (Form_pg_amop) GETSTRUCT(clause_tuple);
1701
1702                                 /* Get the restriction clause operator's strategy/datatype */
1703                                 clause_strategy = (StrategyNumber) clause_form->amopstrategy;
1704                                 Assert(clause_strategy >= 1 && clause_strategy <= 5);
1705                                 Assert(clause_form->amoplefttype == pred_form->amoplefttype);
1706                                 clause_righttype = clause_form->amoprighttype;
1707                                 ReleaseSysCache(clause_tuple);
1708
1709                                 /* Only consider negators that are = */
1710                                 if (clause_strategy != BTEqualStrategyNumber)
1711                                         continue;
1712                                 clause_strategy = BTNE;
1713                         }
1714                         else
1715                                 continue;
1716                 }
1717                 else
1718                         continue;
1719
1720                 /*
1721                  * Look up the "test" strategy number in the implication table
1722                  */
1723                 if (refute_it)
1724                         test_strategy = BT_refute_table[clause_strategy - 1][pred_strategy - 1];
1725                 else
1726                         test_strategy = BT_implic_table[clause_strategy - 1][pred_strategy - 1];
1727
1728                 if (test_strategy == 0)
1729                 {
1730                         /* Can't determine implication using this interpretation */
1731                         continue;
1732                 }
1733
1734                 /*
1735                  * See if opfamily has an operator for the test strategy and the
1736                  * datatypes.
1737                  */
1738                 if (test_strategy == BTNE)
1739                 {
1740                         test_op = get_opfamily_member(opfamily_id,
1741                                                                                   pred_form->amoprighttype,
1742                                                                                   clause_righttype,
1743                                                                                   BTEqualStrategyNumber);
1744                         if (OidIsValid(test_op))
1745                                 test_op = get_negator(test_op);
1746                 }
1747                 else
1748                 {
1749                         test_op = get_opfamily_member(opfamily_id,
1750                                                                                   pred_form->amoprighttype,
1751                                                                                   clause_righttype,
1752                                                                                   test_strategy);
1753                 }
1754                 if (OidIsValid(test_op))
1755                 {
1756                         /*
1757                          * Last check: test_op must be immutable.
1758                          *
1759                          * Note that we require only the test_op to be immutable, not the
1760                          * original clause_op.  (pred_op is assumed to have been checked
1761                          * immutable by the caller.)  Essentially we are assuming that the
1762                          * opfamily is consistent even if it contains operators that are
1763                          * merely stable.
1764                          */
1765                         if (op_volatile(test_op) == PROVOLATILE_IMMUTABLE)
1766                         {
1767                                 found = true;
1768                                 break;
1769                         }
1770                 }
1771         }
1772
1773         ReleaseSysCacheList(catlist);
1774
1775         if (!found)
1776         {
1777                 /* couldn't find a suitable comparison operator */
1778                 test_op = InvalidOid;
1779         }
1780
1781         /* Cache the result, whether positive or negative */
1782         if (refute_it)
1783         {
1784                 cache_entry->refute_test_op = test_op;
1785                 cache_entry->have_refute = true;
1786         }
1787         else
1788         {
1789                 cache_entry->implic_test_op = test_op;
1790                 cache_entry->have_implic = true;
1791         }
1792
1793         return test_op;
1794 }
1795
1796
1797 /*
1798  * Callback for pg_amop inval events
1799  */
1800 static void
1801 InvalidateOprProofCacheCallBack(Datum arg, int cacheid, ItemPointer tuplePtr)
1802 {
1803         HASH_SEQ_STATUS status;
1804         OprProofCacheEntry *hentry;
1805
1806         Assert(OprProofCacheHash != NULL);
1807
1808         /* Currently we just reset all entries; hard to be smarter ... */
1809         hash_seq_init(&status, OprProofCacheHash);
1810
1811         while ((hentry = (OprProofCacheEntry *) hash_seq_search(&status)) != NULL)
1812         {
1813                 hentry->have_implic = false;
1814                 hentry->have_refute = false;
1815         }
1816 }