On Mon, Apr 1, 2024 at 8:06 AM James Coleman <jtc...@gmail.com> wrote: > > On Mon, Mar 25, 2024 at 5:53 PM Tom Lane <t...@sss.pgh.pa.us> wrote: > > > > James Coleman <jtc...@gmail.com> writes: > > > [ v6 patchset ] > > > > I went ahead and committed 0001 after one more round of review > > > > statements; my bad). I also added the changes in test_predtest.c from > > 0002. I attach a rebased version of 0002, as well as 0003 which isn't > > changed, mainly to keep the cfbot happy. > > > > I'm still not happy with what you did in predicate_refuted_by_recurse: > > it feels wrong and rather expensively so. There has to be a better > > way. Maybe strong vs. weak isn't quite the right formulation for > > refutation tests? > > Possibly. Earlier I'd mused that: > > > Alternatively (to avoid unnecessary CPU burn) we could modify > > predicate_implied_by_recurse (and functionals called by it) to have a > > argument beyond "weak = true/false" Ie.g., an enum that allows for > > something like "WEAK", "STRONG", and "EITHER". That's a bigger change, > > so I didn't want to do that right away unless there was agreement on > > that direction. > > I'm going to try implementing that and see how I feel about what it > looks like in practice.
Attached is v8 which does this. Note that I kept the patch 0001 as before and inserted a new 0002 to show exactly what's changed from the previously version -- I wouldn't expect that to be committed separately, of course. With this change we only need to recurse a single time and can check for both strong and weak refutation when either will do for proving refutation of the "NOT x" construct. Regards, James Coleman
v8-0001-Teach-predtest.c-about-BooleanTest.patch
Description: Binary data
v8-0003-Add-temporary-all-permutations-test.patch
Description: Binary data
v8-0002-Recurse-weak-and-strong-implication-at-the-same-t.patch
Description: Binary data