PostgreSQL Source Code  git master
predtest.c File Reference
#include "postgres.h"
#include "catalog/pg_operator.h"
#include "catalog/pg_proc.h"
#include "catalog/pg_type.h"
#include "executor/executor.h"
#include "miscadmin.h"
#include "nodes/makefuncs.h"
#include "nodes/nodeFuncs.h"
#include "nodes/pathnodes.h"
#include "optimizer/optimizer.h"
#include "utils/array.h"
#include "utils/inval.h"
#include "utils/lsyscache.h"
#include "utils/syscache.h"
Include dependency graph for predtest.c:

Go to the source code of this file.

Data Structures

struct  PredIterInfoData
 
struct  ArrayConstIterState
 
struct  ArrayExprIterState
 
struct  OprProofCacheKey
 
struct  OprProofCacheEntry
 

Macros

#define MAX_SAOP_ARRAY_SIZE   100
 
#define iterate_begin(item, clause, info)
 
#define iterate_end(info)
 
#define BTLT   BTLessStrategyNumber
 
#define BTLE   BTLessEqualStrategyNumber
 
#define BTEQ   BTEqualStrategyNumber
 
#define BTGE   BTGreaterEqualStrategyNumber
 
#define BTGT   BTGreaterStrategyNumber
 
#define BTNE   ROWCOMPARE_NE
 
#define none   0
 

Typedefs

typedef struct PredIterInfoDataPredIterInfo
 
typedef struct PredIterInfoData PredIterInfoData
 
typedef struct OprProofCacheKey OprProofCacheKey
 
typedef struct OprProofCacheEntry OprProofCacheEntry
 

Enumerations

enum  PredClass { CLASS_ATOM , CLASS_AND , CLASS_OR }
 

Functions

static bool predicate_implied_by_recurse (Node *clause, Node *predicate, bool weak)
 
static bool predicate_refuted_by_recurse (Node *clause, Node *predicate, bool weak)
 
static PredClass predicate_classify (Node *clause, PredIterInfo info)
 
static void list_startup_fn (Node *clause, PredIterInfo info)
 
static Nodelist_next_fn (PredIterInfo info)
 
static void list_cleanup_fn (PredIterInfo info)
 
static void boolexpr_startup_fn (Node *clause, PredIterInfo info)
 
static void arrayconst_startup_fn (Node *clause, PredIterInfo info)
 
static Nodearrayconst_next_fn (PredIterInfo info)
 
static void arrayconst_cleanup_fn (PredIterInfo info)
 
static void arrayexpr_startup_fn (Node *clause, PredIterInfo info)
 
static Nodearrayexpr_next_fn (PredIterInfo info)
 
static void arrayexpr_cleanup_fn (PredIterInfo info)
 
static bool predicate_implied_by_simple_clause (Expr *predicate, Node *clause, bool weak)
 
static bool predicate_refuted_by_simple_clause (Expr *predicate, Node *clause, bool weak)
 
static Nodeextract_not_arg (Node *clause)
 
static Nodeextract_strong_not_arg (Node *clause)
 
static bool clause_is_strict_for (Node *clause, Node *subexpr, bool allow_false)
 
static bool operator_predicate_proof (Expr *predicate, Node *clause, bool refute_it, bool weak)
 
static bool operator_same_subexprs_proof (Oid pred_op, Oid clause_op, bool refute_it)
 
static bool operator_same_subexprs_lookup (Oid pred_op, Oid clause_op, bool refute_it)
 
static Oid get_btree_test_op (Oid pred_op, Oid clause_op, bool refute_it)
 
static void InvalidateOprProofCacheCallBack (Datum arg, int cacheid, uint32 hashvalue)
 
bool predicate_implied_by (List *predicate_list, List *clause_list, bool weak)
 
bool predicate_refuted_by (List *predicate_list, List *clause_list, bool weak)
 
static OprProofCacheEntrylookup_proof_cache (Oid pred_op, Oid clause_op, bool refute_it)
 

Variables

static const bool BT_implies_table [6][6]
 
static const bool BT_refutes_table [6][6]
 
static const StrategyNumber BT_implic_table [6][6]
 
static const StrategyNumber BT_refute_table [6][6]
 
static HTABOprProofCacheHash = NULL
 

Macro Definition Documentation

◆ BTEQ

#define BTEQ   BTEqualStrategyNumber

Definition at line 1664 of file predtest.c.

◆ BTGE

#define BTGE   BTGreaterEqualStrategyNumber

Definition at line 1665 of file predtest.c.

◆ BTGT

#define BTGT   BTGreaterStrategyNumber

Definition at line 1666 of file predtest.c.

◆ BTLE

#define BTLE   BTLessEqualStrategyNumber

Definition at line 1663 of file predtest.c.

◆ BTLT

#define BTLT   BTLessStrategyNumber

Definition at line 1662 of file predtest.c.

◆ BTNE

#define BTNE   ROWCOMPARE_NE

Definition at line 1667 of file predtest.c.

◆ iterate_begin

#define iterate_begin (   item,
  clause,
  info 
)
Value:
do { \
Node *item; \
(info).startup_fn((clause), &(info)); \
while ((item = (info).next_fn(&(info))) != NULL)

Definition at line 72 of file predtest.c.

◆ iterate_end

#define iterate_end (   info)
Value:
(info).cleanup_fn(&(info)); \
} while (0)

Definition at line 78 of file predtest.c.

◆ MAX_SAOP_ARRAY_SIZE

#define MAX_SAOP_ARRAY_SIZE   100

Definition at line 40 of file predtest.c.

◆ none

#define none   0

Definition at line 1670 of file predtest.c.

Typedef Documentation

◆ OprProofCacheEntry

◆ OprProofCacheKey

◆ PredIterInfo

typedef struct PredIterInfoData* PredIterInfo

Definition at line 57 of file predtest.c.

◆ PredIterInfoData

Enumeration Type Documentation

◆ PredClass

enum PredClass
Enumerator
CLASS_ATOM 
CLASS_AND 
CLASS_OR 

Definition at line 50 of file predtest.c.

51 {
52  CLASS_ATOM, /* expression that's not AND or OR */
53  CLASS_AND, /* expression with AND semantics */
54  CLASS_OR, /* expression with OR semantics */
55 } PredClass;
PredClass
Definition: predtest.c:51
@ CLASS_AND
Definition: predtest.c:53
@ CLASS_OR
Definition: predtest.c:54
@ CLASS_ATOM
Definition: predtest.c:52

Function Documentation

◆ arrayconst_cleanup_fn()

static void arrayconst_cleanup_fn ( PredIterInfo  info)
static

Definition at line 1021 of file predtest.c.

1022 {
1024 
1025  pfree(state->elem_values);
1026  pfree(state->elem_nulls);
1027  list_free(state->opexpr.args);
1028  pfree(state);
1029 }
void list_free(List *list)
Definition: list.c:1546
void pfree(void *pointer)
Definition: mcxt.c:1521
void * state
Definition: predtest.c:62
Definition: regguts.h:323

References list_free(), pfree(), and PredIterInfoData::state.

Referenced by predicate_classify().

◆ arrayconst_next_fn()

static Node * arrayconst_next_fn ( PredIterInfo  info)
static

Definition at line 1008 of file predtest.c.

1009 {
1011 
1012  if (state->next_elem >= state->num_elems)
1013  return NULL;
1014  state->constexpr.constvalue = state->elem_values[state->next_elem];
1015  state->constexpr.constisnull = state->elem_nulls[state->next_elem];
1016  state->next_elem++;
1017  return (Node *) &(state->opexpr);
1018 }
if(TABLE==NULL||TABLE_index==NULL)
Definition: isn.c:77
Definition: nodes.h:129

References if(), and PredIterInfoData::state.

Referenced by predicate_classify().

◆ arrayconst_startup_fn()

static void arrayconst_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 959 of file predtest.c.

960 {
961  ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
963  Const *arrayconst;
964  ArrayType *arrayval;
965  int16 elmlen;
966  bool elmbyval;
967  char elmalign;
968 
969  /* Create working state struct */
971  info->state = (void *) state;
972 
973  /* Deconstruct the array literal */
974  arrayconst = (Const *) lsecond(saop->args);
975  arrayval = DatumGetArrayTypeP(arrayconst->constvalue);
977  &elmlen, &elmbyval, &elmalign);
978  deconstruct_array(arrayval,
979  ARR_ELEMTYPE(arrayval),
980  elmlen, elmbyval, elmalign,
981  &state->elem_values, &state->elem_nulls,
982  &state->num_elems);
983 
984  /* Set up a dummy OpExpr to return as the per-item node */
985  state->opexpr.xpr.type = T_OpExpr;
986  state->opexpr.opno = saop->opno;
987  state->opexpr.opfuncid = saop->opfuncid;
988  state->opexpr.opresulttype = BOOLOID;
989  state->opexpr.opretset = false;
990  state->opexpr.opcollid = InvalidOid;
991  state->opexpr.inputcollid = saop->inputcollid;
992  state->opexpr.args = list_copy(saop->args);
993 
994  /* Set up a dummy Const node to hold the per-element values */
995  state->constexpr.xpr.type = T_Const;
996  state->constexpr.consttype = ARR_ELEMTYPE(arrayval);
997  state->constexpr.consttypmod = -1;
998  state->constexpr.constcollid = arrayconst->constcollid;
999  state->constexpr.constlen = elmlen;
1000  state->constexpr.constbyval = elmbyval;
1001  lsecond(state->opexpr.args) = &state->constexpr;
1002 
1003  /* Initialize iteration state */
1004  state->next_elem = 0;
1005 }
#define DatumGetArrayTypeP(X)
Definition: array.h:261
#define ARR_ELEMTYPE(a)
Definition: array.h:292
void deconstruct_array(ArrayType *array, Oid elmtype, int elmlen, bool elmbyval, char elmalign, Datum **elemsp, bool **nullsp, int *nelemsp)
Definition: arrayfuncs.c:3612
signed short int16
Definition: c.h:493
List * list_copy(const List *oldlist)
Definition: list.c:1573
void get_typlenbyvalalign(Oid typid, int16 *typlen, bool *typbyval, char *typalign)
Definition: lsyscache.c:2271
void * palloc(Size size)
Definition: mcxt.c:1317
#define lsecond(l)
Definition: pg_list.h:183
#define InvalidOid
Definition: postgres_ext.h:36

