diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c
index fb963d0..446207d 100644
*** a/src/backend/optimizer/util/predtest.c
--- b/src/backend/optimizer/util/predtest.c
*************** static Node *extract_not_arg(Node *claus
*** 100,106 ****
static Node *extract_strong_not_arg(Node *clause);
static bool clause_is_strict_for(Node *clause, Node *subexpr);
static bool operator_predicate_proof(Expr *predicate, Node *clause,
! bool refute_it);
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,
--- 100,106 ----
static Node *extract_strong_not_arg(Node *clause);
static bool clause_is_strict_for(Node *clause, Node *subexpr);
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,
*************** predicate_implied_by_simple_clause(Expr
*** 1137,1143 ****
}
/* Else try operator-related knowledge */
! return operator_predicate_proof(predicate, clause, false);
}
/*----------
--- 1137,1143 ----
}
/* Else try operator-related knowledge */
! return operator_predicate_proof(predicate, clause, false, weak);
}
/*----------
*************** predicate_refuted_by_simple_clause(Expr
*** 1232,1238 ****
}
/* Else try operator-related knowledge */
! return operator_predicate_proof(predicate, clause, true);
}
--- 1232,1238 ----
}
/* Else try operator-related knowledge */
! return operator_predicate_proof(predicate, clause, true, weak);
}
*************** static const StrategyNumber BT_refute_ta
*** 1498,1506 ****
* values, since then the operators aren't being given identical inputs. But
* we only support that for btree operators, for which we can assume that all
* non-null inputs result in non-null outputs, so that it doesn't matter which
! * two non-null constants we consider. Currently the code below just reports
! * "proof failed" if either constant is NULL, but in some cases we could be
! * smarter (and that likely would require checking strong vs. weak proofs).
*
* We can make proofs involving several expression forms (here "foo" and "bar"
* represent subexpressions that are identical according to equal()):
--- 1498,1505 ----
* values, since then the operators aren't being given identical inputs. But
* we only support that for btree operators, for which we can assume that all
* non-null inputs result in non-null outputs, so that it doesn't matter which
! * two non-null constants we consider. If either constant is NULL, we have
! * to think harder, but sometimes the proof still works, as explained below.
*
* We can make proofs involving several expression forms (here "foo" and "bar"
* represent subexpressions that are identical according to equal()):
*************** static const StrategyNumber BT_refute_ta
*** 1528,1534 ****
* and we dare not make deductions with those.
*/
static bool
! operator_predicate_proof(Expr *predicate, Node *clause, bool refute_it)
{
OpExpr *pred_opexpr,
*clause_opexpr;
--- 1527,1534 ----
* and we dare not make deductions with those.
*/
static bool
! operator_predicate_proof(Expr *predicate, Node *clause,
! bool refute_it, bool weak)
{
OpExpr *pred_opexpr,
*clause_opexpr;
*************** operator_predicate_proof(Expr *predicate
*** 1675,1691 ****
* We have two identical subexpressions, and two other subexpressions that
* are not identical but are both Consts; and we have commuted the
* operators if necessary so that the Consts are on the right. We'll need
! * to compare the Consts' values. If either is NULL, fail.
! *
! * Future work: in some cases the desired proof might hold even with NULL
! * constants. But beware that we've not yet identified the operators as
! * btree ops, so for instance it'd be quite unsafe to assume they are
! * strict without checking.
*/
- if (pred_const->constisnull)
- return false;
if (clause_const->constisnull)
return false;
/*
* Lookup the constant-comparison operator using the system catalogs and
--- 1675,1720 ----
* We have two identical subexpressions, and two other subexpressions that
* are not identical but are both Consts; and we have commuted the
* operators if necessary so that the Consts are on the right. We'll need
! * to compare the Consts' values. If either is NULL, we can't do that, so
! * usually the proof fails ... but in some cases we can claim success.
*/
if (clause_const->constisnull)
+ {
+ /* If clause_op isn't strict, we can't prove anything */
+ if (!op_strict(clause_op))
+ return false;
+
+ /*
+ * At this point we know that the clause returns NULL. For proof
+ * types that assume truth of the clause, this means the proof is
+ * vacuously true (a/k/a "false implies anything"). That's all proof
+ * types except weak implication.
+ */
+ if (!(weak && !refute_it))
+ return true;
+
+ /*
+ * For weak implication, it's still possible for the proof to succeed,
+ * if the predicate can also be proven NULL. In that case we've got
+ * NULL => NULL which is valid for this proof type.
+ */
+ if (pred_const->constisnull && op_strict(pred_op))
+ return true;
+ /* Else the proof fails */
+ return false;
+ }
+ if (pred_const->constisnull)
+ {
+ /*
+ * If the pred_op is strict, we know the predicate yields NULL, which
+ * means the proof succeeds for either weak implication or weak
+ * refutation.
+ */
+ if (weak && op_strict(pred_op))
+ return true;
+ /* Else the proof fails */
return false;
+ }
/*
* Lookup the constant-comparison operator using the system catalogs and
diff --git a/src/test/modules/test_predtest/expected/test_predtest.out b/src/test/modules/test_predtest/expected/test_predtest.out
index 9dd8aec..5574e03 100644
*** a/src/test/modules/test_predtest/expected/test_predtest.out
--- b/src/test/modules/test_predtest/expected/test_predtest.out
*************** w_i_holds | f
*** 781,793 ****
s_r_holds | f
w_r_holds | f
- -- XXX ideally, we could prove this case too, for strong implication
select * from test_predtest($$
select x <= 5, x in (1,3,5,null)
from integers
$$);
-[ RECORD 1 ]-----+--
! strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
--- 781,792 ----
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= 5, x in (1,3,5,null)
from integers
$$);
-[ RECORD 1 ]-----+--
! strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
diff --git a/src/test/modules/test_predtest/sql/test_predtest.sql b/src/test/modules/test_predtest/sql/test_predtest.sql
index 298b8bf..2734735 100644
*** a/src/test/modules/test_predtest/sql/test_predtest.sql
--- b/src/test/modules/test_predtest/sql/test_predtest.sql
*************** select x <= 5, x in (1,3,5,7)
*** 306,312 ****
from integers
$$);
- -- XXX ideally, we could prove this case too, for strong implication
select * from test_predtest($$
select x <= 5, x in (1,3,5,null)
from integers
--- 306,311 ----
diff --git a/src/test/regress/expected/inherit.out b/src/test/regress/expected/inherit.out
index a79f891..d56e5d2 100644
*** a/src/test/regress/expected/inherit.out
--- b/src/test/regress/expected/inherit.out
*************** explain (costs off) select * from list_p
*** 1715,1725 ****
Append
-> Seq Scan on part_ab_cd
Filter: (((a)::text = 'ab'::text) OR ((a)::text = ANY ('{NULL,cd}'::text[])))
! -> Seq Scan on part_ef_gh
! Filter: (((a)::text = 'ab'::text) OR ((a)::text = ANY ('{NULL,cd}'::text[])))
! -> Seq Scan on part_null_xy
! Filter: (((a)::text = 'ab'::text) OR ((a)::text = ANY ('{NULL,cd}'::text[])))
! (7 rows)
explain (costs off) select * from list_parted where a = 'ab';
QUERY PLAN
--- 1715,1721 ----
Append
-> Seq Scan on part_ab_cd
Filter: (((a)::text = 'ab'::text) OR ((a)::text = ANY ('{NULL,cd}'::text[])))
! (3 rows)
explain (costs off) select * from list_parted where a = 'ab';
QUERY PLAN