z3 power mod 约束抛出 Z3Exception

如何解决z3 power mod 约束抛出 Z3Exception

我已经建立了一个很大的约束表，例如：

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

我得到一个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 类型，那么为什么会发生这种情况，我该如何解决？

解决方法

这里的问题是 ** 产生的是 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 可以决定它。）