PostgreSQL Source Code  git master
predtest.c File Reference
#include "postgres.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 1527 of file predtest.c.

◆ BTGE

#define BTGE   BTGreaterEqualStrategyNumber

Definition at line 1528 of file predtest.c.

◆ BTGT

#define BTGT   BTGreaterStrategyNumber

Definition at line 1529 of file predtest.c.

◆ BTLE

#define BTLE   BTLessEqualStrategyNumber

Definition at line 1526 of file predtest.c.

◆ BTLT

#define BTLT   BTLessStrategyNumber

Definition at line 1525 of file predtest.c.

◆ BTNE

#define BTNE   ROWCOMPARE_NE

Definition at line 1530 of file predtest.c.

Referenced by lookup_proof_cache().

◆ 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 71 of file predtest.c.

Referenced by predicate_implied_by_recurse(), and predicate_refuted_by_recurse().

◆ iterate_end

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

Definition at line 77 of file predtest.c.

Referenced by predicate_implied_by_recurse(), and predicate_refuted_by_recurse().

◆ MAX_SAOP_ARRAY_SIZE

#define MAX_SAOP_ARRAY_SIZE   100

Definition at line 39 of file predtest.c.

Referenced by predicate_classify().

◆ none

#define none   0

Definition at line 1533 of file predtest.c.

Typedef Documentation

◆ OprProofCacheEntry

◆ OprProofCacheKey

◆ PredIterInfo

typedef struct PredIterInfoData* PredIterInfo

Definition at line 56 of file predtest.c.

◆ PredIterInfoData

Enumeration Type Documentation

◆ PredClass

enum PredClass
Enumerator
CLASS_ATOM 
CLASS_AND 
CLASS_OR 

Definition at line 49 of file predtest.c.

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;
PredClass
Definition: predtest.c:49

Function Documentation

◆ arrayconst_cleanup_fn()

static void arrayconst_cleanup_fn ( PredIterInfo  info)
static

Definition at line 1020 of file predtest.c.

References OpExpr::args, ArrayConstIterState::elem_nulls, ArrayConstIterState::elem_values, list_free(), ArrayConstIterState::opexpr, pfree(), and PredIterInfoData::state.

Referenced by predicate_classify().

1021 {
1023 
1024  pfree(state->elem_values);
1025  pfree(state->elem_nulls);
1026  list_free(state->opexpr.args);
1027  pfree(state);
1028 }
Datum * elem_values
Definition: predtest.c:953
void * state
Definition: predtest.c:61
void pfree(void *pointer)
Definition: mcxt.c:1056
Definition: regguts.h:298
void list_free(List *list)
Definition: list.c:1377
List * args
Definition: primnodes.h:508

◆ arrayconst_next_fn()

static Node * arrayconst_next_fn ( PredIterInfo  info)
static

Definition at line 1007 of file predtest.c.

References ArrayConstIterState::constexpr, Const::constisnull, Const::constvalue, ArrayConstIterState::elem_nulls, ArrayConstIterState::elem_values, ArrayConstIterState::next_elem, ArrayConstIterState::num_elems, ArrayConstIterState::opexpr, and PredIterInfoData::state.

Referenced by predicate_classify().

1008 {
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 }
Datum constvalue
Definition: primnodes.h:200
Datum * elem_values
Definition: predtest.c:953
Definition: nodes.h:525
void * state
Definition: predtest.c:61
Definition: regguts.h:298
bool constisnull
Definition: primnodes.h:201

◆ arrayconst_startup_fn()

static void arrayconst_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 958 of file predtest.c.

References OpExpr::args, ScalarArrayOpExpr::args, ARR_ELEMTYPE, Const::constbyval, Const::constcollid, ArrayConstIterState::constexpr, Const::constlen, Const::consttype, Const::consttypmod, Const::constvalue, DatumGetArrayTypeP, deconstruct_array(), ArrayConstIterState::elem_nulls, ArrayConstIterState::elem_values, get_typlenbyvalalign(), OpExpr::inputcollid, ScalarArrayOpExpr::inputcollid, InvalidOid, list_copy(), lsecond, ArrayConstIterState::next_elem, ArrayConstIterState::num_elems, OpExpr::opcollid, ArrayConstIterState::opexpr, OpExpr::opfuncid, ScalarArrayOpExpr::opfuncid, OpExpr::opno, ScalarArrayOpExpr::opno, OpExpr::opresulttype, OpExpr::opretset, palloc(), PredIterInfoData::state, T_Const, T_OpExpr, Expr::type, Const::xpr, and OpExpr::xpr.

