Refactor predicate_{implied,refuted}_by_simple_clause.

Put the node-type-dependent operations into switches on nodeTag.
This should ease addition of new proof rules for other expression
node types.  There is no functional change, although some tests
are made in a different order than before.

Also, add a couple of new cross-checks in test_predtest.c.

James Coleman (part of a larger patch series)

Discussion: https://postgr.es/m/CAAaqYe8Bo4bf_i6qKj8KBsmHMYXhe3Xt6vOe3OBQnOaf3_XBWg@mail.gmail.com

1 files changed, 29 insertions, 0 deletions

diff --git a/src/test/modules/test_predtest/test_predtest.c b/src/test/modules/test_predtest/test_predtest.c
index 9e6a6471ccf..eaf006c6490 100644
--- a/src/test/modules/test_predtest/test_predtest.c
+++ b/src/test/modules/test_predtest/test_predtest.c
@@ -119,6 +119,22 @@ test_predtest(PG_FUNCTION_ARGS)
 	}
 
 	/*
+	 * Strong refutation implies weak refutation, so we should never observe
+	 * s_r_holds = true with w_r_holds = false.
+	 *
+	 * We can't make a comparable assertion for implication since moving from
+	 * strong to weak implication expands the allowed values of "A" from true
+	 * to either true or NULL.
+	 *
+	 * If this fails it constitutes a bug not with the proofs but with either
+	 * this test module or a more core part of expression evaluation since we
+	 * are validating the logical correctness of the observed result rather
+	 * than the proof.
+	 */
+	if (s_r_holds && !w_r_holds)
+		elog(WARNING, "s_r_holds was true; w_r_holds must not be false");
+
+	/*
 	 * Now, dig the clause querytrees out of the plan, and see what predtest.c
 	 * does with them.
 	 */
@@ -180,6 +196,19 @@ test_predtest(PG_FUNCTION_ARGS)
 		elog(WARNING, "weak_refuted_by result is incorrect");
 
 	/*
+	 * As with our earlier check of the logical consistency of whether strong
+	 * and weak refutation hold, we ought never prove strong refutation
+	 * without also proving weak refutation.
+	 *
+	 * Also as earlier we cannot make the same guarantee about implication
+	 * proofs.
+	 *
+	 * A warning here suggests a bug in the proof code.
+	 */
+	if (strong_refuted_by && !weak_refuted_by)
+		elog(WARNING, "strong_refuted_by was proven; weak_refuted_by should also be proven");
+
+	/*
 	 * Clean up and return a record of the results.
 	 */
 	if (SPI_finish() != SPI_OK_FINISH)