References ScalarArrayOpExpr::args, ARR_ELEMTYPE, DatumGetArrayTypeP, deconstruct_array(), get_typlenbyvalalign(), InvalidOid, list_copy(), lsecond, ScalarArrayOpExpr::opno, palloc(), and PredIterInfoData::state.

Referenced by predicate_classify().

◆ arrayexpr_cleanup_fn()

static void arrayexpr_cleanup_fn ( PredIterInfo  info)
static

Definition at line 1081 of file predtest.c.

1082 {
1084 
1085  list_free(state->opexpr.args);
1086  pfree(state);
1087 }

References list_free(), pfree(), and PredIterInfoData::state.

Referenced by predicate_classify().

◆ arrayexpr_next_fn()

static Node * arrayexpr_next_fn ( PredIterInfo  info)
static

Definition at line 1069 of file predtest.c.

1070 {
1072 
1073  if (state->next == NULL)
1074  return NULL;
1075  lsecond(state->opexpr.args) = lfirst(state->next);
1076  state->next = lnext(info->state_list, state->next);
1077  return (Node *) &(state->opexpr);
1078 }
#define lfirst(lc)
Definition: pg_list.h:172
static ListCell * lnext(const List *l, const ListCell *c)
Definition: pg_list.h:343
List * state_list
Definition: predtest.c:63
struct state * next
Definition: regguts.h:332

References if(), lfirst, lnext(), lsecond, state::next, PredIterInfoData::state, and PredIterInfoData::state_list.

Referenced by predicate_classify().

◆ arrayexpr_startup_fn()

static void arrayexpr_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 1042 of file predtest.c.

1043 {
1044  ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
1046  ArrayExpr *arrayexpr;
1047 
1048  /* Create working state struct */
1050  info->state = (void *) state;
1051 
1052  /* Set up a dummy OpExpr to return as the per-item node */
1053  state->opexpr.xpr.type = T_OpExpr;
1054  state->opexpr.opno = saop->opno;
1055  state->opexpr.opfuncid = saop->opfuncid;
1056  state->opexpr.opresulttype = BOOLOID;
1057  state->opexpr.opretset = false;
1058  state->opexpr.opcollid = InvalidOid;
1059  state->opexpr.inputcollid = saop->inputcollid;
1060  state->opexpr.args = list_copy(saop->args);
1061 
1062  /* Initialize iteration variable to first member of ArrayExpr */
1063  arrayexpr = (ArrayExpr *) lsecond(saop->args);
1064  info->state_list = arrayexpr->elements;
1065  state->next = list_head(arrayexpr->elements);
1066 }
static ListCell * list_head(const List *l)
Definition: pg_list.h:128
List * elements
Definition: primnodes.h:1380

References ScalarArrayOpExpr::args, ArrayExpr::elements, InvalidOid, list_copy(), list_head(), lsecond, state::next, ScalarArrayOpExpr::opno, palloc(), PredIterInfoData::state, and PredIterInfoData::state_list.

Referenced by predicate_classify().

◆ boolexpr_startup_fn()

static void boolexpr_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 938 of file predtest.c.

939 {
940  info->state_list = ((BoolExpr *) clause)->args;
941  info->state = (void *) list_head(info->state_list);
942 }

References list_head(), PredIterInfoData::state, and PredIterInfoData::state_list.

Referenced by predicate_classify().

◆ clause_is_strict_for()

static bool clause_is_strict_for ( Node clause,
Node subexpr,
bool  allow_false 
)
static

Definition at line 1460 of file predtest.c.

1461 {
1462  ListCell *lc;
1463 
1464  /* safety checks */
1465  if (clause == NULL || subexpr == NULL)
1466  return false;
1467 
1468  /*
1469  * Look through any RelabelType nodes, so that we can match, say,
1470  * varcharcol with lower(varcharcol::text). (In general we could recurse
1471  * through any nullness-preserving, immutable operation.) We should not
1472  * see stacked RelabelTypes here.
1473  */
1474  if (IsA(clause, RelabelType))
1475  clause = (Node *) ((RelabelType *) clause)->arg;
1476  if (IsA(subexpr, RelabelType))
1477  subexpr = (Node *) ((RelabelType *) subexpr)->arg;
1478 
1479  /* Base case */
1480  if (equal(clause, subexpr))
1481  return true;
1482 
1483  /*
1484  * If we have a strict operator or function, a NULL result is guaranteed
1485  * if any input is forced NULL by subexpr. This is OK even if the op or
1486  * func isn't immutable, since it won't even be called on NULL input.
1487  */
1488  if (is_opclause(clause) &&
1489  op_strict(((OpExpr *) clause)->opno))
1490  {
1491  foreach(lc, ((OpExpr *) clause)->args)
1492  {
1493  if (clause_is_strict_for((Node *) lfirst(lc), subexpr, false))
1494  return true;
1495  }
1496  return false;
1497  }
1498  if (is_funcclause(clause) &&
1499  func_strict(((FuncExpr *) clause)->funcid))
1500  {
1501  foreach(lc, ((FuncExpr *) clause)->args)
1502  {
1503  if (clause_is_strict_for((Node *) lfirst(lc), subexpr, false))
1504  return true;
1505  }
1506  return false;
1507  }
1508 
1509  /*
1510  * CoerceViaIO is strict (whether or not the I/O functions it calls are).
1511  * Likewise, ArrayCoerceExpr is strict for its array argument (regardless
1512  * of what the per-element expression is), ConvertRowtypeExpr is strict at
1513  * the row level, and CoerceToDomain is strict too. These are worth
1514  * checking mainly because it saves us having to explain to users why some
1515  * type coercions are known strict and others aren't.
1516  */
1517  if (IsA(clause, CoerceViaIO))
1518  return clause_is_strict_for((Node *) ((CoerceViaIO *) clause)->arg,
1519  subexpr, false);
1520  if (IsA(clause, ArrayCoerceExpr))
1521  return clause_is_strict_for((Node *) ((ArrayCoerceExpr *) clause)->arg,
1522  subexpr, false);
1523  if (IsA(clause, ConvertRowtypeExpr))
1524  return clause_is_strict_for((Node *) ((ConvertRowtypeExpr *) clause)->arg,
1525  subexpr, false);
1526  if (IsA(clause, CoerceToDomain))
1527  return clause_is_strict_for((Node *) ((CoerceToDomain *) clause)->arg,
1528  subexpr, false);
1529 
1530  /*
1531  * ScalarArrayOpExpr is a special case. Note that we'd only reach here
1532  * with a ScalarArrayOpExpr clause if we failed to deconstruct it into an
1533  * AND or OR tree, as for example if it has too many array elements.
1534  */
1535  if (IsA(clause, ScalarArrayOpExpr))
1536  {
1537  ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
1538  Node *scalarnode = (Node *) linitial(saop->args);
1539  Node *arraynode = (Node *) lsecond(saop->args);
1540 
1541  /*
1542  * If we can prove the scalar input to be null, and the operator is
1543  * strict, then the SAOP result has to be null --- unless the array is
1544  * empty. For an empty array, we'd get either false (for ANY) or true
1545  * (for ALL). So if allow_false = true then the proof succeeds anyway
1546  * for the ANY case; otherwise we can only make the proof if we can
1547  * prove the array non-empty.
1548  */
1549  if (clause_is_strict_for(scalarnode, subexpr, false) &&
1550  op_strict(saop->opno))
1551  {
1552  int nelems = 0;
1553 
1554  if (allow_false && saop->useOr)
1555  return true; /* can succeed even if array is empty */
1556 
1557  if (arraynode && IsA(arraynode, Const))
1558  {
1559  Const *arrayconst = (Const *) arraynode;
1560  ArrayType *arrval;
1561 
1562  /*
1563  * If array is constant NULL then we can succeed, as in the
1564  * case below.
1565  */
1566  if (arrayconst->constisnull)
1567  return true;
1568 
1569  /* Otherwise, we can compute the number of elements. */
1570  arrval = DatumGetArrayTypeP(arrayconst->constvalue);
1571  nelems = ArrayGetNItems(ARR_NDIM(arrval), ARR_DIMS(arrval));
1572  }
1573  else if (arraynode && IsA(arraynode, ArrayExpr) &&
1574  !((ArrayExpr *) arraynode)->multidims)
1575  {
1576  /*
1577  * We can also reliably count the number of array elements if
1578  * the input is a non-multidim ARRAY[] expression.
1579  */
1580  nelems = list_length(((ArrayExpr *) arraynode)->elements);
1581  }
1582 
1583  /* Proof succeeds if array is definitely non-empty */
1584  if (nelems > 0)
1585  return true;
1586  }
1587 
1588  /*
1589  * If we can prove the array input to be null, the proof succeeds in
1590  * all cases, since ScalarArrayOpExpr will always return NULL for a
1591  * NULL array. Otherwise, we're done here.
1592  */
1593  return clause_is_strict_for(arraynode, subexpr, false);
1594  }
1595 
1596  /*
1597  * When recursing into an expression, we might find a NULL constant.
1598  * That's certainly NULL, whether it matches subexpr or not.
1599  */
1600  if (IsA(clause, Const))
1601  return ((Const *) clause)->constisnull;
1602 
1603  return false;
1604 }
#define ARR_NDIM(a)
Definition: array.h:290
#define ARR_DIMS(a)
Definition: array.h:294
int ArrayGetNItems(int ndim, const int *dims)
Definition: arrayutils.c:57
bool equal(const void *a, const void *b)
Definition: equalfuncs.c:223
bool op_strict(Oid opno)
Definition: lsyscache.c:1477
bool func_strict(Oid funcid)
Definition: lsyscache.c:1761
static bool is_opclause(const void *clause)
Definition: nodeFuncs.h:74
static bool is_funcclause(const void *clause)
Definition: nodeFuncs.h:67
#define IsA(nodeptr, _type_)
Definition: nodes.h:158
void * arg
static int list_length(const List *l)
Definition: pg_list.h:152
#define linitial(l)
Definition: pg_list.h:178
static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
Definition: predtest.c:1460