Referenced by predicate_classify().

959 {
960  ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
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);
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 }
Datum constvalue
Definition: primnodes.h:200
signed short int16
Definition: c.h:346
bool constbyval
Definition: primnodes.h:203
void get_typlenbyvalalign(Oid typid, int16 *typlen, bool *typbyval, char *typalign)
Definition: lsyscache.c:2049
Datum * elem_values
Definition: predtest.c:953
List * list_copy(const List *oldlist)
Definition: list.c:1404
void * state
Definition: predtest.c:61
#define lsecond(l)
Definition: pg_list.h:200
int constlen
Definition: primnodes.h:199
Expr xpr
Definition: primnodes.h:501
Oid consttype
Definition: primnodes.h:196
Oid opresulttype
Definition: primnodes.h:504
Oid constcollid
Definition: primnodes.h:198
Expr xpr
Definition: primnodes.h:195
Oid opcollid
Definition: primnodes.h:506
Definition: nodes.h:152
Oid opfuncid
Definition: primnodes.h:503
#define InvalidOid
Definition: postgres_ext.h:36
Definition: regguts.h:298
Oid inputcollid
Definition: primnodes.h:507
int32 consttypmod
Definition: primnodes.h:197
void deconstruct_array(ArrayType *array, Oid elmtype, int elmlen, bool elmbyval, char elmalign, Datum **elemsp, bool **nullsp, int *nelemsp)
Definition: arrayfuncs.c:3461
void * palloc(Size size)
Definition: mcxt.c:949
NodeTag type
Definition: primnodes.h:138
Oid opno
Definition: primnodes.h:502
List * args
Definition: primnodes.h:508
#define ARR_ELEMTYPE(a)
Definition: array.h:280
bool opretset
Definition: primnodes.h:505
#define DatumGetArrayTypeP(X)
Definition: array.h:249

◆ arrayexpr_cleanup_fn()

static void arrayexpr_cleanup_fn ( PredIterInfo  info)
static

Definition at line 1080 of file predtest.c.

References OpExpr::args, list_free(), ArrayExprIterState::opexpr, pfree(), and PredIterInfoData::state.

Referenced by predicate_classify().

1081 {
1083 
1084  list_free(state->opexpr.args);
1085  pfree(state);
1086 }
void * state
Definition: predtest.c:61
void pfree(void *pointer)
Definition: mcxt.c:1056
Definition: regguts.h:298
void list_free(List *list)
Definition: list.c:1377
List * args
Definition: primnodes.h:508

◆ arrayexpr_next_fn()

static Node * arrayexpr_next_fn ( PredIterInfo  info)
static

Definition at line 1068 of file predtest.c.

References OpExpr::args, lfirst, lnext(), lsecond, ArrayExprIterState::next, ArrayExprIterState::opexpr, PredIterInfoData::state, and PredIterInfoData::state_list.

Referenced by predicate_classify().

1069 {
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 }
static ListCell * lnext(const List *l, const ListCell *c)
Definition: pg_list.h:321
Definition: nodes.h:525
void * state
Definition: predtest.c:61
#define lsecond(l)
Definition: pg_list.h:200
#define lfirst(lc)
Definition: pg_list.h:190
Definition: regguts.h:298
ListCell * next
Definition: predtest.c:1037
List * args
Definition: primnodes.h:508
List * state_list
Definition: predtest.c:62

◆ arrayexpr_startup_fn()

static void arrayexpr_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 1041 of file predtest.c.

