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