Brian Dunavant <brian@xxxxxxxxxx> writes: > I am using a partial functional index on a table where F(a) = a. Querying > whre F(a) = a hits the index as expected. However the reverse statement a > = F(a) does not. I have verified this in 9.3.4. > Is this a deficiency with the query planner, or are these not actually > equivalent? I've been stumped on it. Interesting. The reason this doesn't work is that predicate_implied_by() fails to prove "a = b" given "b = a", at least in the general case. It will figure that out if either a or b is a constant, but not if neither one is. The fact that it works with constants might explain the lack of previous complaints, but this is still pretty surprising given the amount of knowledge about equality that the system evinces otherwise. (I'm also wondering whether the EquivalenceClass logic might not sometimes rewrite "a = b" into "b = a", causing a failure of this sort even when the user *had* phrased his query consistently.) It would be fairly straightforward to add a proof rule along the lines of "if both expressions are binary opclauses, and the left input expression of each one is equal() to the right input of the other, and the operators are each other's commutators, then the implication holds". An objection might be made that this would add noticeably to the cost of failing proofs, but I think it wouldn't be that bad, especially if we did the syscache lookup for the commutator check last. In most scenarios the equal() checks would fail pretty quickly when the proof rule doesn't apply. Also, I believe that in the case where a or b is a constant, even though we can make the proof already, this approach would succeed noticeably more quickly than btree_predicate_proof() can. (Worth noting also is that predicate_implied_by() isn't even used unless you have things like partial indexes involved, so that its cost is not especially relevant to "simple" queries.) I'd be inclined to add some similar proof rules to predicate_refuted_by, along the lines of "a op1 b refutes a op2 b if op1 is op2's negator" and "a op1 b refutes b op2 a if op1 is the negator of op2's commutator". Again, the code is currently unable to make such deductions unless a or b is a constant. Given the lack of previous complaints, I'm not sure this amounts to a back-patchable bug, but it does seem like something worth fixing going forward. regards, tom lane