References OpExpr::args, ScalarArrayOpExpr::args, ArrayExpr::elements, OpExpr::inputcollid, ScalarArrayOpExpr::inputcollid, InvalidOid, list_copy(), list_head(), lsecond, ArrayExprIterState::next, OpExpr::opcollid, ArrayExprIterState::opexpr, OpExpr::opfuncid, ScalarArrayOpExpr::opfuncid, OpExpr::opno, ScalarArrayOpExpr::opno, OpExpr::opresulttype, OpExpr::opretset, palloc(), PredIterInfoData::state, PredIterInfoData::state_list, T_OpExpr, Expr::type, and OpExpr::xpr.

Referenced by predicate_classify().

1042 {
1043  ScalarArrayOpExpr *saop = (ScalarArrayOpExpr *) clause;
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 }
List * list_copy(const List *oldlist)
Definition: list.c:1404
void * state
Definition: predtest.c:61
#define lsecond(l)
Definition: pg_list.h:200
Expr xpr
Definition: primnodes.h:501
Oid opresulttype
Definition: primnodes.h:504
static ListCell * list_head(const List *l)
Definition: pg_list.h:125
List * elements
Definition: primnodes.h:977
Oid opcollid
Definition: primnodes.h:506
Oid opfuncid
Definition: primnodes.h:503
#define InvalidOid
Definition: postgres_ext.h:36
Definition: regguts.h:298
ListCell * next
Definition: predtest.c:1037
Oid inputcollid
Definition: primnodes.h:507
void * palloc(Size size)
Definition: mcxt.c:949
NodeTag type
Definition: primnodes.h:138
Oid opno
Definition: primnodes.h:502
List * args
Definition: primnodes.h:508
List * state_list
Definition: predtest.c:62
bool opretset
Definition: primnodes.h:505

◆ boolexpr_startup_fn()

static void boolexpr_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 937 of file predtest.c.

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

Referenced by predicate_classify().

938 {
939  info->state_list = ((BoolExpr *) clause)->args;
940  info->state = (void *) list_head(info->state_list);
941 }
void * state
Definition: predtest.c:61
static ListCell * list_head(const List *l)
Definition: pg_list.h:125
List * state_list
Definition: predtest.c:62

◆ clause_is_strict_for()

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

Definition at line 1323 of file predtest.c.

References arg, ScalarArrayOpExpr::args, ARR_DIMS, ARR_NDIM, ArrayGetNItems(), Const::constisnull, Const::constvalue, 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().

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 }
Datum constvalue
Definition: primnodes.h:200
bool op_strict(Oid opno)
Definition: lsyscache.c:1279
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
bool equal(const void *a, const void *b)
Definition: equalfuncs.c:3011
static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
Definition: predtest.c:1323
int ArrayGetNItems(int ndim, const int *dims)
Definition: arrayutils.c:75
Definition: nodes.h:525
#define lsecond(l)
Definition: pg_list.h:200
static bool is_funcclause(const void *clause)
Definition: nodeFuncs.h:56
#define linitial(l)
Definition: pg_list.h:195
#define ARR_DIMS(a)
Definition: array.h:282
#define lfirst(lc)
Definition: pg_list.h:190
static int list_length(const List *l)
Definition: pg_list.h:169
#define ARR_NDIM(a)
Definition: array.h:278
bool func_strict(Oid funcid)
Definition: lsyscache.c:1563
void * arg
static bool is_opclause(const void *clause)
Definition: nodeFuncs.h:63
bool constisnull
Definition: primnodes.h:201
#define DatumGetArrayTypeP(X)
Definition: array.h:249

◆ extract_not_arg()

static Node * extract_not_arg ( Node clause)
static

Definition at line 1249 of file predtest.c.

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().

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 }
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
Definition: nodes.h:525
#define linitial(l)
Definition: pg_list.h:195
BoolExprType boolop
Definition: primnodes.h:568
Expr * arg
Definition: primnodes.h:1228
BoolTestType booltesttype
Definition: primnodes.h:1229
List * args
Definition: primnodes.h:569

◆ extract_strong_not_arg()

static Node * extract_strong_not_arg ( Node clause)
static

Definition at line 1277 of file predtest.c.

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

Referenced by predicate_refuted_by_recurse().

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 }
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
Definition: nodes.h:525
#define linitial(l)
Definition: pg_list.h:195
BoolExprType boolop
Definition: primnodes.h:568
Expr * arg
Definition: primnodes.h:1228
BoolTestType booltesttype
Definition: primnodes.h:1229
List * args
Definition: primnodes.h:569