References arg, ScalarArrayOpExpr::args, ARR_DIMS, ARR_NDIM, ArrayGetNItems(), DatumGetArrayTypeP, equal(), func_strict(), is_funcclause(), is_opclause(), IsA, lfirst, linitial, list_length(), lsecond, op_strict(), ScalarArrayOpExpr::opno, and ScalarArrayOpExpr::useOr.

Referenced by predicate_implied_by_simple_clause(), and predicate_refuted_by_simple_clause().

◆ extract_not_arg()

static Node * extract_not_arg ( Node clause)
static

Definition at line 1386 of file predtest.c.

1387 {
1388  if (clause == NULL)
1389  return NULL;
1390  if (IsA(clause, BoolExpr))
1391  {
1392  BoolExpr *bexpr = (BoolExpr *) clause;
1393 
1394  if (bexpr->boolop == NOT_EXPR)
1395  return (Node *) linitial(bexpr->args);
1396  }
1397  else if (IsA(clause, BooleanTest))
1398  {
1399  BooleanTest *btest = (BooleanTest *) clause;
1400 
1401  if (btest->booltesttype == IS_NOT_TRUE ||
1402  btest->booltesttype == IS_FALSE ||
1403  btest->booltesttype == IS_UNKNOWN)
1404  return (Node *) btest->arg;
1405  }
1406  return NULL;
1407 }
@ IS_NOT_TRUE
Definition: primnodes.h:1972
@ IS_UNKNOWN
Definition: primnodes.h:1972
@ IS_FALSE
Definition: primnodes.h:1972
@ NOT_EXPR
Definition: primnodes.h:931
BoolExprType boolop
Definition: primnodes.h:939
List * args
Definition: primnodes.h:940
BoolTestType booltesttype
Definition: primnodes.h:1979
Expr * arg
Definition: primnodes.h:1978

References BooleanTest::arg, BoolExpr::args, BoolExpr::boolop, BooleanTest::booltesttype, IS_FALSE, IS_NOT_TRUE, IS_UNKNOWN, IsA, linitial, and NOT_EXPR.

Referenced by predicate_refuted_by_recurse().

◆ extract_strong_not_arg()

static Node * extract_strong_not_arg ( Node clause)
static

Definition at line 1414 of file predtest.c.

1415 {
1416  if (clause == NULL)
1417  return NULL;
1418  if (IsA(clause, BoolExpr))
1419  {
1420  BoolExpr *bexpr = (BoolExpr *) clause;
1421 
1422  if (bexpr->boolop == NOT_EXPR)
1423  return (Node *) linitial(bexpr->args);
1424  }
1425  else if (IsA(clause, BooleanTest))
1426  {
1427  BooleanTest *btest = (BooleanTest *) clause;
1428 
1429  if (btest->booltesttype == IS_FALSE)
1430  return (Node *) btest->arg;
1431  }
1432  return NULL;
1433 }

References BooleanTest::arg, BoolExpr::args, BoolExpr::boolop, BooleanTest::booltesttype, IS_FALSE, IsA, linitial, and NOT_EXPR.

Referenced by predicate_refuted_by_recurse().

◆ get_btree_test_op()

static Oid get_btree_test_op ( Oid  pred_op,
Oid  clause_op,
bool  refute_it 
)
static

Definition at line 2330 of file predtest.c.

2331 {
2332  OprProofCacheEntry *cache_entry;
2333 
2334  cache_entry = lookup_proof_cache(pred_op, clause_op, refute_it);
2335  if (refute_it)
2336  return cache_entry->refute_test_op;
2337  else
2338  return cache_entry->implic_test_op;
2339 }
static OprProofCacheEntry * lookup_proof_cache(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:2101

References OprProofCacheEntry::implic_test_op, lookup_proof_cache(), and OprProofCacheEntry::refute_test_op.

Referenced by operator_predicate_proof().

◆ InvalidateOprProofCacheCallBack()

static void InvalidateOprProofCacheCallBack ( Datum  arg,
int  cacheid,
uint32  hashvalue 
)
static

Definition at line 2346 of file predtest.c.

2347 {
2348  HASH_SEQ_STATUS status;
2349  OprProofCacheEntry *hentry;
2350 
2351  Assert(OprProofCacheHash != NULL);
2352 
2353  /* Currently we just reset all entries; hard to be smarter ... */
2354  hash_seq_init(&status, OprProofCacheHash);
2355 
2356  while ((hentry = (OprProofCacheEntry *) hash_seq_search(&status)) != NULL)
2357  {
2358  hentry->have_implic = false;
2359  hentry->have_refute = false;
2360  }
2361 }
#define Assert(condition)
Definition: c.h:858
void * hash_seq_search(HASH_SEQ_STATUS *status)
Definition: dynahash.c:1395
void hash_seq_init(HASH_SEQ_STATUS *status, HTAB *hashp)
Definition: dynahash.c:1385
static HTAB * OprProofCacheHash
Definition: predtest.c:2093

References Assert, hash_seq_init(), hash_seq_search(), OprProofCacheEntry::have_implic, OprProofCacheEntry::have_refute, and OprProofCacheHash.

Referenced by lookup_proof_cache().

◆ list_cleanup_fn()

static void list_cleanup_fn ( PredIterInfo  info)
static

Definition at line 928 of file predtest.c.

929 {
930  /* Nothing to clean up */
931 }

Referenced by predicate_classify().

◆ list_next_fn()

static Node * list_next_fn ( PredIterInfo  info)
static

Definition at line 915 of file predtest.c.

916 {
917  ListCell *l = (ListCell *) info->state;
918  Node *n;
919 
920  if (l == NULL)
921  return NULL;
922  n = lfirst(l);
923  info->state = (void *) lnext(info->state_list, l);
924  return n;
925 }

References if(), lfirst, lnext(), PredIterInfoData::state, and PredIterInfoData::state_list.

Referenced by predicate_classify().

◆ list_startup_fn()

static void list_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 908 of file predtest.c.

909 {
910  info->state_list = (List *) clause;
911  info->state = (void *) list_head(info->state_list);
912 }
Definition: pg_list.h:54

References list_head(), PredIterInfoData::state, and PredIterInfoData::state_list.

Referenced by predicate_classify().

◆ lookup_proof_cache()

static OprProofCacheEntry* lookup_proof_cache ( Oid  pred_op,
Oid  clause_op,
bool  refute_it 
)
static

Definition at line 2101 of file predtest.c.

2102 {
2104  OprProofCacheEntry *cache_entry;
2105  bool cfound;
2106  bool same_subexprs = false;
2107  Oid test_op = InvalidOid;
2108  bool found = false;
2109  List *pred_op_infos,
2110  *clause_op_infos;
2111  ListCell *lcp,
2112  *lcc;
2113 
2114  /*
2115  * Find or make a cache entry for this pair of operators.
2116  */
2117  if (OprProofCacheHash == NULL)
2118  {
2119  /* First time through: initialize the hash table */
2120  HASHCTL ctl;
2121 
2122  ctl.keysize = sizeof(OprProofCacheKey);
2123  ctl.entrysize = sizeof(OprProofCacheEntry);
2124  OprProofCacheHash = hash_create("Btree proof lookup cache", 256,
2125  &ctl, HASH_ELEM | HASH_BLOBS);
2126 
2127  /* Arrange to flush cache on pg_amop changes */
2130  (Datum) 0);
2131  }
2132 
2133  key.pred_op = pred_op;
2134  key.clause_op = clause_op;
2136  &key,
2137  HASH_ENTER, &cfound);
2138  if (!cfound)
2139  {
2140  /* new cache entry, set it invalid */
2141  cache_entry->have_implic = false;
2142  cache_entry->have_refute = false;
2143  }
2144  else
2145  {
2146  /* pre-existing cache entry, see if we know the answer yet */
2147  if (refute_it ? cache_entry->have_refute : cache_entry->have_implic)
2148  return cache_entry;
2149  }
2150 
2151  /*
2152  * Try to find a btree opfamily containing the given operators.
2153  *
2154  * We must find a btree opfamily that contains both operators, else the
2155  * implication can't be determined. Also, the opfamily must contain a
2156  * suitable test operator taking the operators' righthand datatypes.
2157  *
2158  * If there are multiple matching opfamilies, assume we can use any one to
2159  * determine the logical relationship of the two operators and the correct
2160  * corresponding test operator. This should work for any logically
2161  * consistent opfamilies.
2162  *
2163  * Note that we can determine the operators' relationship for
2164  * same-subexprs cases even from an opfamily that lacks a usable test
2165  * operator. This can happen in cases with incomplete sets of cross-type
2166  * comparison operators.
2167  */
2168  clause_op_infos = get_op_btree_interpretation(clause_op);
2169  if (clause_op_infos)
2170  pred_op_infos = get_op_btree_interpretation(pred_op);
2171  else /* no point in looking */
2172  pred_op_infos = NIL;
2173 
2174  foreach(lcp, pred_op_infos)
2175  {
2176  OpBtreeInterpretation *pred_op_info = lfirst(lcp);
2177  Oid opfamily_id = pred_op_info->opfamily_id;
2178 
2179  foreach(lcc, clause_op_infos)
2180  {
2181  OpBtreeInterpretation *clause_op_info = lfirst(lcc);
2182  StrategyNumber pred_strategy,
2183  clause_strategy,
2184  test_strategy;
2185 
2186  /* Must find them in same opfamily */
2187  if (opfamily_id != clause_op_info->opfamily_id)
2188  continue;
2189  /* Lefttypes should match */
2190  Assert(clause_op_info->oplefttype == pred_op_info->oplefttype);
2191 
2192  pred_strategy = pred_op_info->strategy;
2193  clause_strategy = clause_op_info->strategy;
2194 
2195  /*
2196  * Check to see if we can make a proof for same-subexpressions
2197  * cases based on the operators' relationship in this opfamily.
2198  */
2199  if (refute_it)
2200  same_subexprs |= BT_refutes_table[clause_strategy - 1][pred_strategy - 1];
2201  else
2202  same_subexprs |= BT_implies_table[clause_strategy - 1][pred_strategy - 1];
2203 
2204  /*
2205  * Look up the "test" strategy number in the implication table
2206  */
2207  if (refute_it)
2208  test_strategy = BT_refute_table[clause_strategy - 1][pred_strategy - 1];
2209  else
2210  test_strategy = BT_implic_table[clause_strategy - 1][pred_strategy - 1];
2211 
2212  if (test_strategy == 0)
2213  {
2214  /* Can't determine implication using this interpretation */
2215  continue;
2216  }
2217 
2218  /*
2219  * See if opfamily has an operator for the test strategy and the
2220  * datatypes.
2221  */
2222  if (test_strategy == BTNE)
2223  {
2224  test_op = get_opfamily_member(opfamily_id,
2225  pred_op_info->oprighttype,
2226  clause_op_info->oprighttype,
2228  if (OidIsValid(test_op))
2229  test_op = get_negator(test_op);
2230  }
2231  else
2232  {
2233  test_op = get_opfamily_member(opfamily_id,
2234  pred_op_info->oprighttype,
2235  clause_op_info->oprighttype,
2236  test_strategy);
2237  }
2238 
2239  if (!OidIsValid(test_op))
2240  continue;
2241 
2242  /*
2243  * Last check: test_op must be immutable.
2244  *
2245  * Note that we require only the test_op to be immutable, not the
2246  * original clause_op. (pred_op is assumed to have been checked
2247  * immutable by the caller.) Essentially we are assuming that the
2248  * opfamily is consistent even if it contains operators that are
2249  * merely stable.
2250  */
2251  if (op_volatile(test_op) == PROVOLATILE_IMMUTABLE)
2252  {
2253  found = true;
2254  break;
2255  }
2256  }
2257 
2258  if (found)
2259  break;
2260  }
2261 
2262  list_free_deep(pred_op_infos);
2263  list_free_deep(clause_op_infos);
2264 
2265  if (!found)
2266  {
2267  /* couldn't find a suitable comparison operator */
2268  test_op = InvalidOid;
2269  }
2270 
2271  /*
2272  * If we think we were able to prove something about same-subexpressions
2273  * cases, check to make sure the clause_op is immutable before believing
2274  * it completely. (Usually, the clause_op would be immutable if the
2275  * pred_op is, but it's not entirely clear that this must be true in all
2276  * cases, so let's check.)
2277  */
2278  if (same_subexprs &&
2279  op_volatile(clause_op) != PROVOLATILE_IMMUTABLE)
2280  same_subexprs = false;
2281 
2282  /* Cache the results, whether positive or negative */
2283  if (refute_it)
2284  {
2285  cache_entry->refute_test_op = test_op;
2286  cache_entry->same_subexprs_refutes = same_subexprs;
2287  cache_entry->have_refute = true;
2288  }
2289  else
2290  {
2291  cache_entry->implic_test_op = test_op;
2292  cache_entry->same_subexprs_implies = same_subexprs;
2293  cache_entry->have_implic = true;
2294  }
2295 
2296  return cache_entry;
2297 }
#define OidIsValid(objectId)
Definition: c.h:775
void * hash_search(HTAB *hashp, const void *keyPtr, HASHACTION action, bool *foundPtr)
Definition: dynahash.c:955
HTAB * hash_create(const char *tabname, long nelem, const HASHCTL *info, int flags)
Definition: dynahash.c:352
@ HASH_ENTER
Definition: hsearch.h:114
#define HASH_ELEM
Definition: hsearch.h:95
#define HASH_BLOBS
Definition: hsearch.h:97
void CacheRegisterSyscacheCallback(int cacheid, SyscacheCallbackFunction func, Datum arg)
Definition: inval.c:1516
void list_free_deep(List *list)
Definition: list.c:1560
Oid get_opfamily_member(Oid opfamily, Oid lefttype, Oid righttype, int16 strategy)
Definition: lsyscache.c:166
List * get_op_btree_interpretation(Oid opno)
Definition: lsyscache.c:601
char op_volatile(Oid opno)
Definition: lsyscache.c:1493
Oid get_negator(Oid opno)
Definition: lsyscache.c:1533
#define NIL
Definition: pg_list.h:68
uintptr_t Datum
Definition: postgres.h:64
unsigned int Oid
Definition: postgres_ext.h:31
static const StrategyNumber BT_refute_table[6][6]
Definition: predtest.c:1711
static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, uint32 hashvalue)
Definition: predtest.c:2346
struct OprProofCacheEntry OprProofCacheEntry
static const bool BT_refutes_table[6][6]
Definition: predtest.c:1685
#define BTNE
Definition: predtest.c:1667
static const bool BT_implies_table[6][6]
Definition: predtest.c:1672
struct OprProofCacheKey OprProofCacheKey
static const StrategyNumber BT_implic_table[6][6]
Definition: predtest.c:1698
tree ctl
Definition: radixtree.h:1853
uint16 StrategyNumber
Definition: stratnum.h:22
#define BTEqualStrategyNumber
Definition: stratnum.h:31
bool same_subexprs_refutes
Definition: predtest.c:2088
bool same_subexprs_implies
Definition: predtest.c:2087

