From 6296d783c84fa694ef180ac67ed58d6b3cab80cf Mon Sep 17 00:00:00 2001
From: jcoleman <jtc331@gmail.com>
Date: Tue, 26 Dec 2023 14:47:15 -0500
Subject: [PATCH v6 2/3] Teach predtest.c about BooleanTest

There are lots of things we can prove based on/for IS [NOT]
{TRUE,FALSE,UNKNOWN} clauses -- particularly how they related to
boolean variables, NOT clauses, and IS [NOT] NULL clauses.

There are a few other more generic improvements as well, such as the
ability for clause_is_strict_for to recurse into NOT clauses and
adjusting proofs refutation based on implication to know that if we can
prove strong refutation we can also prove weak refutation by default.
---
 src/backend/optimizer/util/predtest.c         | 611 +++++++++++--
 .../test_predtest/expected/test_predtest.out  | 810 +++++++++++++++++-
 .../test_predtest/sql/test_predtest.sql       | 280 ++++++
 .../modules/test_predtest/test_predtest.c     |  29 +
 4 files changed, 1628 insertions(+), 102 deletions(-)

diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c
index 3a352ca37f..9737a72e46 100644
--- a/src/backend/optimizer/util/predtest.c
+++ b/src/backend/optimizer/util/predtest.c
@@ -99,6 +99,8 @@ 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 bool predicate_implied_not_null_by_clause(Expr *predicate, Node *clause,
+												 bool weak);
 static Node *extract_not_arg(Node *clause);
 static Node *extract_strong_not_arg(Node *clause);
 static bool clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false);
@@ -198,6 +200,11 @@ predicate_implied_by(List *predicate_list, List *clause_list,
  * (i.e., B must yield false or NULL).  We use this to detect mutually
  * contradictory WHERE clauses.
  *
+ * A notable difference between implication and refutation proofs is that
+ * strong/weak refutations don't vary the input of A (both must be true) but
+ * vary the allowed outcomes of B (false vs. non-truth), while for implications
+ * we vary both A (truth vs. non-falsity) and B (truth vs. non-falsity).
+ *
  * Weak refutation can be proven in some cases where strong refutation doesn't
  * hold, so it's useful to use it when possible.  We don't currently have
  * support for disproving one CHECK constraint based on another one, nor for
@@ -740,6 +747,16 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate,
 											 !weak))
 				return true;
 
