From a63c3274a68832182f84ca5d2b8cc5a7462bdacb Mon Sep 17 00:00:00 2001 From: Tom Lane Date: Thu, 8 Mar 2018 19:44:14 -0500 Subject: [PATCH] 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 --- .../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 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; } -- 2.40.0