¿Cómo definir una matriz?

Question

Parece que Microsoft celebra completamente su sitio web "Rise4Fun" y el Z3 tutorial de Python ya no se carga.

¿Cómo puedo definir definir una matriz en Z3 para Python e imponer algunas restricciones en él?

Answer 1

Un ejemplo: 9x9 matriz de variables enteras

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

Ejemplo: algunas restricciones para la matriz X

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