PostgreSQL Source Code git master
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Macros Pages
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 RCLT   COMPARE_LT
 
#define RCLE   COMPARE_LE
 
#define RCEQ   COMPARE_EQ
 
#define RCGE   COMPARE_GE
 
#define RCGT   COMPARE_GT
 
#define RCNE   COMPARE_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 RC_implies_table [6][6]
 
static const bool RC_refutes_table [6][6]
 
static const CompareType RC_implic_table [6][6]
 
static const CompareType RC_refute_table [6][6]
 
static HTABOprProofCacheHash = NULL
 

Macro Definition Documentation

◆ 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.

◆ RCEQ

#define RCEQ   COMPARE_EQ

Definition at line 1664 of file predtest.c.

◆ RCGE

#define RCGE   COMPARE_GE

Definition at line 1665 of file predtest.c.

◆ RCGT

#define RCGT   COMPARE_GT

Definition at line 1666 of file predtest.c.

◆ RCLE

#define RCLE   COMPARE_LE

Definition at line 1663 of file predtest.c.

◆ RCLT

#define RCLT   COMPARE_LT

Definition at line 1662 of file predtest.c.

◆ RCNE

#define RCNE   COMPARE_NE

Definition at line 1667 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:2147
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->const_expr.constvalue = state->elem_values[state->next_elem];
1015 state->const_expr.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:81
Definition: nodes.h:135

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 = 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->const_expr.xpr.type = T_Const;
996 state->const_expr.consttype = ARR_ELEMTYPE(arrayval);
997 state->const_expr.consttypmod = -1;
998 state->const_expr.constcollid = arrayconst->constcollid;
999 state->const_expr.constlen = elmlen;
1000 state->const_expr.constbyval = elmbyval;
1001 lsecond(state->opexpr.args) = &state->const_expr;
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:3631
int16_t int16
Definition: c.h:497
List * list_copy(const List *oldlist)
Definition: list.c:1573
void get_typlenbyvalalign(Oid typid, int16 *typlen, bool *typbyval, char *typalign)
Definition: lsyscache.c:2411
void * palloc(Size size)
Definition: mcxt.c:1940
#define lsecond(l)
Definition: pg_list.h:183
#define InvalidOid
Definition: postgres_ext.h:35

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 = 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

References ScalarArrayOpExpr::args, 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 = 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:1617
bool func_strict(Oid funcid)
Definition: lsyscache.c:1901
static bool is_opclause(const void *clause)
Definition: nodeFuncs.h:76
static bool is_funcclause(const void *clause)
Definition: nodeFuncs.h:69
#define IsA(nodeptr, _type_)
Definition: nodes.h:164
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(), clause_is_strict_for(), DatumGetArrayTypeP, equal(), func_strict(), is_funcclause(), is_opclause(), IsA, lfirst, linitial, list_length(), lsecond, op_strict(), ScalarArrayOpExpr::opno, and ScalarArrayOpExpr::useOr.

