In the thread about being able to prove constraint exclusion from
an IN clause mentioning a NULL,
https://www.postgresql.org/message-id/flat/3bad48fc-f257-c445-feeb-8a2b2fb622ba@lab.ntt.co.jp
I expressed concern about whether there were existing bugs in predtest.c
given the lack of clarity of the comments around recent changes to it.
I also noticed that coverage.postgresql.org shows we don't have great
test coverage for it. This led me to feel that it'd be worth having
a testbed that would allow directly exercising the predtest code, rather
than having to construct queries whose plans would change depending on
the outcome of a predtest proof.
A bit of hacking later, I have the attached. The set of test cases it
includes at the moment were mostly developed with an eye to getting to
full code coverage of predtest.c, but we could add more later. What's
really interesting is that it proves that the "weak refutation" logic,
i.e. predicate_refuted_by() with clause_is_check = true, is not
self-consistent. Now as far as I can tell, we are not using that
option anywhere yet, so this is just a latent problem not a live one.
Also, it's not very clear what semantics we'd be needing if we did have
a use for the case. Presumably the starting assumption is "clause does
not return false", but do we need to prove "predicate returns false",
or just "predicate does not return true"? I'm not sure, TBH, but if
it's the former then we're going to have results like "X does not refute
NOT X", which seems weird and is certainly not how that code acts now.
So I made the testbed assume that we're supposed to prove ""predicate does
not return true", and the conclusion is that the code mostly behaves
that way, but there are cases where it incorrectly claims a proof, and
more cases where it fails to prove relationships it perhaps could.
I'm not sure that that's worth fixing right now. Instead I'm tempted
to revert the addition of the clause_is_check argument to
predicate_refuted_by, on the grounds that it's both broken and currently
unnecessary.
Anyway, barring objections, I'd like to push this, and then we can use
it to carry a test for the null-in-IN fix whenever that lands.
regards, tom lane
diff --git a/src/test/modules/test_predtest/.gitignore b/src/test/modules/test_predtest/.gitignore
index ...5dcb3ff .
*** a/src/test/modules/test_predtest/.gitignore
--- b/src/test/modules/test_predtest/.gitignore
***************
*** 0 ****
--- 1,4 ----
+ # Generated subdirectories
+ /log/
+ /results/
+ /tmp_check/
diff --git a/src/test/modules/test_predtest/Makefile b/src/test/modules/test_predtest/Makefile
index ...1b50fa3 .
*** a/src/test/modules/test_predtest/Makefile
--- b/src/test/modules/test_predtest/Makefile
***************
*** 0 ****
--- 1,21 ----
+ # src/test/modules/test_predtest/Makefile
+
+ MODULE_big = test_predtest
+ OBJS = test_predtest.o $(WIN32RES)
+ PGFILEDESC = "test_predtest - test code for optimizer/util/predtest.c"
+
+ EXTENSION = test_predtest
+ DATA = test_predtest--1.0.sql
+
+ REGRESS = test_predtest
+
+ ifdef USE_PGXS
+ PG_CONFIG = pg_config
+ PGXS := $(shell $(PG_CONFIG) --pgxs)
+ include $(PGXS)
+ else
+ subdir = src/test/modules/test_predtest
+ top_builddir = ../../../..
+ include $(top_builddir)/src/Makefile.global
+ include $(top_srcdir)/contrib/contrib-global.mk
+ endif
diff --git a/src/test/modules/test_predtest/README b/src/test/modules/test_predtest/README
index ...2c9bec0 .
*** a/src/test/modules/test_predtest/README
--- b/src/test/modules/test_predtest/README
***************
*** 0 ****
--- 1,28 ----
+ test_predtest is a module for checking the correctness of the optimizer's
+ predicate-proof logic, in src/backend/optimizer/util/predtest.c.
+
+ The module provides a function that allows direct application of
+ predtest.c's exposed functions, predicate_implied_by() and
+ predicate_refuted_by(), to arbitrary boolean expressions, with direct
+ inspection of the results. This could be done indirectly by checking
+ planner results, but it can be difficult to construct end-to-end test
+ cases that prove that the expected results were obtained.
+
+ In general, the use of this function is like
+ select * from test_predtest('query string')
+ where the query string must be a SELECT returning two boolean
+ columns, for example
+
+ select * from test_predtest($$
+ select x, not x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ The function parses and plans the given query, and then applies the
+ predtest.c code to the two boolean expressions in the SELECT list, to see
+ if the first expression can be proven or refuted by the second. It also
+ executes the query, and checks the resulting rows to see whether any
+ claimed implication or refutation relationship actually holds. If the
+ query is designed to exercise the expressions on a full set of possible
+ input values, as in the example above, then this provides a mechanical
+ cross-check as to whether the proof code has given a correct answer.
diff --git a/src/test/modules/test_predtest/expected/test_predtest.out
b/src/test/modules/test_predtest/expected/test_predtest.out
index ...60c7852 .
*** a/src/test/modules/test_predtest/expected/test_predtest.out
--- b/src/test/modules/test_predtest/expected/test_predtest.out
***************
*** 0 ****
--- 1,885 ----
+ CREATE EXTENSION test_predtest;
+ -- Make output more legible
+ \pset expanded on
+ -- Basic proof rules for single boolean variables
+ select * from test_predtest($$
+ select x, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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, not x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 not x, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 not x, not x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 null, x is null
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 not null
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ RECORD 1 ]-----+--
+ strong_implied_by | f
+ weak_implied_by | f
+ strong_refuted_by | t
+ weak_refuted_by | f
+ 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
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ WARNING: weak_refuted_by result is incorrect
+ -[ 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 | f
+
+ select * from test_predtest($$
+ select x, x is not true
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 | t
+
+ select * from test_predtest($$
+ select x is false, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 false
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ WARNING: weak_refuted_by result is incorrect
+ -[ 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 | f
+
+ select * from test_predtest($$
+ select x, x is unknown
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 | t
+ s_r_holds | f
+ w_r_holds | t
+
+ -- XXX seems like we should be able to refute x is null here
+ select * from test_predtest($$
+ select x is null, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 | t
+ w_r_holds | f
+
+ select * from test_predtest($$
+ select x, x is null
+ from (values (false), (true), (null)) as v(x)
+ $$);
+ -[ 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 | t
+ s_r_holds | f
+ w_r_holds | t
+
+ -- Tests involving AND/OR constructs
+ select * from test_predtest($$
+ select x, x and y
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 and y
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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, not x and y
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 or y, x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 and y, x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 and y, not x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 and y, y and x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 y, y and x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 or y, y or x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+ -[ 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 or y or z, x or z
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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 z or not z, x or y
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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 | t
+ s_r_holds | f
+ w_r_holds | f
+
+ select * from test_predtest($$
+ select z and z is not unknown, x or y
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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, (x and y) or (x and z)
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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 and y) or z, y and x
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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 or not y) and z, y and x
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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 y or x, (x or y) and z
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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 and not y, (x or y) and z
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+ -[ 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
+
+ -- Tests using btree operator knowledge
+ select * from test_predtest($$
+ select x <= y, x < y
+ from (values
+ (0,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+ -[ 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 <= y, x > y
+ from (values
+ (0,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+ -[ 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 <= y, y >= x
+ from (values
+ (0,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+ -[ 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 <= y, y > x and y < x+2
+ from (values
+ (0,0), (0,1), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+ -[ 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 <= 5, x <= 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 <= 5, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 <= 5, 7 > x
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 5 >= x, 7 > x
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 5 >= x, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 5 = x, x = 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 null, int4lt(x,8)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 null, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ RECORD 1 ]-----+--
+ strong_implied_by | f
+ weak_implied_by | f
+ strong_refuted_by | t
+ weak_refuted_by | f
+ s_i_holds | f
+ w_i_holds | f
+ s_r_holds | t
+ w_r_holds | f
+
+ select * from test_predtest($$
+ select x is null, int4lt(x,8)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ RECORD 1 ]-----+--
+ strong_implied_by | f
+ weak_implied_by | f
+ strong_refuted_by | t
+ weak_refuted_by | f
+ s_i_holds | f
+ w_i_holds | f
+ s_r_holds | t
+ w_r_holds | f
+
+ select * from test_predtest($$
+ select x is not null, x < 'foo'
+ from (values
+ ('aaa'::varchar), ('zzz'::varchar), (null)) as v(x)
+ $$);
+ -[ 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
+
+ -- Cases using ScalarArrayOpExpr
+ select * from test_predtest($$
+ select x <= 5, x in (1,3,5)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 <= 5, x in (1,3,5,7)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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
+
+ -- XXX ideally, we could prove this case too
+ select * from test_predtest($$
+ select x <= 5, x in (1,3,5,null)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ RECORD 1 ]-----+--
+ strong_implied_by | f
+ 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 in (null,1,3,5,7), x in (1,3,5)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 <= 5, x < all(array[1,3,5])
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+ -[ 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 <= y, x = any(array[1,3,y])
+ from (values
+ (0,0), (1,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+ -[ 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
+
diff --git a/src/test/modules/test_predtest/sql/test_predtest.sql
b/src/test/modules/test_predtest/sql/test_predtest.sql
index ...7807c1c .
*** a/src/test/modules/test_predtest/sql/test_predtest.sql
--- b/src/test/modules/test_predtest/sql/test_predtest.sql
***************
*** 0 ****
--- 1,411 ----
+ CREATE EXTENSION test_predtest;
+
+ -- Make output more legible
+ \pset expanded on
+
+ -- Basic proof rules for single boolean variables
+
+ select * from test_predtest($$
+ select x, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x, not x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select not x, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select not x, not x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is not null, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is not null, x is null
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is null, x is not null
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is not true, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x, x is not true
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is false, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x, x is false
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is unknown, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x, x is unknown
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ -- XXX seems like we should be able to refute x is null here
+ select * from test_predtest($$
+ select x is null, x
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x, x is null
+ from (values (false), (true), (null)) as v(x)
+ $$);
+
+ -- Tests involving AND/OR constructs
+
+ select * from test_predtest($$
+ select x, x and y
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select not x, x and y
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x, not x and y
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x or y, x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x and y, x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x and y, not x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x and y, y and x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select not y, y and x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x or y, y or x
+ from (values
+ (false,false), (false,true), (false,null),
+ (true,false), (true,true), (true,null),
+ (null,false), (null,true), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x or y or z, x or z
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select z or not z, x or y
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select z and z is not unknown, x or y
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select x, (x and y) or (x and z)
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select (x and y) or z, y and x
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select (not x or not y) and z, y and x
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select y or x, (x or y) and z
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ select * from test_predtest($$
+ select not x and not y, (x or y) and z
+ from (values
+ (false,false,false), (false,true,false), (false,null,false),
+ (true,false,false), (true,true,false), (true,null,false),
+ (null,false,false), (null,true,false), (null,null,false),
+ (false,false,true), (false,true,true), (false,null,true),
+ (true,false,true), (true,true,true), (true,null,true),
+ (null,false,true), (null,true,true), (null,null,true),
+ (false,false,null), (false,true,null), (false,null,null),
+ (true,false,null), (true,true,null), (true,null,null),
+ (null,false,null), (null,true,null), (null,null,null)) as v(x,y,z)
+ $$);
+
+ -- Tests using btree operator knowledge
+
+ select * from test_predtest($$
+ select x <= y, x < y
+ from (values
+ (0,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x <= y, x > y
+ from (values
+ (0,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x <= y, y >= x
+ from (values
+ (0,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x <= y, y > x and y < x+2
+ from (values
+ (0,0), (0,1), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
+
+ select * from test_predtest($$
+ select x <= 5, x <= 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x <= 5, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x <= 5, 7 > x
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select 5 >= x, 7 > x
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select 5 >= x, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select 5 = x, x = 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is not null, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is not null, int4lt(x,8)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is null, x > 7
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is null, int4lt(x,8)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x is not null, x < 'foo'
+ from (values
+ ('aaa'::varchar), ('zzz'::varchar), (null)) as v(x)
+ $$);
+
+ -- Cases using ScalarArrayOpExpr
+
+ select * from test_predtest($$
+ select x <= 5, x in (1,3,5)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x <= 5, x in (1,3,5,7)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ -- XXX ideally, we could prove this case too
+ select * from test_predtest($$
+ select x <= 5, x in (1,3,5,null)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x in (null,1,3,5,7), x in (1,3,5)
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x <= 5, x < all(array[1,3,5])
+ from (values
+ (0), (5), (6), (7), (10), (null)) as v(x)
+ $$);
+
+ select * from test_predtest($$
+ select x <= y, x = any(array[1,3,y])
+ from (values
+ (0,0), (1,0), (0,7), (0,null),
+ (7,0), (7,7), (7,null),
+ (null,0), (null,7), (null,null)) as v(x,y)
+ $$);
diff --git a/src/test/modules/test_predtest/test_predtest--1.0.sql
b/src/test/modules/test_predtest/test_predtest--1.0.sql
index ...11e1444 .
*** a/src/test/modules/test_predtest/test_predtest--1.0.sql
--- b/src/test/modules/test_predtest/test_predtest--1.0.sql
***************
*** 0 ****
--- 1,16 ----
+ /* src/test/modules/test_predtest/test_predtest--1.0.sql */
+
+ -- complain if script is sourced in psql, rather than via CREATE EXTENSION
+ \echo Use "CREATE EXTENSION test_predtest" to load this file. \quit
+
+ CREATE FUNCTION test_predtest(query text,
+ OUT strong_implied_by bool,
+ OUT weak_implied_by bool,
+ OUT strong_refuted_by bool,
+ OUT weak_refuted_by bool,
+ OUT s_i_holds bool,
+ OUT w_i_holds bool,
+ OUT s_r_holds bool,
+ OUT w_r_holds bool)
+ STRICT
+ AS 'MODULE_PATHNAME' LANGUAGE C;
diff --git a/src/test/modules/test_predtest/test_predtest.c b/src/test/modules/test_predtest/test_predtest.c
index ...80ae0c9 .
*** a/src/test/modules/test_predtest/test_predtest.c
--- b/src/test/modules/test_predtest/test_predtest.c
***************
*** 0 ****
--- 1,215 ----
+ /*--------------------------------------------------------------------------
+ *
+ * test_predtest.c
+ * Test correctness of optimizer's predicate proof logic.
+ *
+ * Copyright (c) 2018, PostgreSQL Global Development Group
+ *
+ * IDENTIFICATION
+ * src/test/modules/test_predtest/test_predtest.c
+ *
+ * -------------------------------------------------------------------------
+ */
+
+ #include "postgres.h"
+
+ #include "access/htup_details.h"
+ #include "catalog/pg_type.h"
+ #include "executor/spi.h"
+ #include "funcapi.h"
+ #include "optimizer/clauses.h"
+ #include "optimizer/predtest.h"
+ #include "optimizer/prep.h"
+ #include "utils/builtins.h"
+
+ PG_MODULE_MAGIC;
+
+ /*
+ * test_predtest(query text) returns record
+ */
+ PG_FUNCTION_INFO_V1(test_predtest);
+
+ Datum
+ test_predtest(PG_FUNCTION_ARGS)
+ {
+ text *txt = PG_GETARG_TEXT_PP(0);
+ char *query_string = text_to_cstring(txt);
+ SPIPlanPtr spiplan;
+ int spirc;
+ TupleDesc tupdesc;
+ bool s_i_holds,
+ w_i_holds,
+ s_r_holds,
+ w_r_holds;
+ CachedPlan *cplan;
+ PlannedStmt *stmt;
+ Plan *plan;
+ Expr *clause1;
+ Expr *clause2;
+ bool strong_implied_by,
+ weak_implied_by,
+ strong_refuted_by,
+ weak_refuted_by;
+ Datum values[8];
+ bool nulls[8];
+ int i;
+
+ /* We use SPI to parse, plan, and execute the test query */
+ if (SPI_connect() != SPI_OK_CONNECT)
+ elog(ERROR, "SPI_connect failed");
+
+ /*
+ * First, plan and execute the query, and inspect the results. To the
+ * extent that the query fully exercises the two expressions, this
+ * provides an experimental indication of whether implication or
+ * refutation holds.
+ */
+ spiplan = SPI_prepare(query_string, 0, NULL);
+ if (spiplan == NULL)
+ elog(ERROR, "SPI_prepare failed for \"%s\"", query_string);
+
+ spirc = SPI_execute_plan(spiplan, NULL, NULL, true, 0);
+ if (spirc != SPI_OK_SELECT)
+ elog(ERROR, "failed to execute \"%s\"", query_string);
+ tupdesc = SPI_tuptable->tupdesc;
+ if (tupdesc->natts != 2 ||
+ TupleDescAttr(tupdesc, 0)->atttypid != BOOLOID ||
+ TupleDescAttr(tupdesc, 1)->atttypid != BOOLOID)
+ elog(ERROR, "query must yield two boolean columns");
+
+ s_i_holds = w_i_holds = s_r_holds = w_r_holds = true;
+ for (i = 0; i < SPI_processed; i++)
+ {
+ HeapTuple tup = SPI_tuptable->vals[i];
+ Datum dat;
+ bool isnull;
+ char c1,
+ c2;
+
+ /* Extract column values in a 3-way representation */
+ dat = SPI_getbinval(tup, tupdesc, 1, &isnull);
+ if (isnull)
+ c1 = 'n';
+ else if (DatumGetBool(dat))
+ c1 = 't';
+ else
+ c1 = 'f';
+
+ dat = SPI_getbinval(tup, tupdesc, 2, &isnull);
+ if (isnull)
+ c2 = 'n';
+ else if (DatumGetBool(dat))
+ c2 = 't';
+ else
+ c2 = 'f';
+
+ /* Check for violations of various proof conditions */
+ if (c2 == 't' && c1 != 't')
+ s_i_holds = false;
+ if (c2 != 'f' && c1 == 'f')
+ w_i_holds = false;
+ if (c2 == 't' && c1 != 'f')
+ s_r_holds = false;
+ /* XXX is this the correct definition for weak refutation? */
+ if (c2 != 'f' && c1 == 't')
+ w_r_holds = false;
+ }
+
+ /*
+ * Now, dig the clause querytrees out of the plan, and see what predtest.c
+ * does with them.
+ */
+ cplan = SPI_plan_get_cached_plan(spiplan);
+
+ if (list_length(cplan->stmt_list) != 1)
+ elog(ERROR, "failed to decipher query plan");
+ stmt = linitial_node(PlannedStmt, cplan->stmt_list);
+ if (stmt->commandType != CMD_SELECT)
+ elog(ERROR, "failed to decipher query plan");
+ plan = stmt->planTree;
+ Assert(list_length(plan->targetlist) >= 2);
+ clause1 = castNode(TargetEntry, linitial(plan->targetlist))->expr;
+ clause2 = castNode(TargetEntry, lsecond(plan->targetlist))->expr;
+
+ /*
+ * Because the clauses are in the SELECT list, preprocess_expression did
+ * not pass them through canonicalize_qual nor make_ands_implicit. We can
+ * do that here, though, and should do so to match the planner's normal
+ * usage of the predicate proof functions.
+ *
+ * This still does not exactly duplicate the normal usage of the proof
+ * functions, in that they are often given qual clauses containing
+ * RestrictInfo nodes. But since predtest.c just looks through those
+ * anyway, it seems OK to not worry about that point.
+ */
+ clause1 = canonicalize_qual(clause1);
+ clause2 = canonicalize_qual(clause2);
+
+ clause1 = (Expr *) make_ands_implicit(clause1);
+ clause2 = (Expr *) make_ands_implicit(clause2);
+
+ strong_implied_by = predicate_implied_by((List *) clause1,
+ (List *) clause2,
+ false);
+
+ weak_implied_by = predicate_implied_by((List *) clause1,
+ (List *) clause2,
+ true);
+
+ strong_refuted_by = predicate_refuted_by((List *) clause1,
+ (List *) clause2,
+ false);
+
+ weak_refuted_by = predicate_refuted_by((List *) clause1,
+ (List *) clause2,
+ true);
+
+ /*
+ * Issue warning if any proof is demonstrably incorrect.
+ */
+ if (strong_implied_by && !s_i_holds)
+ elog(WARNING, "strong_implied_by result is incorrect");
+ if (weak_implied_by && !w_i_holds)
+ elog(WARNING, "weak_implied_by result is incorrect");
+ if (strong_refuted_by && !s_r_holds)
+ elog(WARNING, "strong_refuted_by result is incorrect");
+ if (weak_refuted_by && !w_r_holds)
+ elog(WARNING, "weak_refuted_by result is incorrect");
+
+ /*
+ * Clean up and return a record of the results.
+ */
+ if (SPI_finish() != SPI_OK_FINISH)
+ elog(ERROR, "SPI_finish failed");
+
+ tupdesc = CreateTemplateTupleDesc(8, false);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 1,
+ "strong_implied_by", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 2,
+ "weak_implied_by", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 3,
+ "strong_refuted_by", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 4,
+ "weak_refuted_by", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 5,
+ "s_i_holds", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 6,
+ "w_i_holds", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 7,
+ "s_r_holds", BOOLOID, -1, 0);
+ TupleDescInitEntry(tupdesc, (AttrNumber) 8,
+ "w_r_holds", BOOLOID, -1, 0);
+ tupdesc = BlessTupleDesc(tupdesc);
+
+ MemSet(nulls, 0, sizeof(nulls));
+ values[0] = BoolGetDatum(strong_implied_by);
+ values[1] = BoolGetDatum(weak_implied_by);
+ values[2] = BoolGetDatum(strong_refuted_by);
+ values[3] = BoolGetDatum(weak_refuted_by);
+ values[4] = BoolGetDatum(s_i_holds);
+ values[5] = BoolGetDatum(w_i_holds);
+ values[6] = BoolGetDatum(s_r_holds);
+ values[7] = BoolGetDatum(w_r_holds);
+
+ PG_RETURN_DATUM(HeapTupleGetDatum(heap_form_tuple(tupdesc, values, nulls)));
+ }
diff --git a/src/test/modules/test_predtest/test_predtest.control
b/src/test/modules/test_predtest/test_predtest.control
index ...a899a9d .
*** a/src/test/modules/test_predtest/test_predtest.control
--- b/src/test/modules/test_predtest/test_predtest.control
***************
*** 0 ****
--- 1,4 ----
+ comment = 'Test code for optimizer/util/predtest.c'
+ default_version = '1.0'
+ module_pathname = '$libdir/test_predtest'
+ relocatable = true
