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