+			/*
+			 * Because weak refutation expands the allowed outcomes for B
+			 * from "false" to "false or null", we can additionally prove
+			 * weak refutation in the case that strong refutation is proven.
+			 */
+			if (weak && not_arg &&
+				predicate_implied_by_recurse(predicate, not_arg,
+											 true))
+				return true;
+
 			switch (pclass)
 			{
 				case CLASS_AND:
@@ -1138,21 +1155,27 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 					Assert(list_length(op->args) == 2);
 					rightop = lsecond(op->args);
 
-					/* We might never see null Consts here, but better check */
-					if (rightop && IsA(rightop, Const) &&
-						!((Const *) rightop)->constisnull)
+					if (rightop && IsA(rightop, Const))
 					{
+						Const	*constexpr = (Const *) rightop;
 						Node	   *leftop = linitial(op->args);
 
-						if (DatumGetBool(((Const *) rightop)->constvalue))
+						/*
+						 * We might never see a null Const here, but better
+						 * check anyway.
+						 */
+						if (constexpr->constisnull)
+							return false;
+
+						if (DatumGetBool(constexpr->constvalue))
 						{
-							/* X = true implies X */
+							/* x = true implies x */
 							if (equal(predicate, leftop))
 								return true;
 						}
 						else
 						{
-							/* X = false implies NOT X */
+							/* x = false implies NOT x */
 							if (is_notclause(predicate) &&
 								equal(get_notclausearg(predicate), leftop))
 								return true;
@@ -1161,6 +1184,97 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 				}
 			}
 			break;
+		case T_NullTest:
+			{
+				NullTest *clausentest = (NullTest *) clause;
+
+				/*
+				 * row IS NOT NULL does not act in the simple way we have in
+				 * mind
+				 */
+				if (clausentest->argisrow)
+					return false;
+
+				switch (clausentest->nulltesttype)
+				{
+					case IS_NULL:
+						/*
+						 * A clause in the form "foo IS NULL" implies a
+						 * predicate "NOT foo" that is strict for "foo", but
+						 * only weakly since "foo" being null will result in
+						 * the clause evaluating to true while the predicate
+						 * will evaluate to null.
+						 */
+						if (weak && is_notclause(predicate) &&
+							clause_is_strict_for((Node *) get_notclausearg(predicate), (Node *) clausentest->arg, true))
+							return true;
+
+						break;
+					case IS_NOT_NULL:
+						break;
+				}
+			}
+			break;
+		case T_BooleanTest:
+			{
+				BooleanTest	*clausebtest = (BooleanTest *) clause;
+
+				switch (clausebtest->booltesttype)
+				{
+					case IS_TRUE:
+						/* x IS TRUE implies x */
+						if (equal(predicate, clausebtest->arg))
+							return true;
+						break;
+					case IS_FALSE:
+						/* x IS FALSE implies NOT x */
+						if (is_notclause(predicate) &&
+							equal(get_notclausearg(predicate), clausebtest->arg))
+							return true;
+						break;
+					case IS_NOT_TRUE:
+						/*
+						 * A clause in the form "foo IS NOT TRUE" implies a
+						 * predicate "NOT foo", but only weakly since "foo"
+						 * being null will result in the clause evaluating to
+						 * true while the predicate will evaluate to null.
+						 */
+						if (weak && is_notclause(predicate) &&
+							equal(get_notclausearg(predicate), clausebtest->arg))
+							return true;
+						break;
+					case IS_NOT_FALSE:
+						/*
+						 * A clause in the form "foo IS NOT FALSE" implies a
+						 * predicate "foo", but only weakly since "foo" being
+						 * null will result in the clause evaluating to true
+						 * when the predicate is null.
+						 */
+						if (weak && equal(predicate, clausebtest->arg))
+							return true;
+						break;
+					case IS_UNKNOWN:
+						/*
+						 * A clause in the form "foo IS UNKNOWN" implies a
+						 * predicate "NOT foo" that is strict for "foo", but
+						 * only weakly since "foo" being null will result in
+						 * the clause evaluating to true while the predicate
+						 * will evaluate to null.
+						 */
+						if (weak && is_notclause(predicate) &&
+							clause_is_strict_for((Node *) get_notclausearg(predicate), (Node *) clausebtest->arg, true))
+							return true;
+						break;
+					case IS_NOT_UNKNOWN:
+						/*
+						 * "foo IS NOT UKNOWN" implies "foo IS NOT NULL", but
+						 * we handle that in the predicate-type-specific cases
+						 * below.
+						 * */
+						break;
+				}
+			}
+			break;
 		default:
 			break;
 	}