References Assert, BT_implic_table, BT_implies_table, BT_refute_table, BT_refutes_table, BTEqualStrategyNumber, BTNE, CacheRegisterSyscacheCallback(), ctl, get_negator(), get_op_btree_interpretation(), get_opfamily_member(), HASH_BLOBS, hash_create(), HASH_ELEM, HASH_ENTER, hash_search(), OprProofCacheEntry::have_implic, OprProofCacheEntry::have_refute, OprProofCacheEntry::implic_test_op, InvalidateOprProofCacheCallBack(), InvalidOid, sort-test::key, lfirst, list_free_deep(), NIL, OidIsValid, op_volatile(), OpBtreeInterpretation::opfamily_id, OpBtreeInterpretation::oplefttype, OpBtreeInterpretation::oprighttype, OprProofCacheHash, OprProofCacheEntry::refute_test_op, OprProofCacheEntry::same_subexprs_implies, OprProofCacheEntry::same_subexprs_refutes, and OpBtreeInterpretation::strategy.

Referenced by get_btree_test_op(), and operator_same_subexprs_lookup().

◆ operator_predicate_proof()

static bool operator_predicate_proof ( Expr predicate,
Node clause,
bool  refute_it,
bool  weak 
)
static

Definition at line 1779 of file predtest.c.

