James Coleman <jtc...@gmail.com> writes:
> [ v6 patchset ]
I went ahead and committed 0001 after one more round of review
statements; my bad). I also added the changes in test_predtest.c from
0002. I attach a rebased version of 0002, as well as 0003 which isn't
changed, mainly to keep the cfbot happy.
I'm still not happy with what you did in predicate_refuted_by_recurse:
it feels wrong and rather expensively so. There has to be a better
way. Maybe strong vs. weak isn't quite the right formulation for
refutation tests?
regards, tom lane
diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c
index 6e3b376f3d..5bb5bb4f0e 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:
@@ -1137,21 +1154,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;
@@ -1160,6 +1183,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;
}
@@ -1171,30 +1285,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;
}
}
@@ -1211,6 +1419,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
@@ -1254,32 +1566,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;
- }
- break;
- 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 +1588,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;
}
}
@@ -1320,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;
@@ -1366,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;
}
@@ -1506,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
@@ -1593,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
+$$);
From efa4da4428010271ba5f2eecf96ceec614bd6a86 Mon Sep 17 00:00:00 2001
From: jcoleman <jtc...@gmail.com>
Date: Mon, 15 Jan 2024 09:00:14 -0500
Subject: [PATCH v6 3/3] Add temporary 'all permutations' test
---
src/test/modules/test_predtest/Makefile | 2 +-
.../expected/test_all_permutations.out | 226 ++++++++++++++++++
.../sql/test_all_permutations.sql | 26 ++
3 files changed, 253 insertions(+), 1 deletion(-)
create mode 100644 src/test/modules/test_predtest/expected/test_all_permutations.out
create mode 100644 src/test/modules/test_predtest/sql/test_all_permutations.sql
diff --git a/src/test/modules/test_predtest/Makefile b/src/test/modules/test_predtest/Makefile
index a235e2aac9..5416350844 100644
--- a/src/test/modules/test_predtest/Makefile
+++ b/src/test/modules/test_predtest/Makefile
@@ -9,7 +9,7 @@ PGFILEDESC = "test_predtest - test code for optimizer/util/predtest.c"
EXTENSION = test_predtest
DATA = test_predtest--1.0.sql
-REGRESS = test_predtest
+REGRESS = test_predtest test_all_permutations
ifdef USE_PGXS
PG_CONFIG = pg_config
diff --git a/src/test/modules/test_predtest/expected/test_all_permutations.out b/src/test/modules/test_predtest/expected/test_all_permutations.out
new file mode 100644
index 0000000000..a27b2cfcff
--- /dev/null
+++ b/src/test/modules/test_predtest/expected/test_all_permutations.out
@@ -0,0 +1,226 @@
+with clauses(expr) as (
+ values
+ ('x'),
+ ('not x'),
+ ('strictf(x, y)'),
+ ('not strictf(x, y)'),
+ ('x is null'),
+ ('x is not null'),
+ ('x is true'),
+ ('x is not true'),
+ ('x is false'),
+ ('x is not false'),
+ ('x is unknown'),
+ ('x is not unknown'),
+ ('x = true'),
+ ('x = false')
+)
+select p.expr predicate, c.expr clause, t.*
+from clauses p, clauses c
+join lateral (
+ select *
+ from test_predtest(
+ 'select ' || p.expr || ', ' || c.expr ||
+ ' from booleans'
+ )
+) t on true;
+ predicate | clause | strong_implied_by | weak_implied_by | strong_refuted_by | weak_refuted_by | s_i_holds | w_i_holds | s_r_holds | w_r_holds
+-------------------+-------------------+-------------------+-----------------+-------------------+-----------------+-----------+-----------+-----------+-----------
+ x | x | t | t | f | f | t | t | f | f
+ not x | x | f | f | t | t | f | f | t | t
+ strictf(x, y) | x | f | f | f | f | f | f | f | f
+ not strictf(x, y) | x | f | f | f | f | f | f | f | f
+ x is null | x | f | f | t | t | f | f | t | t
+ x is not null | x | t | f | f | f | t | f | f | f
+ x is true | x | t | f | f | f | t | f | f | f
+ x is not true | x | f | f | t | t | f | f | t | t
+ x is false | x | f | f | t | t | f | f | t | t
+ x is not false | x | t | t | f | f | t | t | f | f
+ x is unknown | x | f | f | t | t | f | f | t | t
+ x is not unknown | x | t | f | f | f | t | f | f | f
+ x = true | x | t | t | f | f | t | t | f | f
+ x = false | x | f | f | t | t | f | f | t | t
+ x | not x | f | f | t | t | f | f | t | t
+ not x | not x | t | t | f | f | t | t | f | f
+ strictf(x, y) | not x | f | f | f | f | f | f | f | t
+ not strictf(x, y) | not x | f | f | f | f | f | t | f | f
+ x is null | not x | f | f | t | t | f | f | t | t
+ x is not null | not x | t | f | f | f | t | f | f | f
+ x is true | not x | f | f | t | t | f | f | t | t
+ x is not true | not x | t | t | f | f | t | t | f | f
+ x is false | not x | t | f | f | f | t | f | f | f
+ x is not false | not x | f | f | t | t | f | f | t | t
+ x is unknown | not x | f | f | t | t | f | f | t | t
+ x is not unknown | not x | t | f | f | f | t | f | f | f
+ x = true | not x | f | f | t | t | f | f | t | t
+ x = false | not x | t | t | f | f | t | t | f | f
+ x | strictf(x, y) | f | f | f | f | t | f | f | f
+ not x | strictf(x, y) | f | f | f | f | f | f | t | t
+ strictf(x, y) | strictf(x, y) | t | t | f | f | t | t | f | f
+ not strictf(x, y) | strictf(x, y) | f | f | t | t | f | f | t | t
+ x is null | strictf(x, y) | f | f | t | t | f | f | t | t
+ x is not null | strictf(x, y) | t | f | f | f | t | f | f | f
+ x is true | strictf(x, y) | f | f | f | f | t | f | f | f
+ x is not true | strictf(x, y) | f | f | f | f | f | f | t | t
+ x is false | strictf(x, y) | f | f | f | f | f | f | t | t
+ x is not false | strictf(x, y) | f | f | f | f | t | f | f | f
+ x is unknown | strictf(x, y) | f | f | t | t | f | f | t | t
+ x is not unknown | strictf(x, y) | t | f | f | f | t | f | f | f
+ x = true | strictf(x, y) | f | f | f | f | t | f | f | f
+ x = false | strictf(x, y) | f | f | f | f | f | f | t | t
+ x | not strictf(x, y) | f | f | f | f | f | f | f | f
+ not x | not strictf(x, y) | f | f | f | f | f | f | f | f
+ strictf(x, y) | not strictf(x, y) | f | f | t | t | f | f | t | t
+ not strictf(x, y) | not strictf(x, y) | t | t | f | f | t | t | f | f
+ x is null | not strictf(x, y) | f | f | t | t | f | f | t | t
+ x is not null | not strictf(x, y) | t | f | f | f | t | f | f | f
+ x is true | not strictf(x, y) | f | f | f | f | f | f | f | f
+ x is not true | not strictf(x, y) | f | f | f | f | f | f | f | f
+ x is false | not strictf(x, y) | f | f | f | f | f | f | f | f
+ x is not false | not strictf(x, y) | f | f | f | f | f | f | f | f
+ x is unknown | not strictf(x, y) | f | f | t | t | f | f | t | t
+ x is not unknown | not strictf(x, y) | t | f | f | f | t | f | f | f
+ x = true | not strictf(x, y) | f | f | f | f | f | f | f | f
+ x = false | not strictf(x, y) | f | f | f | f | f | f | f | f
+ x | x is null | f | f | f | t | f | t | f | t
+ not x | x is null | f | t | f | t | f | t | f | t
+ strictf(x, y) | x is null | f | f | f | t | f | t | f | t
+ not strictf(x, y) | x is null | f | t | f | t | f | t | f | t
+ x is null | x is null | t | t | f | f | t | t | f | f
+ x is not null | x is null | f | f | t | t | f | f | t | t
+ x is true | x is null | f | f | t | t | f | f | t | t
+ x is not true | x is null | f | f | f | f | t | t | f | f
+ x is false | x is null | f | f | t | t | f | f | t | t
+ x is not false | x is null | f | f | f | f | t | t | f | f
+ x is unknown | x is null | t | t | f | f | t | t | f | f
+ x is not unknown | x is null | f | f | t | t | f | f | t | t
+ x = true | x is null | f | f | f | t | f | t | f | t
+ x = false | x is null | f | t | f | t | f | t | f | t
+ x | x is not null | f | f | f | f | f | f | f | f
+ not x | x is not null | f | f | f | f | f | f | f | f
+ strictf(x, y) | x is not null | f | f | f | f | f | f | f | f
+ not strictf(x, y) | x is not null | f | f | f | f | f | f | f | f
+ x is null | x is not null | f | f | t | t | f | f | t | t
+ x is not null | x is not null | t | t | f | f | t | t | f | f
+ x is true | x is not null | f | f | f | f | f | f | f | f
+ x is not true | x is not null | f | f | f | f | f | f | f | f
+ x is false | x is not null | f | f | f | f | f | f | f | f
+ x is not false | x is not null | f | f | f | f | f | f | f | f
+ x is unknown | x is not null | f | f | t | t | f | f | t | t
+ x is not unknown | x is not null | t | t | f | f | t | t | f | f
+ x = true | x is not null | f | f | f | f | f | f | f | f
+ x = false | x is not null | f | f | f | f | f | f | f | f
+ x | x is true | t | t | f | f | t | t | f | f
+ not x | x is true | f | f | t | t | f | f | t | t
+ strictf(x, y) | x is true | f | f | f | f | f | f | f | f
+ not strictf(x, y) | x is true | f | f | f | f | f | f | f | f
+ x is null | x is true | f | f | t | t | f | f | t | t
+ x is not null | x is true | t | t | f | f | t | t | f | f
+ x is true | x is true | t | t | f | f | t | t | f | f
+ x is not true | x is true | f | f | t | t | f | f | t | t
+ x is false | x is true | f | f | t | t | f | f | t | t
+ x is not false | x is true | f | f | f | f | t | t | f | f
+ x is unknown | x is true | f | f | t | t | f | f | t | t
+ x is not unknown | x is true | t | t | f | f | t | t | f | f
+ x = true | x is true | t | t | f | f | t | t | f | f
+ x = false | x is true | f | f | t | t | f | f | t | t
+ x | x is not true | f | f | f | t | f | f | f | t
+ not x | x is not true | f | t | f | f | f | t | f | f
+ strictf(x, y) | x is not true | f | f | f | f | f | f | f | t
+ not strictf(x, y) | x is not true | f | f | f | f | f | t | f | f
+ x is null | x is not true | f | f | f | f | f | f | f | f
+ x is not null | x is not true | f | f | f | f | f | f | f | f
+ x is true | x is not true | f | f | t | t | f | f | t | t
+ x is not true | x is not true | t | t | f | f | t | t | f | f
+ x is false | x is not true | f | f | f | f | f | f | f | f
+ x is not false | x is not true | f | f | f | f | f | f | f | f
+ x is unknown | x is not true | f | f | f | f | f | f | f | f
+ x is not unknown | x is not true | f | f | f | f | f | f | f | f
+ x = true | x is not true | f | f | f | t | f | f | f | t
+ x = false | x is not true | f | t | f | f | f | t | f | f
+ x | x is false | f | f | t | t | f | f | t | t
+ not x | x is false | t | t | f | f | t | t | f | f
+ strictf(x, y) | x is false | f | f | f | f | f | f | f | t
+ not strictf(x, y) | x is false | f | f | f | f | f | t | f | f
+ x is null | x is false | f | f | t | t | f | f | t | t
+ x is not null | x is false | t | t | f | f | t | t | f | f
+ x is true | x is false | f | f | t | t | f | f | t | t
+ x is not true | x is false | f | f | f | f | t | t | f | f
+ x is false | x is false | t | t | f | f | t | t | f | f
+ x is not false | x is false | f | f | t | t | f | f | t | t
+ x is unknown | x is false | f | f | t | t | f | f | t | t
+ x is not unknown | x is false | t | t | f | f | t | t | f | f
+ x = true | x is false | f | f | t | t | f | f | t | t
+ x = false | x is false | t | t | f | f | t | t | f | f
+ x | x is not false | f | t | f | f | f | t | f | f
+ not x | x is not false | f | f | f | f | f | f | f | t
+ strictf(x, y) | x is not false | f | f | f | f | f | f | f | f
+ not strictf(x, y) | x is not false | f | f | f | f | f | f | f | f
+ x is null | x is not false | f | f | f | f | f | f | f | f
+ x is not null | x is not false | f | f | f | f | f | f | f | f
+ x is true | x is not false | f | f | f | f | f | f | f | f
+ x is not true | x is not false | f | f | f | f | f | f | f | f
+ x is false | x is not false | f | f | f | f | f | f | t | t
+ x is not false | x is not false | t | t | f | f | t | t | f | f
+ x is unknown | x is not false | f | f | f | f | f | f | f | f
+ x is not unknown | x is not false | f | f | f | f | f | f | f | f
+ x = true | x is not false | f | t | f | f | f | t | f | f
+ x = false | x is not false | f | f | f | f | f | f | f | t
+ x | x is unknown | f | f | f | t | f | t | f | t
+ not x | x is unknown | f | t | f | t | f | t | f | t
+ strictf(x, y) | x is unknown | f | f | f | t | f | t | f | t
+ not strictf(x, y) | x is unknown | f | t | f | t | f | t | f | t
+ x is null | x is unknown | t | t | f | f | t | t | f | f
+ x is not null | x is unknown | f | f | t | t | f | f | t | t
+ x is true | x is unknown | f | f | t | t | f | f | t | t
+ x is not true | x is unknown | t | t | f | f | t | t | f | f
+ x is false | x is unknown | f | f | t | t | f | f | t | t
+ x is not false | x is unknown | t | t | f | f | t | t | f | f
+ x is unknown | x is unknown | t | t | f | f | t | t | f | f
+ x is not unknown | x is unknown | f | f | t | t | f | f | t | t
+ x = true | x is unknown | f | f | f | t | f | t | f | t
+ x = false | x is unknown | f | t | f | t | f | t | f | t
+ x | x is not unknown | f | f | f | f | f | f | f | f
+ not x | x is not unknown | f | f | f | f | f | f | f | f
+ strictf(x, y) | x is not unknown | f | f | f | f | f | f | f | f
+ not strictf(x, y) | x is not unknown | f | f | f | f | f | f | f | f
+ x is null | x is not unknown | f | f | t | t | f | f | t | t
+ x is not null | x is not unknown | t | t | f | f | t | t | f | f
+ x is true | x is not unknown | f | f | f | f | f | f | f | f
+ x is not true | x is not unknown | f | f | f | f | f | f | f | f
+ x is false | x is not unknown | f | f | f | f | f | f | f | f
+ x is not false | x is not unknown | f | f | f | f | f | f | f | f
+ x is unknown | x is not unknown | f | f | t | t | f | f | t | t
+ x is not unknown | x is not unknown | t | t | f | f | t | t | f | f
+ x = true | x is not unknown | f | f | f | f | f | f | f | f
+ x = false | x is not unknown | f | f | f | f | f | f | f | f
+ x | x = true | t | t | f | f | t | t | f | f
+ not x | x = true | f | f | t | t | f | f | t | t
+ strictf(x, y) | x = true | f | f | f | f | f | f | f | f
+ not strictf(x, y) | x = true | f | f | f | f | f | f | f | f
+ x is null | x = true | f | f | t | t | f | f | t | t
+ x is not null | x = true | t | f | f | f | t | f | f | f
+ x is true | x = true | t | f | f | f | t | f | f | f
+ x is not true | x = true | f | f | t | t | f | f | t | t
+ x is false | x = true | f | f | t | t | f | f | t | t
+ x is not false | x = true | t | t | f | f | t | t | f | f
+ x is unknown | x = true | f | f | t | t | f | f | t | t
+ x is not unknown | x = true | t | f | f | f | t | f | f | f
+ x = true | x = true | t | t | f | f | t | t | f | f
+ x = false | x = true | f | f | t | t | f | f | t | t
+ x | x = false | f | f | t | t | f | f | t | t
+ not x | x = false | t | t | f | f | t | t | f | f
+ strictf(x, y) | x = false | f | f | f | f | f | f | f | t
+ not strictf(x, y) | x = false | f | f | f | f | f | t | f | f
+ x is null | x = false | f | f | t | t | f | f | t | t
+ x is not null | x = false | t | f | f | f | t | f | f | f
+ x is true | x = false | f | f | t | t | f | f | t | t
+ x is not true | x = false | t | t | f | f | t | t | f | f
+ x is false | x = false | t | f | f | f | t | f | f | f
+ x is not false | x = false | f | f | t | t | f | f | t | t
+ x is unknown | x = false | f | f | t | t | f | f | t | t
+ x is not unknown | x = false | t | f | f | f | t | f | f | f
+ x = true | x = false | f | f | t | t | f | f | t | t
+ x = false | x = false | t | t | f | f | t | t | f | f
+(196 rows)
+
diff --git a/src/test/modules/test_predtest/sql/test_all_permutations.sql b/src/test/modules/test_predtest/sql/test_all_permutations.sql
new file mode 100644
index 0000000000..aa57e98498
--- /dev/null
+++ b/src/test/modules/test_predtest/sql/test_all_permutations.sql
@@ -0,0 +1,26 @@
+with clauses(expr) as (
+ values
+ ('x'),
+ ('not x'),
+ ('strictf(x, y)'),
+ ('not strictf(x, y)'),
+ ('x is null'),
+ ('x is not null'),
+ ('x is true'),
+ ('x is not true'),
+ ('x is false'),
+ ('x is not false'),
+ ('x is unknown'),
+ ('x is not unknown'),
+ ('x = true'),
+ ('x = false')
+)
+select p.expr predicate, c.expr clause, t.*
+from clauses p, clauses c
+join lateral (
+ select *
+ from test_predtest(
+ 'select ' || p.expr || ', ' || c.expr ||
+ ' from booleans'
+ )
+) t on true;
--
2.39.3 (Apple Git-145)