@@ -1172,30 +1286,124 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 			{
 				NullTest   *predntest = (NullTest *) predicate;
 
+				/*
+				 * row IS NOT NULL does not act in the simple way we have in
+				 * mind
+				 */
+				if (predntest->argisrow)
+					return false;
+
 				switch (predntest->nulltesttype)
 				{
 					case IS_NOT_NULL:
-
 						/*
-						 * If the predicate is of the form "foo IS NOT NULL",
-						 * and we are considering strong implication, we can
-						 * conclude that the predicate is implied if the
-						 * clause is strict for "foo", i.e., it must yield
-						 * false or NULL when "foo" is NULL.  In that case
-						 * truth of the clause ensures that "foo" isn't NULL.
-						 * (Again, this is a safe conclusion because "foo"
-						 * must be immutable.)  This doesn't work for weak
-						 * implication, though.  Also, "row IS NOT NULL" does
-						 * not act in the simple way we have in mind.
+						 * When the predicate is of the form "foo IS NOT NULL",
+						 * we can conclude that the predicate is implied if
+						 * truth of the clause would imply that the predicate
+						 * must be not null.
 						 */
-						if (!weak &&
-							!predntest->argisrow &&
-							clause_is_strict_for(clause,
-												 (Node *) predntest->arg,
-												 true))
+						if (predicate_implied_not_null_by_clause(predntest->arg,
+																 clause, weak))
 							return true;
 						break;
 					case IS_NULL:
+						if (IsA(clause, BooleanTest))
+						{
+							BooleanTest* clausebtest = (BooleanTest *) clause;
+
+							/* x IS NULL is implied by x IS UNKNOWN */
+							if (clausebtest->booltesttype == IS_UNKNOWN &&
+								equal(predntest->arg, clausebtest->arg))
+								return true;
+						}
+						break;
+				}
+			}
+			break;
+		case T_BooleanTest:
+			{
+				BooleanTest	*predbtest = (BooleanTest *) predicate;
+
+				switch (predbtest->booltesttype)
+				{
+					case IS_TRUE:
+						/*
+						 * x implies x is true
+						 *
+						 * We can only prove strong implication here since
+						 * "null is true" is false rather than null.
+						 */
+						if (!weak && equal(clause, predbtest->arg))
+							return true;
+						break;
+					case IS_FALSE:
+						/*
+						 * NOT x implies x is false
+						 *
+						 * We can only prove strong implication here since "not
+						 * null" is null rather than true.
+						 */
+						if (!weak && is_notclause(clause) &&
+							equal(get_notclausearg(clause), predbtest->arg))
+							return true;
+						break;
+					case IS_NOT_TRUE:
+						{
+							/* NOT x implies x is not true */
+							if (is_notclause(clause) &&
+								equal(get_notclausearg(clause), predbtest->arg))
+								return true;
+
+							if (IsA(clause, BooleanTest))
+							{
+								BooleanTest *clausebtest = (BooleanTest *) clause;
+
+								/* x is unknown implies x is not true */
+								if (clausebtest->booltesttype == IS_UNKNOWN &&
+									equal(clausebtest->arg, predbtest->arg))
+									return true;
+							}
+						}
+						break;
+					case IS_NOT_FALSE:
+						{
+							/* x implies x is not false*/
+							if (equal(clause, predbtest->arg))
+								return true;
+
+							if (IsA(clause, BooleanTest))
+							{
+								BooleanTest *clausebtest = (BooleanTest *) clause;
+
+								/* x is unknown implies x is not false */
+								if (clausebtest->booltesttype == IS_UNKNOWN &&
+									equal(clausebtest->arg, predbtest->arg))
+									return true;
+							}
+						}
+						break;
+					case IS_UNKNOWN:
+						if (IsA(clause, NullTest))
+						{
+							NullTest   *clausentest = (NullTest *) clause;
+
+							/* x IS NULL implies x is unknown */
+							if (clausentest->nulltesttype == IS_NULL &&
+								equal(clausentest->arg, predbtest->arg))
+								return true;
+						}
+						break;
+					case IS_NOT_UNKNOWN:
+						/*
+						 * Since "foo IS NOT UNKNOWN" has the same meaning
+						 * as "foo is NOT NULL" (assuming "foo" is a boolean)
+						 * we can prove the same things as we did earlier for
+						 * for NullTest's IS_NOT_NULL case.
+						 *
+						 * For example: truth of x implies x is not unknown.
+						 */
+						if (predicate_implied_not_null_by_clause(predbtest->arg, clause, weak))
+							return true;
 						break;
 				}
 			}
@@ -1212,6 +1420,110 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause,
 	return operator_predicate_proof(predicate, clause, false, weak);
 }
 
