ntheory.AskEvenHandler.Mul is order-dependent

[toolforger]

ask(Q.even(x*y*(y + z)), Q.integer(x) & Q.integer(y) & Q.odd(z)) is supposed to give True (the ability to infer that y*(y+z) for odd z was introduced in e91f8f0 by @skirpichev).
However, some permutations of x, y, and (y + z) will fail because the code will not recognize that y and (y + z) combine in a relevant fashion if it sees x between the two.

Fixing this would require checking all combinations of two terms.
That's O(N^2) for N = number of terms.
So either N needs to be limited, or the list of term combinations to check would need to exclude those that cannot contribute to the answer.

[toolforger]

I spoke too soon - preparing the test case revealed that all permutations work with the old ordering_of_classes sort order, and none with the new, class-name based one.
It's still related to terms being fed to the comparison loop in an unexpected order, but the order in which terms are fed to the comparison loop seems to happen after some internal sorting step.

More analysis is needed.

[skirpichev]

However, some permutations of x, y, and (y + z) will fail

Did you know about sorting?

Fixing this would require checking all combinations of two terms.

Or not count this as a bug at all. If something work differently in non-canonical form, i.e. for unevaluated Mul like Mul(y, x, (y + z), evaluate=False) - not necessary it's a bug.

More analysis is needed.

How sorted results looks now? I think, if they look differently from x*y*(y + z) - this is a real bug.

[skirpichev]

unsubscribed. mention me, if you want reply

[toolforger]

Didn't have to do more detailed analysis, renaming x and y got me a None even in current master. (I didn't know that the terms would be sorted before the ask handler would see them. Once I found that out, I could trigger a changed sort order by renaming symbols.)
Added a PR for a new unit test to demonstrate the problem, see #9130 .
@skirpichev so you know.

[skirpichev]

Didn't have to do more detailed analysis, renaming x and y got me a None even in current master.

I admit, this looks as a bug for me. And same "works" for old assumptions.

Fixing wouldn't require checking all terms - you should do care only about special ones, i.e. Add instances.

I didn't know that the terms would be sorted before the ask handler

I'm sure you know that Python uses eager evaluation rules. So, constructor for Mul must be called before Q.even. Mul have some canonicalization logic in it's constructor (i.e. Mul.flatten and so on) and that include sorting.