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
Branch
------
master
Details
-------
https://git.postgresql.org/pg/commitdiff/a63c3274a68832182f84ca5d2b8cc5a7462bdacb
Modified Files
--------------
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(-)