python - sympy 匹配在取模方面有困难

Question

已关注 this StackOverflow question ，和 fix provided by @smichr ，我尝试了以下方法:

>>> from sympy import *
>>> k,m,n = symbols("k m n", integer=True)
>>> (3*k+4)%2 - k%2
0                   # it works with the fix above. Thank you!
>>> p = Wild('p')
>>> q = Wild('q')
>>> e = (2*k+7)%5 + 7*k+7
>>> e
7*k + Mod(2*k + 2, 5) + 7
>>> e.match(p%5+p)
>>> e.match((p+5*q)%5+p)
>>> e.match(p%5+p+5*q)
{q_: k + 1, p_: 2*k + 2}

我希望第一个或第二个 e.match 对我有用(第一个为 {p:7*k+7} ，{p:第二个是 7*k+7,q:-k})，但事实并非如此。这是一个错误吗？如果是，有修复/解决方法吗？

Answer 1

(复制我在 the SymPy issue 上写的相同内容)

match 的数学知识非常有限。它不知道Mod中的2*k可以替换为7*k。

我不确定这个问题是否容易解决。由于数学匹配有限，匹配已经相当复杂。可能需要更好的设计来解决此类问题。实际上，我认为这是需要 SMT 求解器来解决的问题，但也许有更简单的算法可以做到这一点。

抱歉，这并没有给出如何解决问题的直接答案。