◆ get_btree_test_op()

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

Definition at line 2194 of file predtest.c.

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

Referenced by operator_predicate_proof().

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 }
static OprProofCacheEntry * lookup_proof_cache(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:1964

◆ InvalidateOprProofCacheCallBack()

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

Definition at line 2210 of file predtest.c.

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

Referenced by lookup_proof_cache().

2211 {
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 }
static HTAB * OprProofCacheHash
Definition: predtest.c:1956
#define Assert(condition)
Definition: c.h:739
void * hash_seq_search(HASH_SEQ_STATUS *status)
Definition: dynahash.c:1389
void hash_seq_init(HASH_SEQ_STATUS *status, HTAB *hashp)
Definition: dynahash.c:1379
static void static void status(const char *fmt,...) pg_attribute_printf(1
Definition: pg_regress.c:226

◆ list_cleanup_fn()

static void list_cleanup_fn ( PredIterInfo  info)
static

Definition at line 927 of file predtest.c.

Referenced by predicate_classify().

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

◆ list_next_fn()

static Node * list_next_fn ( PredIterInfo  info)
static

Definition at line 914 of file predtest.c.

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

Referenced by predicate_classify().

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 }
static ListCell * lnext(const List *l, const ListCell *c)
Definition: pg_list.h:321
Definition: nodes.h:525
void * state
Definition: predtest.c:61
#define lfirst(lc)
Definition: pg_list.h:190
List * state_list
Definition: predtest.c:62

◆ list_startup_fn()

static void list_startup_fn ( Node clause,
PredIterInfo  info 
)
static

Definition at line 907 of file predtest.c.

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

Referenced by predicate_classify().

908 {
909  info->state_list = (List *) clause;
910  info->state = (void *) list_head(info->state_list);
911 }
void * state
Definition: predtest.c:61
static ListCell * list_head(const List *l)
Definition: pg_list.h:125
Definition: pg_list.h:50
List * state_list
Definition: predtest.c:62

◆ lookup_proof_cache()

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

Definition at line 1964 of file predtest.c.

References AMOPOPID, Assert, BT_implic_table, BT_implies_table, BT_refute_table, BT_refutes_table, BTEqualStrategyNumber, BTNE, CacheRegisterSyscacheCallback(), OprProofCacheKey::clause_op, HASHCTL::entrysize, 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, HASHCTL::keysize, lfirst, list_free_deep(), MemSet, NIL, OidIsValid, op_volatile(), OpBtreeInterpretation::opfamily_id, OpBtreeInterpretation::oplefttype, OpBtreeInterpretation::oprighttype, OprProofCacheKey::pred_op, 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().

1965 {
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 */
1994  (Datum) 0);
1995  }
1996 
1997  key.pred_op = pred_op;
1998  key.clause_op = clause_op;
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,
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 }
#define NIL
Definition: pg_list.h:65
bool same_subexprs_implies
Definition: predtest.c:1950
#define HASH_ELEM
Definition: hsearch.h:87
static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, uint32 hashvalue)
Definition: predtest.c:2210
Size entrysize
Definition: hsearch.h:73
struct OprProofCacheEntry OprProofCacheEntry
uint16 StrategyNumber
Definition: stratnum.h:22
#define MemSet(start, val, len)
Definition: c.h:962
static const bool BT_refutes_table[6][6]
Definition: predtest.c:1548
void * hash_search(HTAB *hashp, const void *keyPtr, HASHACTION action, bool *foundPtr)
Definition: dynahash.c:906
unsigned int Oid
Definition: postgres_ext.h:31
#define OidIsValid(objectId)
Definition: c.h:645
void list_free_deep(List *list)
Definition: list.c:1391
bool same_subexprs_refutes
Definition: predtest.c:1951
static HTAB * OprProofCacheHash
Definition: predtest.c:1956
static const StrategyNumber BT_refute_table[6][6]
Definition: predtest.c:1574
static const StrategyNumber BT_implic_table[6][6]
Definition: predtest.c:1561
Oid get_opfamily_member(Oid opfamily, Oid lefttype, Oid righttype, int16 strategy)
Definition: lsyscache.c:163
#define BTNE
Definition: predtest.c:1530
struct OprProofCacheKey OprProofCacheKey
#define HASH_BLOBS
Definition: hsearch.h:88
char op_volatile(Oid opno)
Definition: lsyscache.c:1295
void CacheRegisterSyscacheCallback(int cacheid, SyscacheCallbackFunction func, Datum arg)
Definition: inval.c:1426
List * get_op_btree_interpretation(Oid opno)
Definition: lsyscache.c:598
uintptr_t Datum
Definition: postgres.h:367
HTAB * hash_create(const char *tabname, long nelem, HASHCTL *info, int flags)
Definition: dynahash.c:316
Size keysize
Definition: hsearch.h:72
#define InvalidOid
Definition: postgres_ext.h:36
#define Assert(condition)
Definition: c.h:739
#define lfirst(lc)
Definition: pg_list.h:190
Oid get_negator(Oid opno)
Definition: lsyscache.c:1335
Definition: pg_list.h:50
#define BTEqualStrategyNumber
Definition: stratnum.h:31
static const bool BT_implies_table[6][6]
Definition: predtest.c:1535