1781 {
1782  OpExpr *pred_opexpr,
1783  *clause_opexpr;
1784  Oid pred_collation,
1785  clause_collation;
1786  Oid pred_op,
1787  clause_op,
1788  test_op;
1789  Node *pred_leftop,
1790  *pred_rightop,
1791  *clause_leftop,
1792  *clause_rightop;
1793  Const *pred_const,
1794  *clause_const;
1795  Expr *test_expr;
1796  ExprState *test_exprstate;
1797  Datum test_result;
1798  bool isNull;
1799  EState *estate;
1800  MemoryContext oldcontext;
1801 
1802  /*
1803  * Both expressions must be binary opclauses, else we can't do anything.
1804  *
1805  * Note: in future we might extend this logic to other operator-based
1806  * constructs such as DistinctExpr. But the planner isn't very smart
1807  * about DistinctExpr in general, and this probably isn't the first place
1808  * to fix if you want to improve that.
1809  */
1810  if (!is_opclause(predicate))
1811  return false;
1812  pred_opexpr = (OpExpr *) predicate;
1813  if (list_length(pred_opexpr->args) != 2)
1814  return false;
1815  if (!is_opclause(clause))
1816  return false;
1817  clause_opexpr = (OpExpr *) clause;
1818  if (list_length(clause_opexpr->args) != 2)
1819  return false;
1820 
1821  /*
1822  * If they're marked with different collations then we can't do anything.
1823  * This is a cheap test so let's get it out of the way early.
1824  */
1825  pred_collation = pred_opexpr->inputcollid;
1826  clause_collation = clause_opexpr->inputcollid;
1827  if (pred_collation != clause_collation)
1828  return false;
1829 
1830  /* Grab the operator OIDs now too. We may commute these below. */
1831  pred_op = pred_opexpr->opno;
1832  clause_op = clause_opexpr->opno;
1833 
1834  /*
1835  * We have to match up at least one pair of input expressions.
1836  */
1837  pred_leftop = (Node *) linitial(pred_opexpr->args);
1838  pred_rightop = (Node *) lsecond(pred_opexpr->args);
1839  clause_leftop = (Node *) linitial(clause_opexpr->args);
1840  clause_rightop = (Node *) lsecond(clause_opexpr->args);
1841 
1842  if (equal(pred_leftop, clause_leftop))
1843  {
1844  if (equal(pred_rightop, clause_rightop))
1845  {
1846  /* We have x op1 y and x op2 y */
1847  return operator_same_subexprs_proof(pred_op, clause_op, refute_it);
1848  }
1849  else
1850  {
1851  /* Fail unless rightops are both Consts */
1852  if (pred_rightop == NULL || !IsA(pred_rightop, Const))
1853  return false;
1854  pred_const = (Const *) pred_rightop;
1855  if (clause_rightop == NULL || !IsA(clause_rightop, Const))
1856  return false;
1857  clause_const = (Const *) clause_rightop;
1858  }
1859  }
1860  else if (equal(pred_rightop, clause_rightop))
1861  {
1862  /* Fail unless leftops are both Consts */
1863  if (pred_leftop == NULL || !IsA(pred_leftop, Const))
1864  return false;
1865  pred_const = (Const *) pred_leftop;
1866  if (clause_leftop == NULL || !IsA(clause_leftop, Const))
1867  return false;
1868  clause_const = (Const *) clause_leftop;
1869  /* Commute both operators so we can assume Consts are on the right */
1870  pred_op = get_commutator(pred_op);
1871  if (!OidIsValid(pred_op))
1872  return false;
1873  clause_op = get_commutator(clause_op);
1874  if (!OidIsValid(clause_op))
1875  return false;
1876  }
1877  else if (equal(pred_leftop, clause_rightop))
1878  {
1879  if (equal(pred_rightop, clause_leftop))
1880  {
1881  /* We have x op1 y and y op2 x */
1882  /* Commute pred_op that we can treat this like a straight match */
1883  pred_op = get_commutator(pred_op);
1884  if (!OidIsValid(pred_op))
1885  return false;
1886  return operator_same_subexprs_proof(pred_op, clause_op, refute_it);
1887  }
1888  else
1889  {
1890  /* Fail unless pred_rightop/clause_leftop are both Consts */
1891  if (pred_rightop == NULL || !IsA(pred_rightop, Const))
1892  return false;
1893  pred_const = (Const *) pred_rightop;
1894  if (clause_leftop == NULL || !IsA(clause_leftop, Const))
1895  return false;
1896  clause_const = (Const *) clause_leftop;
1897  /* Commute clause_op so we can assume Consts are on the right */
1898  clause_op = get_commutator(clause_op);
1899  if (!OidIsValid(clause_op))
1900  return false;
1901  }
1902  }
1903  else if (equal(pred_rightop, clause_leftop))
1904  {
1905  /* Fail unless pred_leftop/clause_rightop are both Consts */
1906  if (pred_leftop == NULL || !IsA(pred_leftop, Const))
1907  return false;
1908  pred_const = (Const *) pred_leftop;
1909  if (clause_rightop == NULL || !IsA(clause_rightop, Const))
1910  return false;
1911  clause_const = (Const *) clause_rightop;
1912  /* Commute pred_op so we can assume Consts are on the right */
1913  pred_op = get_commutator(pred_op);
1914  if (!OidIsValid(pred_op))
1915  return false;
1916  }
1917  else
1918  {
1919  /* Failed to match up any of the subexpressions, so we lose */
1920  return false;
1921  }
1922 
1923  /*
1924  * We have two identical subexpressions, and two other subexpressions that
1925  * are not identical but are both Consts; and we have commuted the
1926  * operators if necessary so that the Consts are on the right. We'll need
1927  * to compare the Consts' values. If either is NULL, we can't do that, so
1928  * usually the proof fails ... but in some cases we can claim success.
1929  */
1930  if (clause_const->constisnull)
1931  {
1932  /* If clause_op isn't strict, we can't prove anything */
1933  if (!op_strict(clause_op))
1934  return false;
1935 
1936  /*
1937  * At this point we know that the clause returns NULL. For proof
1938  * types that assume truth of the clause, this means the proof is
1939  * vacuously true (a/k/a "false implies anything"). That's all proof
1940  * types except weak implication.
1941  */
1942  if (!(weak && !refute_it))
1943  return true;
1944 
1945  /*
1946  * For weak implication, it's still possible for the proof to succeed,
1947  * if the predicate can also be proven NULL. In that case we've got
1948  * NULL => NULL which is valid for this proof type.
1949  */
1950  if (pred_const->constisnull && op_strict(pred_op))
1951  return true;
1952  /* Else the proof fails */
1953  return false;
1954  }
1955  if (pred_const->constisnull)
1956  {
1957  /*
1958  * If the pred_op is strict, we know the predicate yields NULL, which
1959  * means the proof succeeds for either weak implication or weak
1960  * refutation.
1961  */
1962  if (weak && op_strict(pred_op))
1963  return true;
1964  /* Else the proof fails */
1965  return false;
1966  }
1967 
1968  /*
1969  * Lookup the constant-comparison operator using the system catalogs and
1970  * the operator implication tables.
1971  */
1972  test_op = get_btree_test_op(pred_op, clause_op, refute_it);
1973 
1974  if (!OidIsValid(test_op))
1975  {
1976  /* couldn't find a suitable comparison operator */
1977  return false;
1978  }
1979 
1980  /*
1981  * Evaluate the test. For this we need an EState.
1982  */
1983  estate = CreateExecutorState();
1984 
1985  /* We can use the estate's working context to avoid memory leaks. */
1986  oldcontext = MemoryContextSwitchTo(estate->es_query_cxt);
1987 
1988  /* Build expression tree */
1989  test_expr = make_opclause(test_op,
1990  BOOLOID,
1991  false,
1992  (Expr *) pred_const,
1993  (Expr *) clause_const,
1994  InvalidOid,
1995  pred_collation);
1996 
1997  /* Fill in opfuncids */
1998  fix_opfuncids((Node *) test_expr);
1999 
2000  /* Prepare it for execution */
2001  test_exprstate = ExecInitExpr(test_expr, NULL);
2002 
2003  /* And execute it. */
2004  test_result = ExecEvalExprSwitchContext(test_exprstate,
2005  GetPerTupleExprContext(estate),
2006  &isNull);
2007 
2008  /* Get back to outer memory context */
2009  MemoryContextSwitchTo(oldcontext);
2010 
2011  /* Release all the junk we just created */
2012  FreeExecutorState(estate);
2013 
2014  if (isNull)
2015  {
2016  /* Treat a null result as non-proof ... but it's a tad fishy ... */
2017  elog(DEBUG2, "null predicate test result");
2018  return false;
2019  }
2020  return DatumGetBool(test_result);
2021 }
#define DEBUG2
Definition: elog.h:29
#define elog(elevel,...)
Definition: elog.h:224
ExprState * ExecInitExpr(Expr *node, PlanState *parent)
Definition: execExpr.c:134
EState * CreateExecutorState(void)
Definition: execUtils.c:88
void FreeExecutorState(EState *estate)
Definition: execUtils.c:189
#define GetPerTupleExprContext(estate)
Definition: executor.h:550
static Datum ExecEvalExprSwitchContext(ExprState *state, ExprContext *econtext, bool *isNull)
Definition: executor.h:348
Oid get_commutator(Oid opno)
Definition: lsyscache.c:1509
Expr * make_opclause(Oid opno, Oid opresulttype, bool opretset, Expr *leftop, Expr *rightop, Oid opcollid, Oid inputcollid)
Definition: makefuncs.c:628
void fix_opfuncids(Node *node)
Definition: nodeFuncs.c:1831
static bool DatumGetBool(Datum X)
Definition: postgres.h:90
static bool operator_same_subexprs_proof(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:2032
static Oid get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:2330
MemoryContextSwitchTo(old_ctx)
MemoryContext es_query_cxt
Definition: execnodes.h:667
Oid opno
Definition: primnodes.h:818
List * args
Definition: primnodes.h:836

References OpExpr::args, CreateExecutorState(), DatumGetBool(), DEBUG2, elog, equal(), EState::es_query_cxt, ExecEvalExprSwitchContext(), ExecInitExpr(), fix_opfuncids(), FreeExecutorState(), get_btree_test_op(), get_commutator(), GetPerTupleExprContext, InvalidOid, is_opclause(), IsA, linitial, list_length(), lsecond, make_opclause(), MemoryContextSwitchTo(), OidIsValid, op_strict(), operator_same_subexprs_proof(), and OpExpr::opno.

Referenced by predicate_implied_by_simple_clause(), and predicate_refuted_by_simple_clause().

◆ operator_same_subexprs_lookup()

static bool operator_same_subexprs_lookup ( Oid  pred_op,
Oid  clause_op,
bool  refute_it 
)
static

Definition at line 2305 of file predtest.c.

2306 {
2307  OprProofCacheEntry *cache_entry;
2308 
2309  cache_entry = lookup_proof_cache(pred_op, clause_op, refute_it);
2310  if (refute_it)
2311  return cache_entry->same_subexprs_refutes;
2312  else
2313  return cache_entry->same_subexprs_implies;
2314 }

References lookup_proof_cache(), OprProofCacheEntry::same_subexprs_implies, and OprProofCacheEntry::same_subexprs_refutes.

Referenced by operator_same_subexprs_proof().

◆ operator_same_subexprs_proof()

static bool operator_same_subexprs_proof ( Oid  pred_op,
Oid  clause_op,
bool  refute_it 
)
static

Definition at line 2032 of file predtest.c.

2033 {
2034  /*
2035  * A simple and general rule is that the predicate is proven if clause_op
2036  * and pred_op are the same, or refuted if they are each other's negators.
2037  * We need not check immutability since the pred_op is already known
2038  * immutable. (Actually, by this point we may have the commutator of a
2039  * known-immutable pred_op, but that should certainly be immutable too.
2040  * Likewise we don't worry whether the pred_op's negator is immutable.)
2041  *
2042  * Note: the "same" case won't get here if we actually had EXPR1 clause_op
2043  * EXPR2 and EXPR1 pred_op EXPR2, because the overall-expression-equality
2044  * test in predicate_implied_by_simple_clause would have caught it. But
2045  * we can see the same operator after having commuted the pred_op.
2046  */
2047  if (refute_it)
2048  {
2049  if (get_negator(pred_op) == clause_op)
2050  return true;
2051  }
2052  else
2053  {
2054  if (pred_op == clause_op)
2055  return true;
2056  }
2057 
2058  /*
2059  * Otherwise, see if we can determine the implication by finding the
2060  * operators' relationship via some btree opfamily.
2061  */
2062  return operator_same_subexprs_lookup(pred_op, clause_op, refute_it);
2063 }
static bool operator_same_subexprs_lookup(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:2305

References get_negator(), and operator_same_subexprs_lookup().

Referenced by operator_predicate_proof().

◆ predicate_classify()

static PredClass predicate_classify ( Node clause,
PredIterInfo  info 
)
static

Definition at line 826 of file predtest.c.

827 {
828  /* Caller should not pass us NULL, nor a RestrictInfo clause */
829  Assert(clause != NULL);
830  Assert(!IsA(clause, RestrictInfo));
831 
832  /*
833  * If we see a List, assume it's an implicit-AND list; this is the correct
834  * semantics for lists of RestrictInfo nodes.
835  */
836  if (IsA(clause, List))
837  {
838  info->startup_fn = list_startup_fn;
839  info->next_fn = list_next_fn;
840  info->cleanup_fn = list_cleanup_fn;
841  return CLASS_AND;
842  }
843 
844  /* Handle normal AND and OR boolean clauses */
845  if (is_andclause(clause))
846  {
848  info->next_fn = list_next_fn;
849  info->cleanup_fn = list_cleanup_fn;
850  return CLASS_AND;
851  }
852  if (is_orclause(clause))
853  {
855  info->next_fn = list_next_fn;
856  info->cleanup_fn = list_cleanup_fn;
857  return CLASS_OR;
858  }
859 
860  /* Handle ScalarArrayOpExpr */
861  if (IsA(clause, ScalarArrayOpExpr))
862  {
863  ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
864  Node *arraynode = (Node *) lsecond(saop->args);
865 
866  /*
867  * We can break this down into an AND or OR structure, but only if we
868  * know how to iterate through expressions for the array's elements.
869  * We can do that if the array operand is a non-null constant or a
870  * simple ArrayExpr.
871  */
872  if (arraynode && IsA(arraynode, Const) &&
873  !((Const *) arraynode)->constisnull)
874  {
875  ArrayType *arrayval;
876  int nelems;
877 
878  arrayval = DatumGetArrayTypeP(((Const *) arraynode)->constvalue);
879  nelems = ArrayGetNItems(ARR_NDIM(arrayval), ARR_DIMS(arrayval));
880  if (nelems <= MAX_SAOP_ARRAY_SIZE)
881  {
883  info->next_fn = arrayconst_next_fn;
885  return saop->useOr ? CLASS_OR : CLASS_AND;
886  }
887  }
888  else if (arraynode && IsA(arraynode, ArrayExpr) &&
889  !((ArrayExpr *) arraynode)->multidims &&
890  list_length(((ArrayExpr *) arraynode)->elements) <= MAX_SAOP_ARRAY_SIZE)
891  {
893  info->next_fn = arrayexpr_next_fn;
895  return saop->useOr ? CLASS_OR : CLASS_AND;
896  }
897  }
898 
899  /* None of the above, so it's an atom */
900  return CLASS_ATOM;
901 }
static bool is_andclause(const void *clause)
Definition: nodeFuncs.h:105
static bool is_orclause(const void *clause)
Definition: nodeFuncs.h:114
static Node * arrayconst_next_fn(PredIterInfo info)
Definition: predtest.c:1008
static Node * arrayexpr_next_fn(PredIterInfo info)
Definition: predtest.c:1069
static void arrayexpr_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:1042
static void boolexpr_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:938
static void arrayconst_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:959
#define MAX_SAOP_ARRAY_SIZE
Definition: predtest.c:40
static void list_cleanup_fn(PredIterInfo info)
Definition: predtest.c:928
static Node * list_next_fn(PredIterInfo info)
Definition: predtest.c:915
static void arrayconst_cleanup_fn(PredIterInfo info)
Definition: predtest.c:1021
static void list_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:908
static void arrayexpr_cleanup_fn(PredIterInfo info)
Definition: predtest.c:1081
void(* startup_fn)(Node *clause, PredIterInfo info)
Definition: predtest.c:65
void(* cleanup_fn)(PredIterInfo info)
Definition: predtest.c:69
Node *(* next_fn)(PredIterInfo info)
Definition: predtest.c:67

References ScalarArrayOpExpr::args, ARR_DIMS, ARR_NDIM, arrayconst_cleanup_fn(), arrayconst_next_fn(), arrayconst_startup_fn(), arrayexpr_cleanup_fn(), arrayexpr_next_fn(), arrayexpr_startup_fn(), ArrayGetNItems(), Assert, boolexpr_startup_fn(), CLASS_AND, CLASS_ATOM, CLASS_OR, PredIterInfoData::cleanup_fn, DatumGetArrayTypeP, is_andclause(), is_orclause(), IsA, list_cleanup_fn(), list_length(), list_next_fn(), list_startup_fn(), lsecond, MAX_SAOP_ARRAY_SIZE, PredIterInfoData::next_fn, PredIterInfoData::startup_fn, and ScalarArrayOpExpr::useOr.

Referenced by predicate_implied_by_recurse(), and predicate_refuted_by_recurse().

◆ predicate_implied_by()

bool predicate_implied_by ( List predicate_list,
List clause_list,
bool  weak 
)

Definition at line 152 of file predtest.c.

154 {
155  Node *p,
156  *c;
157 
158  if (predicate_list == NIL)
159  return true; /* no predicate: implication is vacuous */
160  if (clause_list == NIL)
161  return false; /* no restriction: implication must fail */
162 
163  /*
164  * If either input is a single-element list, replace it with its lone
165  * member; this avoids one useless level of AND-recursion. We only need
166  * to worry about this at top level, since eval_const_expressions should
167  * have gotten rid of any trivial ANDs or ORs below that.
168  */
169  if (list_length(predicate_list) == 1)
170  p = (Node *) linitial(predicate_list);
171  else
172  p = (Node *) predicate_list;
173  if (list_length(clause_list) == 1)
174  c = (Node *) linitial(clause_list);
175  else
176  c = (Node *) clause_list;
177 
178  /* And away we go ... */
179  return predicate_implied_by_recurse(c, p, weak);
180 }
static bool predicate_implied_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:290
char * c

References linitial, list_length(), NIL, and predicate_implied_by_recurse().

Referenced by add_predicate_to_index_quals(), build_paths_for_OR(), check_index_predicates(), choose_bitmap_and(), ConstraintImpliedByRelConstraint(), create_bitmap_scan_plan(), create_bitmap_subplan(), create_indexscan_plan(), infer_arbiter_indexes(), and test_predtest().

◆ predicate_implied_by_recurse()

static bool predicate_implied_by_recurse ( Node clause,
Node predicate,
bool  weak 
)
static

Definition at line 290 of file predtest.c.

292 {
293  PredIterInfoData clause_info;
294  PredIterInfoData pred_info;
295  PredClass pclass;
296  bool result;
297 
298  /* skip through RestrictInfo */
299  Assert(clause != NULL);
300  if (IsA(clause, RestrictInfo))
301  clause = (Node *) ((RestrictInfo *) clause)->clause;
302 
303  pclass = predicate_classify(predicate, &pred_info);
304 
305  switch (predicate_classify(clause, &clause_info))
306  {
307  case CLASS_AND:
308  switch (pclass)
309  {
310  case CLASS_AND:
311 
312  /*
313  * AND-clause => AND-clause if A implies each of B's items
314  */
315  result = true;
316  iterate_begin(pitem, predicate, pred_info)
317  {
318  if (!predicate_implied_by_recurse(clause, pitem,
319  weak))
320  {
321  result = false;
322  break;
323  }
324  }
325  iterate_end(pred_info);
326  return result;
327 
328  case CLASS_OR:
329 
330  /*
331  * AND-clause => OR-clause if A implies any of B's items
332  *
333  * Needed to handle (x AND y) => ((x AND y) OR z)
334  */
335  result = false;
336  iterate_begin(pitem, predicate, pred_info)
337  {
338  if (predicate_implied_by_recurse(clause, pitem,
339  weak))
340  {
341  result = true;
342  break;
343  }
344  }
345  iterate_end(pred_info);
346  if (result)
347  return result;
348 
349  /*
350  * Also check if any of A's items implies B
351  *
352  * Needed to handle ((x OR y) AND z) => (x OR y)
353  */
354  iterate_begin(citem, clause, clause_info)
355  {
356  if (predicate_implied_by_recurse(citem, predicate,
357  weak))
358  {
359  result = true;
360  break;
361  }
362  }
363  iterate_end(clause_info);
364  return result;
365 
366  case CLASS_ATOM:
367 
368  /*
369  * AND-clause => atom if any of A's items implies B
370  */
371  result = false;
372  iterate_begin(citem, clause, clause_info)
373  {
374  if (predicate_implied_by_recurse(citem, predicate,
375  weak))
376  {
377  result = true;
378  break;
379  }
380  }
381  iterate_end(clause_info);
382  return result;
383  }
384  break;
385 
386  case CLASS_OR:
387  switch (pclass)
388  {
389  case CLASS_OR:
390 
391  /*
392  * OR-clause => OR-clause if each of A's items implies any
393  * of B's items. Messy but can't do it any more simply.
394  */
395  result = true;
396  iterate_begin(citem, clause, clause_info)
397  {
398  bool presult = false;
399 
400  iterate_begin(pitem, predicate, pred_info)
401  {
402  if (predicate_implied_by_recurse(citem, pitem,
403  weak))
404  {
405  presult = true;
406  break;
407  }
408  }
409  iterate_end(pred_info);
410  if (!presult)
411  {
412  result = false; /* doesn't imply any of B's */
413  break;
414  }
415  }
416  iterate_end(clause_info);
417  return result;
418 
419  case CLASS_AND:
420  case CLASS_ATOM:
421 
422  /*
423  * OR-clause => AND-clause if each of A's items implies B
424  *
425  * OR-clause => atom if each of A's items implies B
426  */
427  result = true;
428  iterate_begin(citem, clause, clause_info)
429  {
430  if (!predicate_implied_by_recurse(citem, predicate,
431  weak))
432  {
433  result = false;
434  break;
435  }
436  }
437  iterate_end(clause_info);
438  return result;
439  }
440  break;
441 
442  case CLASS_ATOM:
443  switch (pclass)
444  {
445  case CLASS_AND:
446 
447  /*
448  * atom => AND-clause if A implies each of B's items
449  */
450  result = true;
451  iterate_begin(pitem, predicate, pred_info)
452  {
453  if (!predicate_implied_by_recurse(clause, pitem,
454  weak))
455  {
456  result = false;
457  break;
458  }
459  }
460  iterate_end(pred_info);
461  return result;
462 
463  case CLASS_OR:
464 
465  /*
466  * atom => OR-clause if A implies any of B's items
467  */
468  result = false;
469  iterate_begin(pitem, predicate, pred_info)
470  {
471  if (predicate_implied_by_recurse(clause, pitem,
472  weak))
473  {
474  result = true;
475  break;
476  }
477  }
478  iterate_end(pred_info);
479  return result;
480 
481  case CLASS_ATOM:
482 
483  /*
484  * atom => atom is the base case
485  */
486  return
488  clause,
489  weak);
490  }
491  break;
492  }
493 
494  /* can't get here */
495  elog(ERROR, "predicate_classify returned a bogus value");
496  return false;
497 }
#define ERROR
Definition: elog.h:39
#define iterate_end(info)
Definition: predtest.c:78
static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause, bool weak)
Definition: predtest.c:1098
static PredClass predicate_classify(Node *clause, PredIterInfo info)
Definition: predtest.c:826
#define iterate_begin(item, clause, info)
Definition: predtest.c:72

