python - How to define a matrix?

Question

It looks like Microsoft completely pooched their "rise4fun" website and the Z3 Python tutorial no longer loads.

How can I define define a matrix in Z3 for Python and impose some constraints on it?

Answer 1

一个例子：9x9 整数变量矩阵

X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ] 
  for i in range(9) ]

示例：矩阵 X 的一些约束

cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9) 
         for i in range(9) for j in range(9) ]