◆ operator_predicate_proof()

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

Definition at line 1642 of file predtest.c.

References OpExpr::args, Const::constisnull, CreateExecutorState(), DatumGetBool, DEBUG2, elog, equal(), EState::es_query_cxt, ExecEvalExprSwitchContext(), ExecInitExpr(), fix_opfuncids(), FreeExecutorState(), get_btree_test_op(), get_commutator(), GetPerTupleExprContext, OpExpr::inputcollid, 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().

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 }
static Oid get_btree_test_op(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:2194
bool op_strict(Oid opno)
Definition: lsyscache.c:1279
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
static Datum ExecEvalExprSwitchContext(ExprState *state, ExprContext *econtext, bool *isNull)
Definition: executor.h:300
Oid get_commutator(Oid opno)
Definition: lsyscache.c:1311
bool equal(const void *a, const void *b)
Definition: equalfuncs.c:3011
void fix_opfuncids(Node *node)
Definition: nodeFuncs.c:1587
static MemoryContext MemoryContextSwitchTo(MemoryContext context)
Definition: palloc.h:109
Definition: nodes.h:525
unsigned int Oid
Definition: postgres_ext.h:31
#define OidIsValid(objectId)
Definition: c.h:645
Expr * make_opclause(Oid opno, Oid opresulttype, bool opretset, Expr *leftop, Expr *rightop, Oid opcollid, Oid inputcollid)
Definition: makefuncs.c:607
#define lsecond(l)
Definition: pg_list.h:200
void FreeExecutorState(EState *estate)
Definition: execUtils.c:190
#define GetPerTupleExprContext(estate)
Definition: executor.h:501
static bool operator_same_subexprs_proof(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:1895
MemoryContext es_query_cxt
Definition: execnodes.h:549
#define linitial(l)
Definition: pg_list.h:195
#define DEBUG2
Definition: elog.h:24
#define DatumGetBool(X)
Definition: postgres.h:393
EState * CreateExecutorState(void)
Definition: execUtils.c:88
uintptr_t Datum
Definition: postgres.h:367
#define InvalidOid
Definition: postgres_ext.h:36
static int list_length(const List *l)
Definition: pg_list.h:169
Oid inputcollid
Definition: primnodes.h:507
#define elog(elevel,...)
Definition: elog.h:228
ExprState * ExecInitExpr(Expr *node, PlanState *parent)
Definition: execExpr.c:121
Oid opno
Definition: primnodes.h:502
static bool is_opclause(const void *clause)
Definition: nodeFuncs.h:63
List * args
Definition: primnodes.h:508
bool constisnull
Definition: primnodes.h:201

◆ operator_same_subexprs_lookup()

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

Definition at line 2169 of file predtest.c.

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

Referenced by operator_same_subexprs_proof().

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 }
bool same_subexprs_implies
Definition: predtest.c:1950
static OprProofCacheEntry * lookup_proof_cache(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:1964
bool same_subexprs_refutes
Definition: predtest.c:1951

◆ operator_same_subexprs_proof()

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

Definition at line 1895 of file predtest.c.

References get_negator(), and operator_same_subexprs_lookup().

Referenced by operator_predicate_proof().

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 }
static bool operator_same_subexprs_lookup(Oid pred_op, Oid clause_op, bool refute_it)
Definition: predtest.c:2169
Oid get_negator(Oid opno)
Definition: lsyscache.c:1335

◆ predicate_classify()

static PredClass predicate_classify ( Node clause,
PredIterInfo  info 
)
static

Definition at line 825 of file predtest.c.

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().

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  {
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  {
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  {
882  info->next_fn = arrayconst_next_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  {
892  info->next_fn = arrayexpr_next_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 }
static Node * arrayexpr_next_fn(PredIterInfo info)
Definition: predtest.c:1068
Node *(* next_fn)(PredIterInfo info)
Definition: predtest.c:66
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
static void arrayexpr_cleanup_fn(PredIterInfo info)
Definition: predtest.c:1080
#define MAX_SAOP_ARRAY_SIZE
Definition: predtest.c:39
static bool is_orclause(const void *clause)
Definition: nodeFuncs.h:103
void(* startup_fn)(Node *clause, PredIterInfo info)
Definition: predtest.c:64
int ArrayGetNItems(int ndim, const int *dims)
Definition: arrayutils.c:75
static bool is_andclause(const void *clause)
Definition: nodeFuncs.h:94
Definition: nodes.h:525
static void arrayconst_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:958
void(* cleanup_fn)(PredIterInfo info)
Definition: predtest.c:68
static void arrayexpr_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:1041
#define lsecond(l)
Definition: pg_list.h:200
#define ARR_DIMS(a)
Definition: array.h:282
static Node * arrayconst_next_fn(PredIterInfo info)
Definition: predtest.c:1007
static void list_cleanup_fn(PredIterInfo info)
Definition: predtest.c:927
static void list_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:907
#define Assert(condition)
Definition: c.h:739
static Node * list_next_fn(PredIterInfo info)
Definition: predtest.c:914
static int list_length(const List *l)
Definition: pg_list.h:169
#define ARR_NDIM(a)
Definition: array.h:278
static void boolexpr_startup_fn(Node *clause, PredIterInfo info)
Definition: predtest.c:937
Definition: pg_list.h:50
static void arrayconst_cleanup_fn(PredIterInfo info)
Definition: predtest.c:1020
#define DatumGetArrayTypeP(X)
Definition: array.h:249

◆ predicate_implied_by()

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

Definition at line 151 of file predtest.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().

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 }
#define NIL
Definition: pg_list.h:65
Definition: nodes.h:525
#define linitial(l)
Definition: pg_list.h:195
char * c
static int list_length(const List *l)
Definition: pg_list.h:169
static bool predicate_implied_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:289

◆ predicate_implied_by_recurse()

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

Definition at line 289 of file predtest.c.

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().

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
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 }
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
#define iterate_begin(item, clause, info)
Definition: predtest.c:71
Definition: nodes.h:525
static PredClass predicate_classify(Node *clause, PredIterInfo info)
Definition: predtest.c:825
static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause, bool weak)
Definition: predtest.c:1117
PredClass
Definition: predtest.c:49
#define ERROR
Definition: elog.h:43
#define Assert(condition)
Definition: c.h:739
static bool predicate_implied_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:289
#define elog(elevel,...)
Definition: elog.h:228
#define iterate_end(info)
Definition: predtest.c:77

◆ predicate_implied_by_simple_clause()

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

Definition at line 1117 of file predtest.c.

References NullTest::arg, NullTest::argisrow, CHECK_FOR_INTERRUPTS, clause_is_strict_for(), equal(), IS_NOT_NULL, IsA, NullTest::nulltesttype, and operator_predicate_proof().

Referenced by predicate_implied_by_recurse().

1119 {
1120  /* Allow interrupting long proof attempts */
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 }
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
bool equal(const void *a, const void *b)
Definition: equalfuncs.c:3011
static bool operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it, bool weak)
Definition: predtest.c:1642
static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
Definition: predtest.c:1323
Definition: nodes.h:525
Expr * arg
Definition: primnodes.h:1205
NullTestType nulltesttype
Definition: primnodes.h:1206
bool argisrow
Definition: primnodes.h:1207
#define CHECK_FOR_INTERRUPTS()
Definition: miscadmin.h:99

