Come definire una matrice?

Question

Sembra che Microsoft completamente avvolga il loro sito web "Rise4fun" e il tutorial Z3 Python non carichi più.

Come posso definire Definire una matrice in Z3 per Python e imporre alcuni vincoli su di esso?

Answer 1

Un esempio: 9x9 matrice di variabili integer

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

.

Esempio: alcuni vincoli per la matrice x

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

.