Referenced by clause_is_strict_for(), 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:1981
@ IS_UNKNOWN
Definition: primnodes.h:1981
@ IS_FALSE
Definition: primnodes.h:1981
@ NOT_EXPR
Definition: primnodes.h:948
BoolExprType boolop
Definition: primnodes.h:956
List * args
Definition: primnodes.h:957
BoolTestType booltesttype
Definition: primnodes.h:1988
Expr * arg
Definition: primnodes.h:1987

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 ... */
2355
2356 while ((hentry = (OprProofCacheEntry *) hash_seq_search(&status)) != NULL)
2357 {
2358 hentry->have_implic = false;
2359 hentry->have_refute = false;
2360 }
2361}
void * hash_seq_search(HASH_SEQ_STATUS *status)
Definition: dynahash.c:1420
void hash_seq_init(HASH_SEQ_STATUS *status, HTAB *hashp)
Definition: dynahash.c:1385
Assert(PointerIsAligned(start, uint64))
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 = 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 = 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,
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_index_interpretation(clause_op);
2169 if (clause_op_infos)
2170 pred_op_infos = get_op_index_interpretation(pred_op);
2171 else /* no point in looking */
2172 pred_op_infos = NIL;
2173
2174 foreach(lcp, pred_op_infos)
2175 {
2176 OpIndexInterpretation *pred_op_info = lfirst(lcp);
2177 Oid opfamily_id = pred_op_info->opfamily_id;
2178
2179 foreach(lcc, clause_op_infos)
2180 {
2181 OpIndexInterpretation *clause_op_info = lfirst(lcc);
2182 CompareType pred_cmptype,
2183 clause_cmptype,
2184 test_cmptype;
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_cmptype = pred_op_info->cmptype;
2193 clause_cmptype = clause_op_info->cmptype;
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 |= RC_refutes_table[clause_cmptype - 1][pred_cmptype - 1];
2201 else
2202 same_subexprs |= RC_implies_table[clause_cmptype - 1][pred_cmptype - 1];
2203
2204 /*
2205 * Look up the "test" cmptype number in the implication table
2206 */
2207 if (refute_it)
2208 test_cmptype = RC_refute_table[clause_cmptype - 1][pred_cmptype - 1];
2209 else
2210 test_cmptype = RC_implic_table[clause_cmptype - 1][pred_cmptype - 1];
2211
2212 if (test_cmptype == 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 cmptype and the
2220 * datatypes.
2221 */
2222 if (test_cmptype == RCNE)
2223 {
2224 test_op = get_opfamily_member_for_cmptype(opfamily_id,
2225 pred_op_info->oprighttype,
2226 clause_op_info->oprighttype,
2227 COMPARE_EQ);
2228 if (OidIsValid(test_op))
2229 test_op = get_negator(test_op);
2230 }
2231 else
2232 {
2233 test_op = get_opfamily_member_for_cmptype(opfamily_id,
2234 pred_op_info->oprighttype,
2235 clause_op_info->oprighttype,
2236 test_cmptype);
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:746
CompareType
Definition: cmptype.h:32
@ COMPARE_EQ
Definition: cmptype.h:36
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:1802
void list_free_deep(List *list)
Definition: list.c:1560
Oid get_opfamily_member_for_cmptype(Oid opfamily, Oid lefttype, Oid righttype, CompareType cmptype)
Definition: lsyscache.c:196
List * get_op_index_interpretation(Oid opno)
Definition: lsyscache.c:672
char op_volatile(Oid opno)
Definition: lsyscache.c:1633
Oid get_negator(Oid opno)
Definition: lsyscache.c:1673
#define NIL
Definition: pg_list.h:68
uintptr_t Datum
Definition: postgres.h:69
unsigned int Oid
Definition: postgres_ext.h:30
static const CompareType RC_implic_table[6][6]
Definition: predtest.c:1698
static void InvalidateOprProofCacheCallBack(Datum arg, int cacheid, uint32 hashvalue)
Definition: predtest.c:2346
static const bool RC_refutes_table[6][6]
Definition: predtest.c:1685
static const bool RC_implies_table[6][6]
Definition: predtest.c:1672
struct OprProofCacheEntry OprProofCacheEntry
#define RCNE
Definition: predtest.c:1667
struct OprProofCacheKey OprProofCacheKey
static const CompareType RC_refute_table[6][6]
Definition: predtest.c:1711
tree ctl
Definition: radixtree.h:1838
CompareType cmptype
Definition: lsyscache.h:28
bool same_subexprs_refutes
Definition: predtest.c:2088
bool same_subexprs_implies
Definition: predtest.c:2087

References Assert(), CacheRegisterSyscacheCallback(), OpIndexInterpretation::cmptype, COMPARE_EQ, ctl, get_negator(), get_op_index_interpretation(), get_opfamily_member_for_cmptype(), 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(), OpIndexInterpretation::opfamily_id, OpIndexInterpretation::oplefttype, OpIndexInterpretation::oprighttype, OprProofCacheHash, RC_implic_table, RC_implies_table, RC_refute_table, RC_refutes_table, RCNE, OprProofCacheEntry::refute_test_op, OprProofCacheEntry::same_subexprs_implies, and OprProofCacheEntry::same_subexprs_refutes.

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:226
ExprState * ExecInitExpr(Expr *node, PlanState *parent)
Definition: execExpr.c:143
void FreeExecutorState(EState *estate)
Definition: execUtils.c:193
EState * CreateExecutorState(void)
Definition: execUtils.c:88
#define GetPerTupleExprContext(estate)
Definition: executor.h:678
static Datum ExecEvalExprSwitchContext(ExprState *state, ExprContext *econtext, bool *isNull)
Definition: executor.h:458
Oid get_commutator(Oid opno)
Definition: lsyscache.c:1649
Expr * make_opclause(Oid opno, Oid opresulttype, bool opretset, Expr *leftop, Expr *rightop, Oid opcollid, Oid inputcollid)
Definition: makefuncs.c:701
void fix_opfuncids(Node *node)
Definition: nodeFuncs.c:1841
static MemoryContext MemoryContextSwitchTo(MemoryContext context)
Definition: palloc.h:124
static bool DatumGetBool(Datum X)
Definition: postgres.h:95
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
MemoryContext es_query_cxt
Definition: execnodes.h:708
Oid opno
Definition: primnodes.h:835
List * args
Definition: primnodes.h:853

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 {
839 info->next_fn = list_next_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;
850 return CLASS_AND;
851 }
852 if (is_orclause(clause))
853 {
855 info->next_fn = list_next_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 {
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 {
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:107
static bool is_orclause(const void *clause)
Definition: nodeFuncs.h:116
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(), predicate_implied_by_recurse(), and predicate_implied_by_simple_clause().

Referenced by predicate_implied_by(), predicate_implied_by_recurse(), 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:123
static bool is_notclause(const void *clause)
Definition: nodeFuncs.h:125
static Expr * get_notclausearg(const void *notclause)
Definition: nodeFuncs.h:134
#define nodeTag(nodeptr)
Definition: nodes.h:139
static bool operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it, bool weak)
Definition: predtest.c:1779
@ IS_NULL
Definition: primnodes.h:1957
@ IS_NOT_NULL
Definition: primnodes.h:1957
NullTestType nulltesttype
Definition: primnodes.h:1964
Expr * arg
Definition: primnodes.h:1963

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(), predicate_refuted_by_recurse(), and predicate_refuted_by_simple_clause().

Referenced by predicate_refuted_by(), and predicate_refuted_by_recurse().

◆ 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

◆ OprProofCacheHash

HTAB* OprProofCacheHash = NULL
static

Definition at line 2093 of file predtest.c.

Referenced by InvalidateOprProofCacheCallBack(), and lookup_proof_cache().

◆ RC_implic_table

const CompareType RC_implic_table[6][6]
static
Initial value:
= {
}
#define RCGE
Definition: predtest.c:1665
#define RCLE
Definition: predtest.c:1663
#define none
Definition: predtest.c:1670
#define RCGT
Definition: predtest.c:1666
#define RCLT
Definition: predtest.c:1662
#define RCEQ
Definition: predtest.c:1664

Definition at line 1698 of file predtest.c.

Referenced by lookup_proof_cache().

◆ RC_implies_table

const bool RC_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().

◆ RC_refute_table

const CompareType RC_refute_table[6][6]
static
Initial value:

Definition at line 1711 of file predtest.c.

Referenced by lookup_proof_cache().

◆ RC_refutes_table

const bool RC_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().