◆ predicate_refuted_by()

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

Definition at line 221 of file predtest.c.

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

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

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 }
#define NIL
Definition: pg_list.h:65
Definition: nodes.h:525
#define linitial(l)
Definition: pg_list.h:195
char * c
static bool predicate_refuted_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:530
static int list_length(const List *l)
Definition: pg_list.h:169

◆ predicate_refuted_by_recurse()

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

Definition at line 530 of file predtest.c.

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().

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
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 }
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
#define iterate_begin(item, clause, info)
Definition: predtest.c:71
Definition: nodes.h:525
static PredClass predicate_classify(Node *clause, PredIterInfo info)
Definition: predtest.c:825
PredClass
Definition: predtest.c:49
#define ERROR
Definition: elog.h:43
static Node * extract_strong_not_arg(Node *clause)
Definition: predtest.c:1277
static bool predicate_refuted_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:530
static Node * extract_not_arg(Node *clause)
Definition: predtest.c:1249
static bool predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, bool weak)
Definition: predtest.c:1179
#define Assert(condition)
Definition: c.h:739
static bool predicate_implied_by_recurse(Node *clause, Node *predicate, bool weak)
Definition: predtest.c:289
#define elog(elevel,...)
Definition: elog.h:228
#define iterate_end(info)
Definition: predtest.c:77

