sympy 匹配对模有困难

Question

我尝试了以下操作：

>>> 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

match 的数学知识非常有限。它不知道2*k中的Mod可以替换为7*k。我不确定这是否容易解决。match 已经非常复杂，因为它所做的数学匹配有限。可能需要更好的设计来解决此类问题。实际上，这让我觉得是您需要 SMT 求解器来解决的那种问题，但也许有更简单的算法可以做到这一点。抱歉，这并没有直接回答如何解决问题。