From: Tom Lane <tgl@sss.pgh.pa.us>
Date: Fri, 9 Mar 2018 00:44:14 +0000 (-0500)
Subject: Fix test_predtest's idea of what weak refutation means.
X-Git-Tag: REL_11_BETA1~626
X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=a63c3274a68832182f84ca5d2b8cc5a7462bdacb;p=postgresql

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 c2c39f92bc..66fcca7d16 100644
--- 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 80ae0c9322..4a3b14a199 100644
--- 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;
 	}