References Assert, CLASS_AND, CLASS_ATOM, CLASS_OR, elog, ERROR, IsA, iterate_begin, iterate_end, predicate_classify(), and predicate_implied_by_simple_clause().

Referenced by predicate_implied_by(), and predicate_refuted_by_recurse().

◆ predicate_implied_by_simple_clause()

static bool predicate_implied_by_simple_clause ( Expr predicate,
Node clause,
bool  weak 
)
static

Definition at line 1098 of file predtest.c.

1100 {
1101  /* Allow interrupting long proof attempts */
1103 
1104  /*
1105  * A simple and general rule is that a clause implies itself, hence we
1106  * check if they are equal(); this works for any kind of expression, and
1107  * for either implication definition. (Actually, there is an implied
1108  * assumption that the functions in the expression are immutable --- but
1109  * this was checked for the predicate by the caller.)
1110  */
1111  if (equal((Node *) predicate, clause))
1112  return true;
1113 
1114  /* Next we have some clause-type-specific strategies */
1115  switch (nodeTag(clause))
1116  {
1117  case T_OpExpr:
1118  {
1119  OpExpr *op = (OpExpr *) clause;
1120 
1121  /*----------
1122  * For boolean x, "x = TRUE" is equivalent to "x", likewise
1123  * "x = FALSE" is equivalent to "NOT x". These can be worth
1124  * checking because, while we preferentially simplify boolean
1125  * comparisons down to "x" and "NOT x", the other form has to
1126  * be dealt with anyway in the context of index conditions.
1127  *
1128  * We could likewise check whether the predicate is boolean
1129  * equality to a constant; but there are no known use-cases
1130  * for that at the moment, assuming that the predicate has
1131  * been through constant-folding.
1132  *----------
1133  */
1134  if (op->opno == BooleanEqualOperator)
1135  {
1136  Node *rightop;
1137 
1138  Assert(list_length(op->args) == 2);
1139  rightop = lsecond(op->args);
1140  /* We might never see null Consts here, but better check */
1141  if (rightop && IsA(rightop, Const) &&
1142  !((Const *) rightop)->constisnull)
1143  {
1144  Node *leftop = linitial(op->args);
1145 
1146  if (DatumGetBool(((Const *) rightop)->constvalue))
1147  {
1148  /* X = true implies X */
1149  if (equal(predicate, leftop))
1150  return true;
1151  }
1152  else
1153  {
1154  /* X = false implies NOT X */
1155  if (is_notclause(predicate) &&
1156  equal(get_notclausearg(predicate), leftop))
1157  return true;
1158  }
1159  }
1160  }
1161  }
1162  break;
1163  default:
1164  break;
1165  }
1166 
1167  /* ... and some predicate-type-specific ones */
1168  switch (nodeTag(predicate))
1169  {
1170  case T_NullTest:
1171  {
1172  NullTest *predntest = (NullTest *) predicate;
1173 
1174  switch (predntest->nulltesttype)
1175  {
1176  case IS_NOT_NULL:
1177 
1178  /*
1179  * If the predicate is of the form "foo IS NOT NULL",
1180  * and we are considering strong implication, we can
1181  * conclude that the predicate is implied if the
1182  * clause is strict for "foo", i.e., it must yield
1183  * false or NULL when "foo" is NULL. In that case
1184  * truth of the clause ensures that "foo" isn't NULL.
1185  * (Again, this is a safe conclusion because "foo"
1186  * must be immutable.) This doesn't work for weak
1187  * implication, though. Also, "row IS NOT NULL" does
1188  * not act in the simple way we have in mind.
1189  */
1190  if (!weak &&
1191  !predntest->argisrow &&
1192  clause_is_strict_for(clause,
1193  (Node *) predntest->arg,
1194  true))
1195  return true;
1196  break;
1197  case IS_NULL:
1198  break;
1199  }
1200  }
1201  break;
1202  default:
1203  break;
1204  }
1205 
1206  /*
1207  * Finally, if both clauses are binary operator expressions, we may be
1208  * able to prove something using the system's knowledge about operators;
1209  * those proof rules are encapsulated in operator_predicate_proof().
1210  */
1211  return operator_predicate_proof(predicate, clause, false, weak);
1212 }
#define CHECK_FOR_INTERRUPTS()
Definition: miscadmin.h:122
static Expr * get_notclausearg(const void *notclause)
Definition: nodeFuncs.h:132
static bool is_notclause(const void *clause)
Definition: nodeFuncs.h:123
#define nodeTag(nodeptr)
Definition: nodes.h:133
static bool operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it, bool weak)
Definition: predtest.c:1779
@ IS_NULL
Definition: primnodes.h:1948
@ IS_NOT_NULL
Definition: primnodes.h:1948
NullTestType nulltesttype
Definition: primnodes.h:1955
Expr * arg
Definition: primnodes.h:1954

