z3 power mod 约束抛出 Z3Exception

Question

我设置了大量 table 约束，例如：

value_n=1319677575750664593269928592823122088231102756079484792845079638972350094036132691958059688916820689747030184510113829740113041751835106779040361964704732781674939111970921386382076965209456061359009064103696057581141587585573457409644899626416953339600078178839886677162434056466419378007334549881514299423667452655244230384294862385143577667675301828094532154331478209619704980444350466007158636501159025323438259949492591777519923746198537834074290240109117233
value_a=342691274423584349791056473125411134098438481683180895903867322580082465637958239934448846612075098614285219068292647847040005389205050272757677433858953494823759242244829180636673330238802274884481886959589470615694177803698174718690765848886907721839332228324388423577817424201793491303906581758910921445168317877902384290187158732544836897687264045955879735934334920222645677067477720579027115764510363046519727124832263309244176383203195395120143396393280178
value_c=966614148477848624030200621625258849031380625915218872283078816676928740125344244698257425964002821854099461580094436358123535723290845114669846893220163142039503329214545667563764436310988727558365456532947041619144359286499858057080380889267035885314605337688144688305837511055021190348080983083350965687703714494963398464234969815079998913589315977406087449734769882954669673024108621512376903207095402574078110055132403183173806026764738715566878703793779398
value_sigma=8464844919528024050776743166493391951099685330616502566136514764715071037185126965166263456592507665693764888945402100735300264199432720007286127252491425
value_tau=10382212427405516607551590772908169835382410408959523296597160297199683505639053103035865826384731049385602808678770211265514520018139117856623297634063128
value_rho=2180308065203712074036416623837957892343118044869765657224934920507007488415740097667016690791656923501004556879088800046225392947371826678430341848539725784764496743600951899723067587234367926146679537689197024965709655834286819439034454072201704826252187806261154259276367446581026005274199093558591833001447262700832466548485390911986069977032843293472245605677321290489737169381053552716457700040526454320831401386889040870267821074531233371107830697865854527


sigma = Int('sigma')
tau = Int('tau')
rho = Int('rho')
random_1340 = Int('random_1340')
random_1160 = Int('random_1160')
random_335 = Int('random_335')
n = Int('n')
a = Int('a')
c = Int('c')
p = Int('p')
q = Int('q')
a_to_n = Int('a_to_n')
a_to_flag = Int('a_to_flag')
a_to_p_1 = Int('a_to_p_1')
kappa = Int('kappa')
flag = Int('flag')
equations = [
    flag < p,
    n == value_n, a == value_a, c == value_c, sigma == value_sigma, tau == value_tau, rho == value_rho,
    a_to_n == a ** n,
    a_to_flag == a ** flag,
    a_to_p_1 == a ** (p-1),
    c == ((((a_to_n % n) ** kappa) % n) * (a_to_flag % n)) % n,
    n == p ** 2 * q,
    kappa >= 1, kappa <= n - 1,
    p > q, 2 * q > p,
    a >= 2, a <= n - 1 , a_to_p1 % (p * p) != 1,
    sigma >= 2, sigma <= q - 1,
    random_1340 >= 1, random_1340 <= 2**1340, random_1160 >= 1, random_1160 <= 2**1160, random_335 >= 1, random_335 <= 2 ** 335,
    tau == (p * p * sigma - random_1340) / q ** 2 + random_335,
    rho == p * p * sigma + q * q * tau + random_1160
]

当我尝试求解时，有两个方程式出现问题：

[
c == ((((a_to_n % n) ** kappa) % n) * (a_to_flag % n)) % n,
a_to_p1 % (p * p) != 1,
]

我得到一个 z3.z3types.Z3Exception: Z3 integer expression expected:

c == ((((a_to_n % n) ** kappa) % n) * (a_to_flag % n)) % n,
  File "/home/retep/.local/lib/python3.8/site-packages/z3/z3.py", line 2411, in __mod__
    _z3_assert(a.is_int(), "Z3 integer expression expected")

A 被定义为 Int 类型，所以 为什么会发生这种情况，我该如何解决？

Answer 1

这里的问题是 ** 产生一个 Real 数字，而不是 Int，因此你不能在以后将结果与 % 组合。这里有一个简单的例子来说明：

>>> from z3 import *
>>> a, n = Ints('a n')
>>> (a ** n).sort()
Real

即表达式a ** n的值为Real；所以你以后不能用整数取模。要转换回整数，请使用 ToInt:

>>> ToInt(a ** n).sort()
Int

因此，每当您使用 ** 时，请将结果包装在对 ToInt 的调用中以避免此问题。

话虽如此，以这种方式混合实数和整数无疑会使您的问题在 z3 中很难处理。如果 z3 很难求解你的方程，我不会感到惊讶，假设它们不仅仅是常数折叠。也许你应该简单地坚持所有事物的 Real 值，这有一个可判定的理论。（并不是说 z3 可以轻松回答你的问题，只是说如果你愿意等待足够长的时间并且有足够的计算资源，z3 可以决定它。）

z3 power mod 约束抛出 Z3Exception

z3 power mod constraint throws Z3Exception

python

z3

z3py