test_extensions \
test_parser \
test_pg_dump \
+ test_predtest \
test_rbtree \
test_rls_hooks \
test_shm_mq \
--- /dev/null
+# Generated subdirectories
+/log/
+/results/
+/tmp_check/
--- /dev/null
+# 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
--- /dev/null
+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.
--- /dev/null
+CREATE EXTENSION test_predtest;
+-- Make output more legible
+\pset expanded on
+-- Test data
+-- all combinations of four boolean values
+create table booleans as
+select
+ case i%3 when 0 then true when 1 then false else null end as x,
+ case (i/3)%3 when 0 then true when 1 then false else null end as y,
+ case (i/9)%3 when 0 then true when 1 then false else null end as z,
+ case (i/27)%3 when 0 then true when 1 then false else null end as w
+from generate_series(0, 3*3*3*3-1) i;
+-- all combinations of two integers 0..9, plus null
+create table integers as
+select
+ case i%11 when 10 then null else i%11 end as x,
+ case (i/11)%11 when 10 then null else (i/11)%11 end as y
+from generate_series(0, 11*11-1) i;
+-- Basic proof rules for single boolean variables
+select * from test_predtest($$
+select x, 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, 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 not x, 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 not x, 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 x is not null, 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 null, x is null
+from integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 booleans
+$$);
+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 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 | t
+
+select * from test_predtest($$
+select x is false, 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 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
+from booleans
+$$);
+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 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 | 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 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 | t
+w_r_holds | f
+
+select * from test_predtest($$
+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
+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 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 and 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, not x and 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 or y, 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 and y, x
+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 and y, 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 and y, y and 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 y, y and 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 or y, y or 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 or y or z, x or z
+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 z or w, x or y
+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 z and w, x or y
+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, (x and y) or (x and z)
+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 and y) or z, y and 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 or not y) and z, y and 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 y or x, (x or y) and z
+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 and not y, (x or y) and z
+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
+
+-- Tests using btree operator knowledge
+select * from test_predtest($$
+select x <= y, x < y
+from integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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 integers
+$$);
+-[ 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
+
--- /dev/null
+CREATE EXTENSION test_predtest;
+
+-- Make output more legible
+\pset expanded on
+
+-- Test data
+
+-- all combinations of four boolean values
+create table booleans as
+select
+ case i%3 when 0 then true when 1 then false else null end as x,
+ case (i/3)%3 when 0 then true when 1 then false else null end as y,
+ case (i/9)%3 when 0 then true when 1 then false else null end as z,
+ case (i/27)%3 when 0 then true when 1 then false else null end as w
+from generate_series(0, 3*3*3*3-1) i;
+
+-- all combinations of two integers 0..9, plus null
+create table integers as
+select
+ case i%11 when 10 then null else i%11 end as x,
+ case (i/11)%11 when 10 then null else (i/11)%11 end as y
+from generate_series(0, 11*11-1) i;
+
+-- Basic proof rules for single boolean variables
+
+select * from test_predtest($$
+select x, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, not x
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, not x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not null, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is not null, x is null
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, x is not null
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not true, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is not true
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is false, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is false
+from booleans
+$$);
+
+select * from test_predtest($$
+select x is unknown, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is unknown
+from booleans
+$$);
+
+-- XXX seems like we should be able to refute x is null here
+select * from test_predtest($$
+select x is null, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, x is null
+from booleans
+$$);
+
+-- Tests involving AND/OR constructs
+
+select * from test_predtest($$
+select x, x and y
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x, x and y
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, not x and y
+from booleans
+$$);
+
+select * from test_predtest($$
+select x or y, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x and y, x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x and y, not x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x and y, y and x
+from booleans
+$$);
+
+select * from test_predtest($$
+select not y, y and x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x or y, y or x
+from booleans
+$$);
+
+select * from test_predtest($$
+select x or y or z, x or z
+from booleans
+$$);
+
+select * from test_predtest($$
+select z or w, x or y
+from booleans
+$$);
+
+select * from test_predtest($$
+select z and w, x or y
+from booleans
+$$);
+
+select * from test_predtest($$
+select x, (x and y) or (x and z)
+from booleans
+$$);
+
+select * from test_predtest($$
+select (x and y) or z, y and x
+from booleans
+$$);
+
+select * from test_predtest($$
+select (not x or not y) and z, y and x
+from booleans
+$$);
+
+select * from test_predtest($$
+select y or x, (x or y) and z
+from booleans
+$$);
+
+select * from test_predtest($$
+select not x and not y, (x or y) and z
+from booleans
+$$);
+
+-- Tests using btree operator knowledge
+
+select * from test_predtest($$
+select x <= y, x < y
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= y, x > y
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= y, y >= x
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= y, y > x and y < x+2
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= 5, x <= 7
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= 5, x > 7
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= 5, 7 > x
+from integers
+$$);
+
+select * from test_predtest($$
+select 5 >= x, 7 > x
+from integers
+$$);
+
+select * from test_predtest($$
+select 5 >= x, x > 7
+from integers
+$$);
+
+select * from test_predtest($$
+select 5 = x, x = 7
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, x > 7
+from integers
+$$);
+
+select * from test_predtest($$
+select x is not null, int4lt(x,8)
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, x > 7
+from integers
+$$);
+
+select * from test_predtest($$
+select x is null, int4lt(x,8)
+from integers
+$$);
+
+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 integers
+$$);
+
+select * from test_predtest($$
+select x <= 5, x in (1,3,5,7)
+from integers
+$$);
+
+-- XXX ideally, we could prove this case too
+select * from test_predtest($$
+select x <= 5, x in (1,3,5,null)
+from integers
+$$);
+
+select * from test_predtest($$
+select x in (null,1,3,5,7), x in (1,3,5)
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= 5, x < all(array[1,3,5])
+from integers
+$$);
+
+select * from test_predtest($$
+select x <= y, x = any(array[1,3,y])
+from integers
+$$);
--- /dev/null
+/* 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;
--- /dev/null
+/*--------------------------------------------------------------------------
+ *
+ * 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)));
+}
--- /dev/null
+comment = 'Test code for optimizer/util/predtest.c'
+default_version = '1.0'
+module_pathname = '$libdir/test_predtest'
+relocatable = true