References NullTest::arg, OpExpr::args, Assert, CHECK_FOR_INTERRUPTS, clause_is_strict_for(), DatumGetBool(), equal(), get_notclausearg(), IS_NOT_NULL, is_notclause(), IS_NULL, IsA, linitial, list_length(), lsecond, nodeTag, NullTest::nulltesttype, operator_predicate_proof(), and OpExpr::opno.

Referenced by predicate_implied_by_recurse().

◆ predicate_refuted_by()

bool predicate_refuted_by ( List predicate_list,
List clause_list,
bool  weak 
)

Definition at line 222 of file predtest.c.

224 {
225  Node *p,
226  *c;
227 
228  if (predicate_list == NIL)
229  return false; /* no predicate: no refutation is possible */
230  if (clause_list == NIL)
231  return false; /* no restriction: refutation must fail */
232 
233  /*
234  * If either input is a single-element list, replace it with its lone
235  * member; this avoids one useless level of AND-recursion. We only need
236  * to worry about this at top level, since eval_const_expressions should
237  * have gotten rid of any trivial ANDs or ORs below that.
238  */
239  if (list_length(predicate_list) == 1)
240  p = (Node *) linitial(predicate_list);
241  else
242  p = (Node *) predicate_list;
243  if (list_length(clause_list) == 1)
244  c = (Node *) linitial(clause_list);
245  else
246  c = (Node *) clause_list;
247 
248  /* And away we go ... */
249  return predicate_refuted_by_recurse(c, p, weak);
250 }
static bool predicate_refuted_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:531

References linitial, list_length(), NIL, and predicate_refuted_by_recurse().

Referenced by gen_partprune_steps_internal(), relation_excluded_by_constraints(), and test_predtest().

◆ predicate_refuted_by_recurse()

static bool predicate_refuted_by_recurse ( Node clause,
Node predicate,
bool  weak 
)
static

Definition at line 531 of file predtest.c.

533 {
534  PredIterInfoData clause_info;
535  PredIterInfoData pred_info;
536  PredClass pclass;
537  Node *not_arg;
538  bool result;
539 
540  /* skip through RestrictInfo */
541  Assert(clause != NULL);
542  if (IsA(clause, RestrictInfo))
543  clause = (Node *) ((RestrictInfo *) clause)->clause;
544 
545  pclass = predicate_classify(predicate, &pred_info);
546 
547  switch (predicate_classify(clause, &clause_info))
548  {
549  case CLASS_AND:
550  switch (pclass)
551  {
552  case CLASS_AND:
553 
554  /*
555  * AND-clause R=> AND-clause if A refutes any of B's items
556  *
557  * Needed to handle (x AND y) R=> ((!x OR !y) AND z)
558  */
559  result = false;
560  iterate_begin(pitem, predicate, pred_info)
561  {
562  if (predicate_refuted_by_recurse(clause, pitem,
563  weak))
564  {
565  result = true;
566  break;
567  }
568  }
569  iterate_end(pred_info);
570  if (result)
571  return result;
572 
573  /*
574  * Also check if any of A's items refutes B
575  *
576  * Needed to handle ((x OR y) AND z) R=> (!x AND !y)
577  */
578  iterate_begin(citem, clause, clause_info)
579  {
580  if (predicate_refuted_by_recurse(citem, predicate,
581  weak))
582  {
583  result = true;
584  break;
585  }
586  }
587  iterate_end(clause_info);
588  return result;
589 
590  case CLASS_OR:
591 
592  /*
593  * AND-clause R=> OR-clause if A refutes each of B's items
594  */
595  result = true;
596  iterate_begin(pitem, predicate, pred_info)
597  {
598  if (!predicate_refuted_by_recurse(clause, pitem,
599  weak))
600  {
601  result = false;
602  break;
603  }
604  }
605  iterate_end(pred_info);
606  return result;
607 
608  case CLASS_ATOM:
609 
610  /*
611  * If B is a NOT-type clause, A R=> B if A => B's arg
612  *
613  * Since, for either type of refutation, we are starting
614  * with the premise that A is true, we can use a strong
615  * implication test in all cases. That proves B's arg is
616  * true, which is more than we need for weak refutation if
617  * B is a simple NOT, but it allows not worrying about
618  * exactly which kind of negation clause we have.
619  */
620  not_arg = extract_not_arg(predicate);
621  if (not_arg &&
622  predicate_implied_by_recurse(clause, not_arg,
623  false))
624  return true;
625 
626  /*
627  * AND-clause R=> atom if any of A's items refutes B
628  */
629  result = false;
630  iterate_begin(citem, clause, clause_info)
631  {
632  if (predicate_refuted_by_recurse(citem, predicate,
633  weak))
634  {
635  result = true;
636  break;
637  }
638  }
639  iterate_end(clause_info);
640  return result;
641  }
642  break;
643 
644  case CLASS_OR:
645  switch (pclass)
646  {
647  case CLASS_OR:
648 
649  /*
650  * OR-clause R=> OR-clause if A refutes each of B's items
651  */
652  result = true;
653  iterate_begin(pitem, predicate, pred_info)
654  {
655  if (!predicate_refuted_by_recurse(clause, pitem,
656  weak))
657  {
658  result = false;
659  break;
660  }
661  }
662  iterate_end(pred_info);
663  return result;
664 
665  case CLASS_AND:
666 
667  /*
668  * OR-clause R=> AND-clause if each of A's items refutes
669  * any of B's items.
670  */
671  result = true;
672  iterate_begin(citem, clause, clause_info)
673  {
674  bool presult = false;
675 
676  iterate_begin(pitem, predicate, pred_info)
677  {
678  if (predicate_refuted_by_recurse(citem, pitem,
679  weak))
680  {
681  presult = true;
682  break;
683  }
684  }
685  iterate_end(pred_info);
686  if (!presult)
687  {
688  result = false; /* citem refutes nothing */
689  break;
690  }
691  }
692  iterate_end(clause_info);
693  return result;
694 
695  case CLASS_ATOM:
696 
697  /*
698  * If B is a NOT-type clause, A R=> B if A => B's arg
699  *
700  * Same logic as for the AND-clause case above.
701  */
702  not_arg = extract_not_arg(predicate);
703  if (not_arg &&
704  predicate_implied_by_recurse(clause, not_arg,
705  false))
706  return true;
707 
708  /*
709  * OR-clause R=> atom if each of A's items refutes B
710  */
711  result = true;
712  iterate_begin(citem, clause, clause_info)
713  {
714  if (!predicate_refuted_by_recurse(citem, predicate,
715  weak))
716  {
717  result = false;
718  break;
719  }
720  }
721  iterate_end(clause_info);
722  return result;
723  }
724  break;
725 
726  case CLASS_ATOM:
727 
728  /*
729  * If A is a strong NOT-clause, A R=> B if B => A's arg
730  *
731  * Since A is strong, we may assume A's arg is false (not just
732  * not-true). If B weakly implies A's arg, then B can be neither
733  * true nor null, so that strong refutation is proven. If B
734  * strongly implies A's arg, then B cannot be true, so that weak
735  * refutation is proven.
736  */
737  not_arg = extract_strong_not_arg(clause);
738  if (not_arg &&
739  predicate_implied_by_recurse(predicate, not_arg,
740  !weak))
741  return true;
742 
743  switch (pclass)
744  {
745  case CLASS_AND:
746 
747  /*
748  * atom R=> AND-clause if A refutes any of B's items
749  */
750  result = false;
751  iterate_begin(pitem, predicate, pred_info)
752  {
753  if (predicate_refuted_by_recurse(clause, pitem,
754  weak))
755  {
756  result = true;
757  break;
758  }
759  }
760  iterate_end(pred_info);
761  return result;
762 
763  case CLASS_OR:
764 
765  /*
766  * atom R=> OR-clause if A refutes each of B's items
767  */
768  result = true;
769  iterate_begin(pitem, predicate, pred_info)
770  {
771  if (!predicate_refuted_by_recurse(clause, pitem,
772  weak))
773  {
774  result = false;
775  break;
776  }
777  }
778  iterate_end(pred_info);
779  return result;
780 
781  case CLASS_ATOM:
782 
783  /*
784  * If B is a NOT-type clause, A R=> B if A => B's arg
785  *
786  * Same logic as for the AND-clause case above.
787  */
788  not_arg = extract_not_arg(predicate);
789  if (not_arg &&
790  predicate_implied_by_recurse(clause, not_arg,
791  false))
792  return true;
793 
794  /*
795  * atom R=> atom is the base case
796  */
797  return
799  clause,
800  weak);
801  }
802  break;
803  }
804 
805  /* can't get here */
806  elog(ERROR, "predicate_classify returned a bogus value");
807  return false;
808 }
static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, bool weak)
Definition: predtest.c:1225
static Node * extract_strong_not_arg(Node *clause)
Definition: predtest.c:1414
static Node * extract_not_arg(Node *clause)
Definition: predtest.c:1386