+/*
+ * predicate_implied_not_null_by_clause
+ *	  Tests a "simple clause" predicate to see if truth of the "simple clause"
+ *	  restriction implies that that predicate is not null.
+ *
+ * We return true if able to prove the implication, false if not. It is expected
+ * that the predicate argument to this function has already been reduced to the
+ * argument of any BooleanTest or NullTest predicate expressions.
+ *
+ * This function encapsulates a specific subcase of
+ * predicate_implied_by_simple_clause cases which is useful in several cases of
+ * both refutation and implication.
+ *
+ * Proving implication of "NOT NULL" is particularly useful for proving it's
+ * safe to use partial indexes defined with a "foo NOT NULL" condition.
+ *
+ * In several of the cases below (e.g., BooleanTest and NullTest) we could
+ * recurse into the argument of those expressions. For example, if the argument
+ * in a BooleanTest is itself a BooleanTest or a NullTest, then if the argument
+ * to that nested test expression matches the clause's subexpression we can
+ * trivially prove implication of "NOT NULL" since BooleanTest and NullTest
+ * always evaluate to true or false. However that doesn't seem useful to expend
+ * cycles on at this point.
+ */
+static bool
+predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, bool weak)
+{
+	switch (nodeTag(clause))
+	{
+		case T_BooleanTest:
+			{
+				BooleanTest *clausebtest = (BooleanTest *) clause;
+
+				/*
+				 * Because the obvious case of "foo IS NOT UNKNOWN" proving
+				 * "foo" isn't null, we can also prove "foo" isn't null if we
+				 * know that it has to be true or false.
+				 */
+				switch (clausebtest->booltesttype)
+				{
+					case IS_TRUE:
+					case IS_FALSE:
+					case IS_NOT_UNKNOWN:
+						if (equal(clausebtest->arg, predicate))
+							return true;
+						break;
+					default:
+						break;
+				}
+			}
+			break;
+		case T_NullTest:
+			{
+				NullTest *clausentest = (NullTest *) clause;
+
+				/*
+				 * row IS NULL does not act in the simple way we have in mind
+				 */
+				if (clausentest->argisrow)
+					return false;
+
+				/*
+				 * It's self-evident that "foo IS NOT NULL" implies "foo"
+				 * isn't NULL.
+				 */
+				if (clausentest->nulltesttype == IS_NOT_NULL &&
+					equal(predicate, clausentest->arg))
+					return true;
+			}
+			break;
+		case T_DistinctExpr:
+			/*
+			 * If both of the two arguments to IS [NOT] DISTINCT FROM separately
+			 * imply that the predicate is not null or are strict for the
+			 * predicate, then we could prove implication that the predicate is
+			 * not null. But it's not obvious that it's worth expending time
+			 * on that check since having the predicate in the expression on
+			 * both sides of the distinct expression is likely uncommon.
+			 */
+			break;
+		case T_Const:
+			/*
+			 * We don't currently have to consider Const expressions because constant
+			 * folding would have eliminated the node types we consider here.
+			 */
+			break;
+		default:
+			break;
+	}
+
+	/*
+	 * We can conclude that a predicate "foo" is not null if the clause is
+	 * strict for "foo", i.e., it must yield false or NULL when "foo" is NULL.
+	 * In that case truth of the clause ensures that "foo" isn't NULL.  (Again,
+	 * this is a safe conclusion because "foo" must be immutable.) This doesn't
+	 * work for weak implication, though, since the clause yielding the
+	 * non-false value NULL means the predicate will evaluate to false.
+	 */
+	if (!weak && clause_is_strict_for(clause, (Node *) predicate, true))
+		return true;
+
+	return false;
+}
+
 /*
  * predicate_refuted_by_simple_clause
  *	  Does the predicate refutation test for a "simple clause" predicate
@@ -1255,31 +1567,20 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 				{
 					case IS_NULL:
 						{
-							switch (nodeTag(predicate))
-							{
-								case T_NullTest:
-									{
-										NullTest   *predntest = (NullTest *) predicate;
-
-										/*
-										 * row IS NULL does not act in the
-										 * simple way we have in mind
-										 */
-										if (predntest->argisrow)
-											return false;
-
-										/*
-										 * foo IS NULL refutes foo IS NOT
-										 * NULL, at least in the non-row case,
-										 * for both strong and weak refutation
-										 */
-										if (predntest->nulltesttype == IS_NOT_NULL &&
-											equal(predntest->arg, clausentest->arg))
-											return true;
-									}
-								default:
-									break;
-							}
+							/*
+							 * A clause in the form "foo IS NULL" refutes any
+							 * predicate that is itself implied not null, but
+							 * we have to exclude cases where we'd allow false
+							 * in strictness checking so we always pass
+							 * weak=true here. This is because we aren't
+							 * assuming anything about the form of the
+							 * predicate in that case, and, for example, we
+							 * might have a predicate of simply "foo", but "foo
+							 * = false" would mean both our clause and our
+							 * predicate would evaluate to "false".
+							 */
+							if (predicate_implied_not_null_by_clause(clausentest->arg, (Node *) predicate, true))
+								return true;
 
 							/*
 							 * foo IS NULL weakly refutes any predicate that
@@ -1288,15 +1589,111 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 							 * in the predicate, it's known immutable).
 							 */
 							if (weak &&
-								clause_is_strict_for((Node *) predicate,
-													 (Node *) clausentest->arg,
-													 true))
+								clause_is_strict_for((Node *) predicate, (Node *) clausentest->arg, true))
 								return true;
 
 							return false;	/* we can't succeed below... */
 						}
 						break;
 					case IS_NOT_NULL:
