From 92d81a50cfdcea1a2b3f0000c3a4a79125434faf Mon Sep 17 00:00:00 2001 From: jcoleman Date: Tue, 26 Dec 2023 14:47:15 -0500 Subject: [PATCH v4 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 | 607 +++++++++++-- .../test_predtest/expected/test_predtest.out | 810 +++++++++++++++++- .../test_predtest/sql/test_predtest.sql | 280 ++++++ .../modules/test_predtest/test_predtest.c | 29 + 4 files changed, 1617 insertions(+), 109 deletions(-) diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c index e8c309f358..5a9487c4dd 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,32 +1155,114 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, Assert(list_length(op->args) == 2); rightop = lsecond(op->args); - /* - * We might never see a null Const here, but better check - * anyway - */ - 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)) - { - /* X = true implies X */ - if (equal(predicate, leftop)) - return true; - } + if (constexpr->constisnull) + return false; + + if (DatumGetBool(constexpr->constvalue)) + return equal(predicate, leftop); else - { - /* X = false implies NOT X */ - if (is_notclause(predicate) && - equal(get_notclausearg(predicate), leftop)) - return true; - } + return is_notclause(predicate) && + equal(get_notclausearg(predicate), leftop); } } } 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: + /* + * When the clause is in the form "foo IS NULL" then + * we can prove weak implication of a predicate that + * is strict for "foo" and negated. This doesn't work + * for strong implication since if "foo" is "null" then + * the predicate will evaluate to "null" rather than + * "true". + */ + 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: + /* + * When the clause is in the form "foo IS UNKNOWN" then + * we can prove weak implication of a predicate that + * is strict for "foo" and negated. This doesn't work + * for strong implication since if "foo" is "null" then + * the predicate will evaluate to "null" rather than + * "true". + */ + 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; } @@ -1173,30 +1272,117 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, { case T_NullTest: { - NullTest *ntest = (NullTest *) predicate; + 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 (ntest->nulltesttype) + switch (predntest->nulltesttype) { case IS_NOT_NULL: + 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: /* - * 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. + * X implies X is true + * + * We can only prove strong implication here since + * `null is true` is false rather than null. */ - if (!weak && - !ntest->argisrow && - clause_is_strict_for(clause, (Node *) ntest->arg, true)) + if (!weak && equal(clause, predbtest->arg)) return true; break; - case IS_NULL: + 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 weakly implies X is not true */ + if (weak && 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 weakly implies X is not false */ + if (weak && 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; } } @@ -1213,6 +1399,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 @@ -1242,14 +1532,6 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, return false; /* Our remaining strategies are all clause-type-specific */ - - /* - * A clause "foo IS NULL" refutes a predicate "foo IS NOT NULL" in all - * cases. If we are considering weak refutation, it also refutes a - * predicate that is strict for "foo", since then the predicate must yield - * false or NULL (and since "foo" appears in the predicate, it's known - * immutable). - */ switch (nodeTag(clause)) { case T_NullTest: @@ -1264,36 +1546,132 @@ 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 */ - if (predntest->nulltesttype == IS_NOT_NULL && - equal(predntest->arg, clausentest->arg)) - return true; - } - default: - break; - } + + /* + * When we know what the clause is in the form "foo + * IS NULL" then we can prove refutation of 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 is - * strict for foo */ + * strict for foo; see notes in implication for + * foo IS NOT NULL */ 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: + { + /* + * When we know what the clause is in the form "foo + * IS UNKNOWN" then we can prove refutation of 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; + + /* + * Truth of the clause "foo IS UNKNOWN" tells us + * that "foo" is null, and if the predicate is + * strict for "foo", then "foo" being null will + * mean the predicate will 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; } } @@ -1316,36 +1694,16 @@ 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. + * When we know what the predicate is in the form + * "foo IS NULL" then we can prove strong and weak + * refutation together. This is because the limits + * imposed by weak refutation (allowing "false" + * instead of just "null") is equivalently helpful + * since "foo" being "false" also refutes the + * predicate. Hence we pass weak=false here always. */ - if (clause_is_strict_for(clause, (Node *) predntest->arg, true)) + if (predicate_implied_not_null_by_clause(predntest->arg, clause, false)) return true; return false; /* we can't succeed below... */ @@ -1356,6 +1714,35 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, } } break; + case T_BooleanTest: + { + BooleanTest *predbtest = (BooleanTest *) predicate; + + switch (predbtest->booltesttype) + { + case IS_UNKNOWN: + { + /* + * When we know what the predicate is in the form + * "foo IS UNKNOWN" then we can prove strong and + * weak refutation together. This is because the + * limits imposed by weak refutation (allowing + * "false" instead of just "null") is equivalently + * helpful since "foo" being "false" also refutes + * the predicate. Hence we pass weak=false here + * always. + */ + 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; } @@ -1470,6 +1857,8 @@ clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false) if (equal(clause, subexpr)) return true; + /* TODO: refactor this into switch statements also? */ + /* * If we have a strict operator or function, a NULL result is guaranteed * if any input is forced NULL by subexpr. This is OK even if the op or @@ -1496,6 +1885,15 @@ clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false) return false; } + /* + * We can recurse into "not foo" without any additional processing because + * "not (null)" evaluates to null. That doesn't work for allow_false, + * however, 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 @@ -1583,6 +1981,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..ae43fc9152 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 | f +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 | f +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 d44e66d6f6..f7339fd038 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)