◆ predicate_refuted_by_simple_clause()

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

Definition at line 1179 of file predtest.c.

References arg, CHECK_FOR_INTERRUPTS, clause_is_strict_for(), equal(), IS_NOT_NULL, IS_NULL, IsA, and operator_predicate_proof().

Referenced by predicate_refuted_by_recurse().

1181 {
1182  /* Allow interrupting long proof attempts */
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 }
#define IsA(nodeptr, _type_)
Definition: nodes.h:576
bool equal(const void *a, const void *b)
Definition: equalfuncs.c:3011
static bool operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it, bool weak)
Definition: predtest.c:1642
static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
Definition: predtest.c:1323
Definition: nodes.h:525
void * arg
#define CHECK_FOR_INTERRUPTS()
Definition: miscadmin.h:99

Variable Documentation

◆ BT_implic_table

const StrategyNumber BT_implic_table[6][6]
static
Initial value:
= {
{BTGE, BTGE, none, none, none, BTGE},
{none, none, none, BTLE, BTLT, BTLT},
{none, none, none, BTLE, BTLE, BTLE},
}
#define none
Definition: predtest.c:1533
#define BTGT
Definition: predtest.c:1529
#define BTLT
Definition: predtest.c:1525
#define BTGE
Definition: predtest.c:1528
#define BTEQ
Definition: predtest.c:1527
#define BTNE
Definition: predtest.c:1530
#define BTLE
Definition: predtest.c:1526

Definition at line 1561 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}
}
#define none
Definition: predtest.c:1533

Definition at line 1535 of file predtest.c.

Referenced by lookup_proof_cache().

◆ BT_refute_table

const StrategyNumber BT_refute_table[6][6]
static
Initial value:
= {
{none, none, BTGE, BTGE, BTGE, none},
{none, none, BTGT, BTGT, BTGE, none},
{BTLE, BTLT, BTLT, none, none, none},
{BTLE, BTLE, BTLE, none, none, none},
{none, none, BTEQ, none, none, none}
}
#define none
Definition: predtest.c:1533
#define BTGT
Definition: predtest.c:1529
#define BTLT
Definition: predtest.c:1525
#define BTGE
Definition: predtest.c:1528
#define BTEQ
Definition: predtest.c:1527
#define BTNE
Definition: predtest.c:1530
#define BTLE
Definition: predtest.c:1526

Definition at line 1574 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}
}
#define none
Definition: predtest.c:1533

Definition at line 1548 of file predtest.c.

Referenced by lookup_proof_cache().

◆ OprProofCacheHash

HTAB* OprProofCacheHash = NULL
static

Definition at line 1956 of file predtest.c.