handle-null-constants-in-predtest-1.patch

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