+						/*
+						 * "foo IS NOT NULL" refutes both "foo IS NULL"
+						 * and "foo IS UNKNOWN", but we handle that in the
+						 * predicate switch statement.
+						 */
+						break;
+				}
+			}
+			break;
+		case T_BooleanTest:
+			{
+				BooleanTest 	*clausebtest = (BooleanTest *) clause;
+
+				switch (clausebtest->booltesttype)
+				{
+					case IS_TRUE:
+						/*
+						 * We've already previously checked for the clause
+						 * being a NOT arg and determined refutation based on
+						 * implication of the predicate by that arg. That check
+						 * handles the case "foos IS TRUE" refuting "NOT foo",
+						 * so we don't have to do anything special here.
+						 */
+						break;
+					case IS_NOT_TRUE:
+						{
+							if (IsA(predicate, BooleanTest))
+							{
+								BooleanTest	*predbtest = (BooleanTest *) predicate;
+
+								/* foo IS NOT TRUE refutes foo IS TRUE */
+								if (predbtest->booltesttype == IS_TRUE &&
+									equal(predbtest->arg, clausebtest->arg))
+									return true;
+							}
+
+							/* foo IS NOT TRUE weakly refutes foo */
+							if (weak && equal(predicate, clausebtest->arg))
+								return true;
+
+						}
+						break;
+					case IS_FALSE:
+						if (IsA(predicate, BooleanTest))
+						{
+							BooleanTest	*predbtest = (BooleanTest *) predicate;
+
+							/* foo IS UNKNOWN refutes foo IS TRUE */
+							/* foo IS UNKNOWN refutes foo IS NOT UNKNOWN */
+							if (predbtest->booltesttype == IS_UNKNOWN &&
+								equal(predbtest->arg, clausebtest->arg))
+								return true;
+						}
+						break;
+					case IS_NOT_FALSE:
+						break;
+					case IS_UNKNOWN:
+						{
+							/*
+							 * A clause in the form "foo IS UNKNOWN" refutes any
+							 * predicate that is itself implied not null, but
+							 * we have to exclude cases where we'd allow false
+							 * in strictness checking so we always pass
+							 * weak=true here. This is because we aren't
+							 * assuming anything about the form of the
+							 * predicate in that case, and, for example, we
+							 * might have a predicate of simply "foo", but "foo
+							 * = false" would mean both our clause and our
+							 * predicate would evaluate to "false".
+							 */
+							if (predicate_implied_not_null_by_clause(clausebtest->arg, (Node *) predicate, true))
+								return true;
+
+							/*
+							 * A clause in the form "foo IS UNKNOWN" implies
+							 * that "foo" is null, so if the predicate is
+							 * strict for "foo" then that clause weakly refutes
+							 * the predicate since "foo" being null will cause
+							 * the predicate to evaluate to non-true, therefore
+							 * proving weak refutation.
+							 *
+							 * This doesn't work for strong refutation, however,
+							 * since evaluating the predicate with "foo" set to
+							 * null may result in "null" rather than "false".
+							 */
+							if (weak &&
+								clause_is_strict_for((Node *) predicate, (Node *) clausebtest->arg, true))
+								return true;
+
+							return false;			/* we can't succeed below... */
+						}
+						break;
+					case IS_NOT_UNKNOWN:
+						/*
+						 * "foo IS NOT UNKNOWN" refutes both "foo IS UNKNOWN"
+						 * and "foo IS NULL", but we handle that in the
+						 * predicate switch statement.
+						 */
 						break;
 				}
 			}
@@ -1319,42 +1716,19 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 				{
 					case IS_NULL:
 						{
-							switch (nodeTag(clause))
-							{
-								case T_NullTest:
-									{
-										NullTest   *clausentest = (NullTest *) clause;
-
-										/*
-										 * row IS NULL does not act in the
-										 * simple way we have in mind
-										 */
-										if (clausentest->argisrow)
-											return false;
-
-										/*
-										 * foo IS NOT NULL refutes foo IS NULL
-										 * for both strong and weak refutation
-										 */
-										if (clausentest->nulltesttype == IS_NOT_NULL &&
-											equal(clausentest->arg, predntest->arg))
-											return true;
-									}
-									break;
-								default:
-									break;
-							}
-
 							/*
-							 * When the predicate is of the form "foo IS
-							 * NULL", we can conclude that the predicate is
-							 * refuted if the clause is strict for "foo" (see
-							 * notes for implication case).  That works for
-							 * either strong or weak refutation.
+							 * A predicate in the form "foo IS NULL" is refuted
+							 * if truth of the clause would imply that the
+							 * predicate must be not null.
+							 *
+							 * We always pass weak=false here because there are
+							 * some cases where we can only prove strong
+							 * implication of "foo is not null", but that will
+							 * also prove weak refutation since strong
+							 * refutation is a strict superset of weak
+							 * refutation.
 							 */
-							if (clause_is_strict_for(clause,
-													 (Node *) predntest->arg,
-													 true))
+							if (predicate_implied_not_null_by_clause(predntest->arg, clause, false))
 								return true;
 						}
 						break;
@@ -1365,6 +1739,37 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause,
 				return false;	/* we can't succeed below... */
 			}
 			break;
