postgres.git / summary / log / commit / refs

commit    a63c3274a68832182f84ca5d2b8cc5a7462bdacb
Author:   Tom Lane <tgl@sss.pgh.pa.us>
Date:     Fri Mar 09 00:44:14 2018 +0000
First released in: 11.0

    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


 src/test/modules/test_predtest/expected/test_predtest.out | 12 +++++-------
 src/test/modules/test_predtest/test_predtest.c            |  8 ++++++--
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/test/modules/test_predtest/expected/test_predtest.out b/src/test/modules/test_predtest/expected/test_predtest.out
index c2c39f92bc1..66fcca7d161 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 80ae0c9322e..4a3b14a199c 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;
 	}
 


[parent: 960df2a9715c]