References Assert, CLASS_AND, CLASS_ATOM, CLASS_OR, elog, ERROR, extract_not_arg(), extract_strong_not_arg(), IsA, iterate_begin, iterate_end, predicate_classify(), predicate_implied_by_recurse(), and predicate_refuted_by_simple_clause().

Referenced by predicate_refuted_by().

◆ predicate_refuted_by_simple_clause()

static bool predicate_refuted_by_simple_clause ( Expr predicate,
Node clause,
bool  weak 
)
static

Definition at line 1225 of file predtest.c.

1227 {
1228  /* Allow interrupting long proof attempts */
1230 
1231  /*
1232  * A simple clause can't refute itself, so unlike the implication case,
1233  * checking for equal() clauses isn't helpful.
1234  *
1235  * But relation_excluded_by_constraints() checks for self-contradictions
1236  * in a list of clauses, so that we may get here with predicate and clause
1237  * being actually pointer-equal, and that is worth eliminating quickly.
1238  */
1239  if ((Node *) predicate == clause)
1240  return false;
1241 
1242  /* Next we have some clause-type-specific strategies */
1243  switch (nodeTag(clause))
1244  {
1245  case T_NullTest:
1246  {
1247  NullTest *clausentest = (NullTest *) clause;
1248 
1249  /* row IS NULL does not act in the simple way we have in mind */
1250  if (clausentest->argisrow)
1251  return false;
1252 
1253  switch (clausentest->nulltesttype)
1254  {
1255  case IS_NULL:
1256  {
1257  switch (nodeTag(predicate))
1258  {
1259  case T_NullTest:
1260  {
1261  NullTest *predntest = (NullTest *) predicate;
1262 
1263  /*
1264  * row IS NULL does not act in the
1265  * simple way we have in mind
1266  */
1267  if (predntest->argisrow)
1268  return false;
1269 
1270  /*
1271  * foo IS NULL refutes foo IS NOT
1272  * NULL, at least in the non-row case,
1273  * for both strong and weak refutation
1274  */
1275  if (predntest->nulltesttype == IS_NOT_NULL &&
1276  equal(predntest->arg, clausentest->arg))
1277  return true;
1278  }
1279  break;
1280  default:
1281  break;
1282  }
1283 
1284  /*
1285  * foo IS NULL weakly refutes any predicate that
1286  * is strict for foo, since then the predicate
1287  * must yield false or NULL (and since foo appears
1288  * in the predicate, it's known immutable).
1289  */
1290  if (weak &&
1291  clause_is_strict_for((Node *) predicate,
1292  (Node *) clausentest->arg,
1293  true))
1294  return true;
1295 
1296  return false; /* we can't succeed below... */
1297  }
1298  break;
1299  case IS_NOT_NULL:
1300  break;
1301  }
1302  }
1303  break;
1304  default:
1305  break;
1306  }
1307 
1308  /* ... and some predicate-type-specific ones */
1309  switch (nodeTag(predicate))
1310  {
1311  case T_NullTest:
1312  {
1313  NullTest *predntest = (NullTest *) predicate;
1314 
1315  /* row IS NULL does not act in the simple way we have in mind */
1316  if (predntest->argisrow)
1317  return false;
1318 
1319  switch (predntest->nulltesttype)
1320  {
1321  case IS_NULL:
1322  {
1323  switch (nodeTag(clause))
1324  {
1325  case T_NullTest:
1326  {
1327  NullTest *clausentest = (NullTest *) clause;
1328 
1329  /*
1330  * row IS NULL does not act in the
1331  * simple way we have in mind
1332  */
1333  if (clausentest->argisrow)
1334  return false;
1335 
1336  /*
1337  * foo IS NOT NULL refutes foo IS NULL
1338  * for both strong and weak refutation
1339  */
1340  if (clausentest->nulltesttype == IS_NOT_NULL &&
1341  equal(clausentest->arg, predntest->arg))
1342  return true;
1343  }
1344  break;
1345  default:
1346  break;
1347  }
1348 
1349  /*
1350  * When the predicate is of the form "foo IS
1351  * NULL", we can conclude that the predicate is
1352  * refuted if the clause is strict for "foo" (see
1353  * notes for implication case). That works for
1354  * either strong or weak refutation.
1355  */
1356  if (clause_is_strict_for(clause,
1357  (Node *) predntest->arg,
1358  true))
1359  return true;
1360  }
1361  break;
1362  case IS_NOT_NULL:
1363  break;
1364  }
1365 
1366  return false; /* we can't succeed below... */
1367  }
1368  break;
1369  default:
1370  break;
1371  }
1372 
1373  /*
1374  * Finally, if both clauses are binary operator expressions, we may be
1375  * able to prove something using the system's knowledge about operators.
1376  */
1377  return operator_predicate_proof(predicate, clause, true, weak);
1378 }

References NullTest::arg, CHECK_FOR_INTERRUPTS, clause_is_strict_for(), equal(), IS_NOT_NULL, IS_NULL, nodeTag, NullTest::nulltesttype, and operator_predicate_proof().

Referenced by predicate_refuted_by_recurse().

Variable Documentation

◆ BT_implic_table

const StrategyNumber BT_implic_table[6][6]
static
Initial value:
= {
}
#define BTLT
Definition: predtest.c:1662
#define BTGE
Definition: predtest.c:1665
#define none
Definition: predtest.c:1670
#define BTGT
Definition: predtest.c:1666
#define BTLE
Definition: predtest.c:1663
#define BTEQ
Definition: predtest.c:1664

Definition at line 1698 of file predtest.c.

Referenced by lookup_proof_cache().

◆ BT_implies_table

const bool BT_implies_table[6][6]
static
Initial value:
= {
{true, true, none, none, none, true},
{none, true, none, none, none, none},
{none, true, true, true, none, none},
{none, none, none, true, none, none},
{none, none, none, true, true, true},
{none, none, none, none, none, true}
}

Definition at line 1672 of file predtest.c.

Referenced by lookup_proof_cache().

◆ BT_refute_table

const StrategyNumber BT_refute_table[6][6]
static
Initial value:

Definition at line 1711 of file predtest.c.

Referenced by lookup_proof_cache().

◆ BT_refutes_table

const bool BT_refutes_table[6][6]
static
Initial value:
= {
{none, none, true, true, true, none},
{none, none, none, none, true, none},
{true, none, none, none, true, true},
{true, none, none, none, none, none},
{true, true, true, none, none, none},
{none, none, true, none, none, none}
}

Definition at line 1685 of file predtest.c.

Referenced by lookup_proof_cache().

◆ OprProofCacheHash

HTAB* OprProofCacheHash = NULL
static

Definition at line 2093 of file predtest.c.

Referenced by InvalidateOprProofCacheCallBack(), and lookup_proof_cache().