From 316c234154f0aefa98cf0730f66a381b1e07b95a Mon Sep 17 00:00:00 2001 From: jcoleman Date: Thu, 21 Sep 2023 14:34:15 -0400 Subject: [PATCH v1] Teach predtest about IS [NOT] proofs This is particularly helpful for ensuring partial indexes are used. For example: ``` create table foo(i int, bar boolean); create index on foo(i) where bar is true; ``` this change allows the following query to use the index: ``` select * from foo where i = 1 and bar; ``` --- src/backend/optimizer/util/predtest.c | 266 ++++++++- .../test_predtest/expected/test_predtest.out | 539 +++++++++++++++++- .../test_predtest/sql/test_predtest.sql | 196 +++++++ 3 files changed, 990 insertions(+), 11 deletions(-) diff --git a/src/backend/optimizer/util/predtest.c b/src/backend/optimizer/util/predtest.c index fe83e45311..afd0925cd9 100644 --- a/src/backend/optimizer/util/predtest.c +++ b/src/backend/optimizer/util/predtest.c @@ -1162,27 +1162,160 @@ predicate_implied_by_simple_clause(Expr *predicate, Node *clause, } } + /* Similarly check for boolean IS clauses */ + if (IsA(clause, BooleanTest)) + { + BooleanTest *test = (BooleanTest *) clause; + if (test->booltesttype == IS_TRUE) + { + /* X is true implies X */ + if (equal(predicate, test->arg)) + return true; + } + else if (test->booltesttype == IS_FALSE) + { + /* X is false implies NOT X */ + if (is_notclause(predicate) && + equal(get_notclausearg(predicate), test->arg)) + return true; + } + else if (test->booltesttype == IS_NOT_TRUE) + { + /* + * X is not true implies NOT X + * + * We can only prove weak implication here since null is not true + * evaluates to true rather than null. + */ + if (weak && is_notclause(predicate) && + equal(get_notclausearg(predicate), test->arg)) + return true; + } + else if (test->booltesttype == IS_NOT_FALSE) + { + /* + * X is not false implies X + * + * We can only prove weak implication here since null is not false + * evaluates to true rather than null. + */ + if (weak && equal(predicate, test->arg)) + return true; + } + } + + /* + * As well as boolean IS predicates + */ + if (IsA(predicate, BooleanTest)) + { + BooleanTest *test = (BooleanTest *) predicate; + if (test->booltesttype == 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, test->arg)) + return true; + } + else if (test->booltesttype == 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), test->arg)) + return true; + } + else if (test->booltesttype == IS_NOT_TRUE) + { + /* NOT X implies X is not true */ + if (is_notclause(clause) && + equal(get_notclausearg(clause), test->arg)) + return true; + } + else if (test->booltesttype == IS_NOT_FALSE) + { + /* X implies X is not false*/ + if (equal(clause, test->arg)) + return true; + } + else if (test->booltesttype == IS_UNKNOWN) + { + if (IsA(clause, NullTest)) + { + NullTest *ntest = (NullTest *) clause; + + /* X IS NULL implies X is unknown */ + if (ntest->nulltesttype == IS_NULL && + equal(ntest->arg, test->arg)) + return true; + } + } + + if (test->booltesttype == IS_NOT_TRUE + || test->booltesttype == IS_NOT_FALSE) + { + + if (IsA(clause, BooleanTest)) + { + BooleanTest *testclause = (BooleanTest *) clause; + + /* + * X is unknown weakly implies X is not true + * X is unknown weakly implies X is not false + */ + if (weak && testclause->booltesttype == IS_UNKNOWN && + equal(testclause->arg, test->arg)) + return true; + } + } + + } + /* * We could likewise check whether the predicate is boolean equality to a * constant; but there are no known use-cases for that at the moment, * assuming that the predicate has been through constant-folding. */ - /* Next try the IS NOT NULL case */ - if (!weak && - predicate && IsA(predicate, NullTest)) + /* Next try the IS [NOT] NULL cases */ + if (IsA(predicate, NullTest)) { NullTest *ntest = (NullTest *) predicate; - /* row IS NOT NULL does not act in the simple way we have in mind */ - if (ntest->nulltesttype == IS_NOT_NULL && - !ntest->argisrow) + if (IsA(clause, BooleanTest)) { - /* strictness of clause for foo implies foo IS NOT NULL */ - if (clause_is_strict_for(clause, (Node *) ntest->arg, true)) - return true; + BooleanTest* btest = (BooleanTest *) clause; + + if ((ntest->nulltesttype == IS_NOT_NULL && + btest->booltesttype == IS_NOT_UNKNOWN) || + (ntest->nulltesttype == IS_NULL && + btest->booltesttype == IS_UNKNOWN)) + { + if (equal(ntest->arg, btest->arg)) + return true; + } + } + + if (!weak) + { + /* row IS NOT NULL does not act in the simple way we have in mind */ + if (ntest->nulltesttype == IS_NOT_NULL && + !ntest->argisrow) + { + /* strictness of clause for foo implies foo IS NOT NULL */ + if (clause_is_strict_for(clause, (Node *) ntest->arg, true)) + return true; + } + return false; /* we can't succeed below... */ } - return false; /* we can't succeed below... */ } /* Else try operator-related knowledge */ @@ -1272,6 +1405,18 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, equal(((NullTest *) predicate)->arg, isnullarg)) return true; + if (IsA(predicate, BooleanTest)) + { + BooleanTest *testpredicate = (BooleanTest *) predicate; + + /* foo IS NULL refutes foo IS FALSE */ + /* foo IS NULL refutes foo IS TRUE*/ + if ((testpredicate->booltesttype == IS_FALSE || + testpredicate->booltesttype == IS_TRUE) && + equal(testpredicate->arg, isnullarg)) + return true; + } + /* foo IS NULL weakly refutes any predicate that is strict for foo */ if (weak && clause_is_strict_for((Node *) predicate, (Node *) isnullarg, true)) @@ -1280,6 +1425,98 @@ predicate_refuted_by_simple_clause(Expr *predicate, Node *clause, return false; /* we can't succeed below... */ } + /* Try the clause-IS-NOT-NULL case */ + if (clause && IsA(clause, NullTest) && + ((NullTest *) clause)->nulltesttype == IS_NOT_NULL) + { + Expr *isnotnullarg = ((NullTest *) clause)->arg; + + if (IsA(predicate, BooleanTest)) + { + BooleanTest *testpredicate = (BooleanTest *) predicate; + + /* foo IS NOT NULL refutes foo IS UNKNOWN */ + if (testpredicate->booltesttype == IS_UNKNOWN && + equal(testpredicate->arg, isnotnullarg)) + return true; + } + } + + if (IsA(predicate, BooleanTest)) + { + BooleanTest *test = (BooleanTest *) predicate; + + if (test->booltesttype == IS_UNKNOWN) + { + /* + * foo IS NOT UNKNOWN refutes foo IS UNKNOWN is covered by the + * clause strictness check below + */ + + /* strictness of clause for foo refutes foo IS UNKNOWN */ + if (clause_is_strict_for(clause, (Node *) test->arg, true)) + return true; + } + + if (test->booltesttype == IS_TRUE) + { + if (IsA(clause, BooleanTest)) + { + BooleanTest *testclause = (BooleanTest *) clause; + + /* foo IS NOT TRUE refutes foo IS TRUE */ + /* foo IS UNKNOWN refutes foo IS TRUE */ + if ((testclause->booltesttype == IS_NOT_TRUE || + testclause->booltesttype == IS_UNKNOWN) && + equal(test->arg, testclause->arg)) + return true; + } + } + + } + + if (IsA(clause, BooleanTest)) + { + BooleanTest *test = (BooleanTest *) clause; + + if (test->booltesttype == IS_UNKNOWN) + { + if (IsA(predicate, BooleanTest)) + { + BooleanTest *testpredicate= (BooleanTest *) predicate; + + /* foo IS UNKNOWN refutes foo IS TRUE */ + /* foo IS UNKNOWN refutes foo IS NOT UNKNOWN */ + if ((testpredicate->booltesttype == IS_FALSE || + testpredicate->booltesttype == IS_NOT_UNKNOWN) && + equal(testpredicate->arg, test->arg)) + return true; + } + + /* foo IS UNKNOWN weakly refutes any predicate that is strict for foo */ + if (weak && + clause_is_strict_for((Node *) predicate, (Node *) test->arg, true)) + return true; + } + + if (test->booltesttype == IS_TRUE) + { + /* foo IS TRUE refutes NOT foo */ + if (is_notclause(predicate) && + equal(get_notclausearg(predicate), test->arg)) + return true; + } + else if (test->booltesttype == IS_NOT_TRUE) + { + /* foo IS NOT TRUE weakly refutes foo */ + if (weak && equal(predicate, test->arg)) + return true; + } + else if (test->booltesttype == IS_FALSE) + { + } + } + /* Else try operator-related knowledge */ return operator_predicate_proof(predicate, clause, true, weak); } @@ -1500,6 +1737,15 @@ clause_is_strict_for(Node *clause, Node *subexpr, bool allow_false) return clause_is_strict_for(arraynode, subexpr, false); } + if (IsA(clause, BooleanTest)) + { + BooleanTest *test = (BooleanTest *) clause; + + if (test->booltesttype == IS_TRUE || test->booltesttype == IS_FALSE || + test->booltesttype == IS_NOT_UNKNOWN) + return true; + } + /* * 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..ea1272e2cc 100644 --- a/src/test/modules/test_predtest/expected/test_predtest.out +++ b/src/test/modules/test_predtest/expected/test_predtest.out @@ -143,12 +143,194 @@ $$); 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 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 @@ -177,6 +359,62 @@ 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 @@ -199,12 +437,96 @@ $$); 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 +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 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 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 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 | t +s_r_holds | f +w_r_holds | f + +select * from test_predtest($$ +select x is not null, x is 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 | t +s_r_holds | f +w_r_holds | f + -- Assorted not-so-trivial refutation rules select * from test_predtest($$ select x is null, x @@ -234,6 +556,34 @@ w_i_holds | t s_r_holds | f w_r_holds | t +select * from test_predtest($$ +select x is null, 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 x is not unknown, x is null +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 | t +w_r_holds | t + select * from test_predtest($$ select strictf(x,y), x is null from booleans @@ -1094,3 +1444,190 @@ w_i_holds | t s_r_holds | f w_r_holds | t +-- More BooleanTest proofs +-- TODO: some of these are duplicative, but it's easier to see them all in one +-- spot. 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, 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, 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 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..d2eb4bdb5f 100644 --- a/src/test/modules/test_predtest/sql/test_predtest.sql +++ b/src/test/modules/test_predtest/sql/test_predtest.sql @@ -76,6 +76,71 @@ 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 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 +151,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 +181,36 @@ 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 x is null, x is unknown +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 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 +223,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 +565,74 @@ select * from test_predtest($$ select x = all(opaque_array(array[1])), x is null from integers $$); + +-- More BooleanTest proofs +-- TODO: some of these are duplicative, but it's easier to see them all in one +-- spot. 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, x is false +from booleans +$$); + +select * from test_predtest($$ +select x, x is 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 +$$); -- 2.39.3 (Apple Git-145)