James Coleman <jtc...@gmail.com> writes: > I'm attaching the current version of the patch with the new tests, but > I'm not sure I understand the *_holds results mentioned above. Are > they an artifact of the data under test? Or do they suggest a > remaining bug? I'm a bit fuzzy on what to expect for *_holds though I > understand the requirements for strongly/weakly_implied/refuted_by.
IIRC, the "foo_holds" outputs mean "the foo relationship appears to hold for these expressions across all tested inputs", for instance s_i_holds means "there were no tested cases where A is true and B is not true". The implied_by/refuted_by outputs mean "predtest.c claims it can prove this". Obviously, a claimed proof for a relationship that fails experimentally would be big trouble. The other way around just means that either the proof rules are inadequate to prove this particular case, or the set of test values for the expressions don't expose the fact that the relationship doesn't hold. Now, if we *expected* that predtest.c should be able to prove something, failure to do so would be a bug, but it's not a bug if we know it's incapable of making that proof. The second explanation might represent a bug in the test case. I added the foo_holds columns just as a sort of cross-check on the test cases themselves, they don't test anything about the predtest code. regards, tom lane