+		case T_BooleanTest:
+			{
+				BooleanTest 	*predbtest = (BooleanTest *) predicate;
+
+				switch (predbtest->booltesttype)
+				{
+					case IS_UNKNOWN:
+						{
+							/*
+							 * A predicate in the form "foo IS UNKNOWN" is refuted
+							 * if truth of the clause would imply that the
+							 * predicate must be not null.
+							 *
+							 * We always pass weak=false here because there are
+							 * some cases where we can only prove strong
+							 * implication of "foo is not null", but that will
+							 * also prove weak refutation since strong
+							 * refutation is a strict superset of weak
+							 * refutation.
+							 */
+							if (predicate_implied_not_null_by_clause(predbtest->arg, clause, false))
+								return true;
+
+							return false;			/* we can't succeed below... */
+						}
+						break;
+					default:
+						break;
+				}
+			}
+			break;
 		default:
 			break;
 	}
@@ -1505,6 +1910,17 @@ clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
 		return false;
 	}
 
+	/*
+	 * We can recurse into "not foo" without any additional processing because
+	 * the "not" operator is itself strict, evaluating to null when its
+	 * argument is null. We can't pass along allow_false=true, and instead
+	 * always pass allow_false=false since "not (false)" is true rather than
+	 * null.
+	 */
+	if (is_notclause(clause) &&
+		clause_is_strict_for((Node *) get_notclausearg(clause), subexpr, false))
+		return true;
+
 	/*
 	 * CoerceViaIO is strict (whether or not the I/O functions it calls are).
 	 * Likewise, ArrayCoerceExpr is strict for its array argument (regardless
@@ -1592,6 +2008,33 @@ clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false)
 		return clause_is_strict_for(arraynode, subexpr, false);
 	}
 
+	/*
+	 * BooleanTest expressions never evaluate to null so we can't do anything
+	 * if allow_false isn't true.
+	 */
+	if (allow_false && IsA(clause, BooleanTest))
+	{
+		BooleanTest *test = (BooleanTest *) clause;
+
+		switch (test->booltesttype)
+		{
+			case IS_TRUE:
+			case IS_FALSE:
+			case IS_NOT_UNKNOWN:
+				return clause_is_strict_for((Node *) test->arg, subexpr, false);
+				break;
+			/*
+			 * null is not true, null is not false, and null is unknown are
+			 * true, hence we know they can't be strict.
+			 */
+			case IS_NOT_TRUE:
+			case IS_NOT_FALSE:
+			case IS_UNKNOWN:
+				return false;
+				break;
+		}
+	}
+
 	/*
 	 * When recursing into an expression, we might find a NULL constant.
 	 * That's certainly NULL, whether it matches subexpr or not.
diff --git a/src/test/modules/test_predtest/expected/test_predtest.out b/src/test/modules/test_predtest/expected/test_predtest.out
index 6d21bcd603..7a01fe1252 100644
--- a/src/test/modules/test_predtest/expected/test_predtest.out
+++ b/src/test/modules/test_predtest/expected/test_predtest.out
@@ -93,6 +93,48 @@ w_i_holds         | f
 s_r_holds         | f
 w_r_holds         | f
 
+select * from test_predtest($$
+select x is not unknown, x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not unknown, x is not null
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not null, x is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
 select * from test_predtest($$
 select x is not null, x is null
 from integers
@@ -143,12 +185,222 @@ $$);
 strong_implied_by | f
 weak_implied_by   | f
 strong_refuted_by | f
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is not true, not x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select not x, x is not true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not true, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is unknown, x is not true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not unknown, x is not true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
 weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not unknown, x is not false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is true, x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x, x is true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select not x, x is true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is true, not x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is not true, x is true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is false, x is true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
 w_r_holds         | t
 
+select * from test_predtest($$
+select x is unknown, x is true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is false, not x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select not x, x is false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
 select * from test_predtest($$
 select x is false, x
 from booleans
@@ -164,21 +416,316 @@ s_r_holds         | t
 w_r_holds         | t
 
 select * from test_predtest($$
-select x, x is false
+select x, x is false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is not false, x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x, x is not false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not false, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is unknown, x is not false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is unknown, x
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is not unknown, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is unknown, x is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select strictf(x, y) is unknown, x is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select strictf(x, y) is unknown, strictf(x, y) is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is unknown, strictf(x, y) is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is unknown, (x is true) is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is null, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select not strictf(x, y), x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | t
+
+select * from test_predtest($$
+select not strictf(x, y), x is null
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is null, not strictf(x, y)
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is not null, not strictf(x, y)
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is not unknown, not strictf(x, y)
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is unknown, not strictf(x, y)
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is not null, x is true
 from booleans
 $$);
 -[ RECORD 1 ]-----+--
-strong_implied_by | f
-weak_implied_by   | f
-strong_refuted_by | t
-weak_refuted_by   | t
-s_i_holds         | f
-w_i_holds         | f
-s_r_holds         | t
-w_r_holds         | t
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
 
 select * from test_predtest($$
-select x is unknown, x
+select x is not null, x is false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+-- Assorted not-so-trivial refutation rules
+select * from test_predtest($$
+select x is null, x
 from booleans
 $$);
 -[ RECORD 1 ]-----+--
@@ -192,22 +739,21 @@ s_r_holds         | t
 w_r_holds         | t
 
 select * from test_predtest($$
-select x, x is unknown
+select x, x is null
 from booleans
 $$);
 -[ RECORD 1 ]-----+--
 strong_implied_by | f
 weak_implied_by   | f
 strong_refuted_by | f
-weak_refuted_by   | f
+weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | t
 s_r_holds         | f
 w_r_holds         | t
 
--- Assorted not-so-trivial refutation rules
 select * from test_predtest($$
-select x is null, x
+select x is null, x is not unknown
 from booleans
 $$);
 -[ RECORD 1 ]-----+--
@@ -221,17 +767,17 @@ s_r_holds         | t
 w_r_holds         | t
 
 select * from test_predtest($$
-select x, x is null
+select x is not unknown, x is null
 from booleans
 $$);
 -[ RECORD 1 ]-----+--
 strong_implied_by | f
 weak_implied_by   | f
-strong_refuted_by | f
+strong_refuted_by | t
 weak_refuted_by   | t
 s_i_holds         | f
-w_i_holds         | t
-s_r_holds         | f
+w_i_holds         | f
+s_r_holds         | t
 w_r_holds         | t
 
 select * from test_predtest($$
@@ -1094,3 +1640,231 @@ w_i_holds         | t
 s_r_holds         | f
 w_r_holds         | t
 
+-- More BooleanTest proofs
+-- I'm wondering if we should standardize a location for all of them, and
+-- potentially updated test_predtest to run both directions rather than
+-- needing to duplicate queries (with the two clauses swapped).
+select * from test_predtest($$
+select x is true, x = true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is false, x = false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x, x is false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select strictf(x, y), x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | t
+
+select * from test_predtest($$
+select strictf(x, y), x is not unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select not x, x is true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x, x is not true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | f
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | f
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is true, x is not true
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is true, x is false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is true, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is true, x is null
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is false, x is unknown
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is false, x is null
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is unknown, x is false
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
+select * from test_predtest($$
+select x is unknown, x is null
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | t
+weak_implied_by   | t
+strong_refuted_by | f
+weak_refuted_by   | f
+s_i_holds         | t
+w_i_holds         | t
+s_r_holds         | f
+w_r_holds         | f
+
+select * from test_predtest($$
+select x is unknown, x is not null
+from booleans
+$$);
+-[ RECORD 1 ]-----+--
+strong_implied_by | f
+weak_implied_by   | f
+strong_refuted_by | t
+weak_refuted_by   | t
+s_i_holds         | f
+w_i_holds         | f
+s_r_holds         | t
+w_r_holds         | t
+
diff --git a/src/test/modules/test_predtest/sql/test_predtest.sql b/src/test/modules/test_predtest/sql/test_predtest.sql
index 072eb5b0d5..6a3c01dbf3 100644
--- a/src/test/modules/test_predtest/sql/test_predtest.sql
+++ b/src/test/modules/test_predtest/sql/test_predtest.sql
@@ -56,6 +56,21 @@ select x is not null, x
 from booleans
 $$);
 
+select * from test_predtest($$
+select x is not unknown, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not unknown, x is not null
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not null, x is not unknown
+from booleans
+$$);
+
 select * from test_predtest($$
 select x is not null, x is null
 from integers
@@ -76,6 +91,81 @@ select x, x is not true
 from booleans
 $$);
 
+select * from test_predtest($$
+select x is not true, not x
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, x is not true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not true, x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is not true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not unknown, x is not true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not unknown, x is not false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is true, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is true, not x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not true, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is false, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is false, not x
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, x is false
+from booleans
+$$);
+
 select * from test_predtest($$
 select x is false, x
 from booleans
@@ -86,6 +176,26 @@ select x, x is false
 from booleans
 $$);
 
+select * from test_predtest($$
+select x is not false, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is not false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not false, x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is not false
+from booleans
+$$);
+
 select * from test_predtest($$
 select x is unknown, x
 from booleans
@@ -96,6 +206,81 @@ select x, x is unknown
 from booleans
 $$);
 
+select * from test_predtest($$
+select x is not unknown, x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select strictf(x, y) is unknown, x is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select strictf(x, y) is unknown, strictf(x, y) is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, strictf(x, y) is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, (x is true) is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is null, x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select not strictf(x, y), x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select not strictf(x, y), x is null
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is null, not strictf(x, y)
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not null, not strictf(x, y)
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not unknown, not strictf(x, y)
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, not strictf(x, y)
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not null, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not null, x is false
+from booleans
+$$);
+
 -- Assorted not-so-trivial refutation rules
 
 select * from test_predtest($$
@@ -108,6 +293,16 @@ select x, x is null
 from booleans
 $$);
 
+select * from test_predtest($$
+select x is null, x is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not unknown, x is null
+from booleans
+$$);
+
 select * from test_predtest($$
 select strictf(x,y), x is null
 from booleans
@@ -440,3 +635,88 @@ select * from test_predtest($$
 select x = all(opaque_array(array[1])), x is null
 from integers
 $$);
+
+-- More BooleanTest proofs
+-- I'm wondering if we should standardize a location for all of them, and
+-- potentially updated test_predtest to run both directions rather than
+-- needing to duplicate queries (with the two clauses swapped).
+
+select * from test_predtest($$
+select x is true, x = true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is false, x = false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is false
+from booleans
+$$);
+
+select * from test_predtest($$
+select strictf(x, y), x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select strictf(x, y), x is not unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, x is true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is not true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is true, x is not true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is true, x is false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is true, x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is true, x is null
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is false, x is unknown
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is false, x is null
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is null
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x is not null
+from booleans
+$$);
diff --git a/src/test/modules/test_predtest/test_predtest.c b/src/test/modules/test_predtest/test_predtest.c
index 9e6a6471cc..7f35a976ed 100644
--- a/src/test/modules/test_predtest/test_predtest.c
+++ b/src/test/modules/test_predtest/test_predtest.c
@@ -118,6 +118,22 @@ test_predtest(PG_FUNCTION_ARGS)
 			w_r_holds = false;
 	}
 
+	/* Because weak refutation proofs are a strict subset of strong refutation
+	 * proofs (since for "A => B" "A" is always true) we ought never have strong
+	 * refutation hold when weak refutation does not.
+	 *
+	 * We can't make the same assertion for implication since moving from strong
+	 * to weak implication expands the allowed values of "A" from true to either
+	 * true or NULL.
+	 *
+	 * If this fails it constitutes a bug not with the proofs but with either
+	 * this test module or a more core part of expression evaluation since we
+	 * are validating the logical correctness of the observed result rather
+	 * than the proof.
+	 */
+	if (s_r_holds && !w_r_holds)
+		elog(ERROR, "s_r_holds was true; w_r_holds cannot be false");
+
 	/*
 	 * Now, dig the clause querytrees out of the plan, and see what predtest.c
 	 * does with them.
@@ -179,6 +195,19 @@ test_predtest(PG_FUNCTION_ARGS)
 	if (weak_refuted_by && !w_r_holds)
 		elog(WARNING, "weak_refuted_by result is incorrect");
 
+	/*
+	 * As with our earlier check of the logical consistency of whether strong
+	 * and weak refutation hold, we ought never prove strong refutation without
+	 * also proving weak refutation.
+	 *
+	 * Also as earlier we cannot make the same guarantee about implication
+	 * proofs.
+	 *
+	 * A warning here suggests a bug in the proof code.
+	 */
+	if (s_r_holds && strong_refuted_by && !weak_refuted_by)
+		elog(WARNING, "strong_refuted_by was true; weak_refuted_by should also be proven");
+
 	/*
 	 * Clean up and return a record of the results.
 	 */
-- 
2.39.3 (Apple Git-145)

