Fix test_predtest's idea of what weak refutation means.

I'd initially supposed that predicate_refuted_by(..., true) ought to
say that "A refutes B" means "non-falsity of A implies non-truth of B".
But it seems better to define it as "truth of A implies non-truth of B".
This is more useful in the current system, slightly easier to prove,
and in closer correspondence to the existing code behavior.

With this change, test_predtest no longer claims that any existing
test cases show false proof reports, though there still are cases
where we could prove something and fail to.

Discussion: https://postgr.es/m/5983.1520487191@sss.pgh.pa.us

diff --git a/src/test/modules/test_predtest/expected/test_predtest.out b/src/test/modules/test_predtest/expected/test_predtest.out
index c2c39f92bc132f85ababf9332080a4e7028dcf67..66fcca7d16183ef2687ace3b4912d9d8ac93ce4c 100644 (file)
--- a/src/test/modules/test_predtest/expected/test_predtest.out
+++ b/src/test/modules/test_predtest/expected/test_predtest.out
@@ -119,7 +119,6 @@ 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
@@ -128,7 +127,7 @@ weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x, x is not true
@@ -176,7 +175,6 @@ 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
@@ -185,7 +183,7 @@ weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x, x is unknown
@@ -214,7 +212,7 @@ weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x, x is null
@@ -650,7 +648,7 @@ weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x is null, int4lt(x,8)
@@ -664,7 +662,7 @@ weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x is not null, x < 'foo'

diff --git a/src/test/modules/test_predtest/test_predtest.c b/src/test/modules/test_predtest/test_predtest.c
index 80ae0c9322ed69fd5f8526b86e2475dfebd81ece..4a3b14a199c889d3a8db850eccf9859e4cd15f0d 100644 (file)
--- a/src/test/modules/test_predtest/test_predtest.c
+++ b/src/test/modules/test_predtest/test_predtest.c
@@ -104,14 +104,18 @@ test_predtest(PG_FUNCTION_ARGS)
                        c2 = 'f';
 
                /* Check for violations of various proof conditions */
+
+               /* strong implication: truth of c2 implies truth of c1 */
                if (c2 == 't' && c1 != 't')
                        s_i_holds = false;
+               /* weak implication: non-falsity of c2 implies non-falsity of c1 */
                if (c2 != 'f' && c1 == 'f')
                        w_i_holds = false;
+               /* strong refutation: truth of c2 implies falsity of c1 */
                if (c2 == 't' && c1 != 'f')
                        s_r_holds = false;
-               /* XXX is this the correct definition for weak refutation? */
-               if (c2 != 'f' && c1 == 't')
+               /* weak refutation: truth of c2 implies non-truth of c1 */
+               if (c2 == 't' && c1 == 't')
                        w_r_holds = false;
        }