Fix test_predtest's idea of what weak refutation means.

tglsfdc · tglsfdc · commit a63c3274a688 · 2018-03-08T19:44:23.000-05:00
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
@@ -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
@@ -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;
 	}
 
