Абстрагирование над группами утверждений в Z3 / SMT-LIB

Попытка объяснить это более описательно,

Операция 1:

x = [[0, 0], [0, 0]]
print(type(x)) # <class 'list'>
print(x) # [[0, 0], [0, 0]]

x[0][0] = 1
print(x) # [[1, 0], [0, 0]]

Операция 2:

y = [[0] * 2] * 2
print(type(y)) # <class 'list'>
print(y) # [[0, 0], [0, 0]]

y[0][0] = 1
print(y) # [[1, 0], [1, 0]]

Заметил, почему не изменяется первый элемент первого списка не изменил второй элемент каждого списка? Это потому, что [0] * 2 действительно представляет собой список из двух чисел, и ссылка на 0 не может быть изменена.

Если вы хотите создать копии клонов, попробуйте выполнить операцию 3:

import copy
y = [0] * 2   
print(y)   # [0, 0]

y = [y, copy.deepcopy(y)]  
print(y) # [[0, 0], [0, 0]]

y[0][0] = 1
print(y) # [[1, 0], [0, 0]]

еще один интересный способ создания копий клонов, операция 4:

import copy
y = [0] * 2
print(y) # [0, 0]

y = [copy.deepcopy(y) for num in range(1,5)]
print(y) # [[0, 0], [0, 0], [0, 0], [0, 0]]

y[0][0] = 5
print(y) # [[5, 0], [0, 0], [0, 0], [0, 0]]