From b4d82f8abfe53f90707773f142be6cf4ecb61838 Mon Sep 17 00:00:00 2001 From: jcoleman Date: Mon, 1 Apr 2024 08:11:29 -0400 Subject: [PATCH 1/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 | 612 +++++++++++-- .../test_predtest/expected/test_predtest.out | 810 +++++++++++++++++- .../test_predtest/sql/test_predtest.sql | 280 ++++++ 3 files changed, 1599 insertions(+), 103 deletions(-) diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c index ac28573cd0a5..7af098e4d5b7 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 6d21bcd603ee..7a01fe1252bc 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 072eb5b0d502..6a3c01dbf3ac 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 c37f6317534ebb2156a7a9956fe71402ad4d5ecf Mon Sep 17 00:00:00 2001 From: jcoleman Date: Fri, 5 Apr 2024 18:33:02 -0400 Subject: [PATCH 2/3] Recurse weak and strong implication at the same time This is particularly useful for implication as used in refutation proofs with "NOT x" clauses. We don't plumb through external callers this way since they are generally interested in one or the other. --- src/backend/optimizer/util/predtest.c | 97 ++++++++++++++------------- 1 file changed, 51 insertions(+), 46 deletions(-) diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c index 7af098e4d5b7..534f98ee5756 100644 --- a/src/backend/optimizer/util/predtest.c +++ b/src/backend/optimizer/util/predtest.c @@ -79,9 +79,12 @@ typedef struct PredIterInfoData (info).cleanup_fn(&(info)); \ } while (0) +typedef int ImplicationType; +#define STRONG ((ImplicationType) 0x01) +#define WEAK ((ImplicationType) 0x02) static bool predicate_implied_by_recurse(Node *clause, Node *predicate, - bool weak); + ImplicationType implication_mask); static bool predicate_refuted_by_recurse(Node *clause, Node *predicate, bool weak); static PredClass predicate_classify(Node *clause, PredIterInfo info); @@ -96,11 +99,11 @@ static void arrayexpr_startup_fn(Node *clause, PredIterInfo info); static Node *arrayexpr_next_fn(PredIterInfo info); static void arrayexpr_cleanup_fn(PredIterInfo info); static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause, - bool weak); + ImplicationType implication_mask); 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); + ImplicationType implication_mask); 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); @@ -178,7 +181,7 @@ predicate_implied_by(List *predicate_list, List *clause_list, c = (Node *) clause_list; /* And away we go ... */ - return predicate_implied_by_recurse(c, p, weak); + return predicate_implied_by_recurse(c, p, weak ? WEAK : STRONG); } /* @@ -295,7 +298,7 @@ predicate_refuted_by(List *predicate_list, List *clause_list, */ static bool predicate_implied_by_recurse(Node *clause, Node *predicate, - bool weak) + ImplicationType implication_mask) { PredIterInfoData clause_info; PredIterInfoData pred_info; @@ -323,7 +326,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(pitem, predicate, pred_info) { if (!predicate_implied_by_recurse(clause, pitem, - weak)) + implication_mask)) { result = false; break; @@ -343,7 +346,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(pitem, predicate, pred_info) { if (predicate_implied_by_recurse(clause, pitem, - weak)) + implication_mask)) { result = true; break; @@ -361,7 +364,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(citem, clause, clause_info) { if (predicate_implied_by_recurse(citem, predicate, - weak)) + implication_mask)) { result = true; break; @@ -379,7 +382,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(citem, clause, clause_info) { if (predicate_implied_by_recurse(citem, predicate, - weak)) + implication_mask)) { result = true; break; @@ -407,7 +410,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(pitem, predicate, pred_info) { if (predicate_implied_by_recurse(citem, pitem, - weak)) + implication_mask)) { presult = true; break; @@ -435,7 +438,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(citem, clause, clause_info) { if (!predicate_implied_by_recurse(citem, predicate, - weak)) + implication_mask)) { result = false; break; @@ -458,7 +461,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(pitem, predicate, pred_info) { if (!predicate_implied_by_recurse(clause, pitem, - weak)) + implication_mask)) { result = false; break; @@ -476,7 +479,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, iterate_begin(pitem, predicate, pred_info) { if (predicate_implied_by_recurse(clause, pitem, - weak)) + implication_mask)) { result = true; break; @@ -493,7 +496,7 @@ predicate_implied_by_recurse(Node *clause, Node *predicate, return predicate_implied_by_simple_clause((Expr *) predicate, clause, - weak); + implication_mask); } break; } @@ -627,7 +630,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate, not_arg = extract_not_arg(predicate); if (not_arg && predicate_implied_by_recurse(clause, not_arg, - false)) + STRONG)) return true; /* @@ -709,7 +712,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate, not_arg = extract_not_arg(predicate); if (not_arg && predicate_implied_by_recurse(clause, not_arg, - false)) + STRONG)) return true; /* @@ -736,26 +739,24 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate, * If A is a strong NOT-clause, A R=> B if B => A's arg * * Since A is strong, we may assume A's arg is false (not just - * not-true). If B weakly implies A's arg, then B can be neither - * true nor null, so that strong refutation is proven. If B - * strongly implies A's arg, then B cannot be true, so that weak - * refutation is proven. + * not-true). If B strongly implies A's arg, then B cannot be true, + * so that weak refutation is proven. If B weakly implies A's arg, + * then B can be neither true nor null, so that strong refutation + * are proven. In that case we can also prove weak refutation since + * if B must be false, then surely it is not true. */ not_arg = extract_strong_not_arg(clause); - if (not_arg && - predicate_implied_by_recurse(predicate, not_arg, - !weak)) - return true; + if (not_arg) + { + int useful_implications = weak ? STRONG : WEAK; - /* - * 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; + if (weak) + useful_implications |= WEAK; + + if (predicate_implied_by_recurse(predicate, not_arg, + useful_implications)) + return true; + } switch (pclass) { @@ -805,7 +806,7 @@ predicate_refuted_by_recurse(Node *clause, Node *predicate, not_arg = extract_not_arg(predicate); if (not_arg && predicate_implied_by_recurse(clause, not_arg, - false)) + STRONG)) return true; /* @@ -1113,8 +1114,12 @@ arrayexpr_cleanup_fn(PredIterInfo info) */ static bool predicate_implied_by_simple_clause(Expr *predicate, Node *clause, - bool weak) + ImplicationType implication_mask) { + bool weak = implication_mask & WEAK; + bool strong = implication_mask & STRONG; + + /* Allow interrupting long proof attempts */ CHECK_FOR_INTERRUPTS(); @@ -1302,7 +1307,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, * must be not null. */ if (predicate_implied_not_null_by_clause(predntest->arg, - clause, weak)) + clause, implication_mask)) return true; break; case IS_NULL: @@ -1332,7 +1337,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, * We can only prove strong implication here since * "null is true" is false rather than null. */ - if (!weak && equal(clause, predbtest->arg)) + if (strong && equal(clause, predbtest->arg)) return true; break; case IS_FALSE: @@ -1342,7 +1347,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, * We can only prove strong implication here since "not * null" is null rather than true. */ - if (!weak && is_notclause(clause) && + if (strong && is_notclause(clause) && equal(get_notclausearg(clause), predbtest->arg)) return true; break; @@ -1401,7 +1406,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, * * For example: truth of x implies x is not unknown. */ - if (predicate_implied_not_null_by_clause(predbtest->arg, clause, weak)) + if (predicate_implied_not_null_by_clause(predbtest->arg, clause, implication_mask)) return true; break; } @@ -1444,7 +1449,7 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, * cycles on at this point. */ static bool -predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, bool weak) +predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, ImplicationType implication_mask) { switch (nodeTag(clause)) { @@ -1517,7 +1522,7 @@ predicate_implied_not_null_by_clause(Expr *predicate, Node *clause, bool weak) * 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)) + if (implication_mask & STRONG && clause_is_strict_for(clause, (Node *) predicate, true)) return true; return false; @@ -1578,7 +1583,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, * = 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)) + if (predicate_implied_not_null_by_clause(clausentest->arg, (Node *) predicate, WEAK)) return true; /* @@ -1588,7 +1593,7 @@ 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, WEAK)) return true; return false; /* we can't succeed below... */ @@ -1665,7 +1670,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, * = 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)) + if (predicate_implied_not_null_by_clause(clausebtest->arg, (Node *) predicate, WEAK)) return true; /* @@ -1728,7 +1733,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, * refutation is a strict superset of weak * refutation. */ - if (predicate_implied_not_null_by_clause(predntest->arg, clause, false)) + if (predicate_implied_not_null_by_clause(predntest->arg, clause, STRONG)) return true; } break; @@ -1759,7 +1764,7 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, * refutation is a strict superset of weak * refutation. */ - if (predicate_implied_not_null_by_clause(predbtest->arg, clause, false)) + if (predicate_implied_not_null_by_clause(predbtest->arg, clause, STRONG)) return true; return false; /* we can't succeed below... */ From ce09fd5ff8b88b873a07a4f8006915ebcde59bd9 Mon Sep 17 00:00:00 2001 From: jcoleman Date: Mon, 15 Jan 2024 09:00:14 -0500 Subject: [PATCH 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 a235e2aac9c5..5416350844ef 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 000000000000..a27b2cfcffde --- /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 000000000000..aa57e98498f4 --- /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;