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