From other questions, i knew how to convert a 1-d list to an array. The function “Store” inside can finish this. However, i would like to get a general method to do this job. I don’t know how many dimensions the array has, and I don’t know the size of each dimension in the array.

Here’s an example to explain my question:

i, j = Ints('i j')
L = [[0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0]]
A = Array('A',IntSort(),ArraySort(IntSort(), IntSort()))

I need to make the array A equal the list L, because i will add some constraints like this:

s = Solver()
s.add(FORALL([i,j],Implies(And(i>=0, i<9, j>=0, j<3), A[i][j]>=0)))

if I use the list L to do this:
s.add(FORALL([i,j],Implies(And(i>=0, i<9, j>=0, j<3), L[i][j]>=0)))
z3 reported below error messages:

s.add(ForAll([i,j],Implies(And(i>=0, i<9, j>=0, j<3), VG[i][j]>=0)))
                                                          ~~^^^
TypeError: list indices must be integers or slices, not ArithRef

I searched for information about this error message on stackoverflow, like this Error with quantifier in Z3Py but when the list have more dimensions, this method doesn’t seems to work.