Testbed for predtest.c ... and some arguable bugs therein

In the thread about being able to prove constraint exclusion from
an IN clause mentioning a NULL,
https://www.postgresql.org/message-id/flat/3bad48fc-f257-c445-feeb-8a2b2fb622ba(at)lab(dot)ntt(dot)co(dot)jp
I expressed concern about whether there were existing bugs in predtest.c
given the lack of clarity of the comments around recent changes to it.
I also noticed that coverage.postgresql.org shows we don't have great
test coverage for it. This led me to feel that it'd be worth having
a testbed that would allow directly exercising the predtest code, rather
than having to construct queries whose plans would change depending on
the outcome of a predtest proof.

A bit of hacking later, I have the attached. The set of test cases it
includes at the moment were mostly developed with an eye to getting to
full code coverage of predtest.c, but we could add more later. What's
really interesting is that it proves that the "weak refutation" logic,
i.e. predicate_refuted_by() with clause_is_check = true, is not
self-consistent. Now as far as I can tell, we are not using that
option anywhere yet, so this is just a latent problem not a live one.
Also, it's not very clear what semantics we'd be needing if we did have
a use for the case. Presumably the starting assumption is "clause does
not return false", but do we need to prove "predicate returns false",
or just "predicate does not return true"? I'm not sure, TBH, but if
it's the former then we're going to have results like "X does not refute
NOT X", which seems weird and is certainly not how that code acts now.
So I made the testbed assume that we're supposed to prove ""predicate does
not return true", and the conclusion is that the code mostly behaves
that way, but there are cases where it incorrectly claims a proof, and
more cases where it fails to prove relationships it perhaps could.

I'm not sure that that's worth fixing right now. Instead I'm tempted
to revert the addition of the clause_is_check argument to
predicate_refuted_by, on the grounds that it's both broken and currently
unnecessary.

Anyway, barring objections, I'd like to push this, and then we can use
it to carry a test for the null-in-IN fix whenever that lands.

regards, tom lane