I have set up a large table of constraints, as such:
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
]
When I try to solve, two of the equations are giving me issues:
[
c == ((((a_to_n % n) ** kappa) % n) * (a_to_flag % n)) % n,
a_to_p1 % (p * p) != 1,
]
I get a 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 is defined as an Int type, so why does this happen and how do I resolve it?
The problem here is that ** produces a Real number, not an Int, and thus you cannot combine the result with % later on. Here's a simple example to illustrate:
>>> from z3 import *
>>> a, n = Ints('a n')
>>> (a ** n).sort()
Real
That is, the expression a ** n is Real valued; so you cannot take the modulus with an integer later on. To convert back to integer, use ToInt:
>>> ToInt(a ** n).sort()
Int
So, whenever you use **, wrap the result in a call to ToInt to avoid this issue.
Having said that, mixing reals and integers this way will no doubt make your problem quite hard to deal with in z3. I wouldn't be surprised if z3 had very hard time solving your equations, assuming they're not merely constant folding. Perhaps you should simply stick to Real values for everything, which has a decidable theory. (Doesn't mean z3 can answer your queries easily; it just means z3 can decide it if you are willing to wait long enough and have enough computing resources.)