Как объявить массив со смешанными типами данных в Z3?
Я использую API Python для z3, и моя цель — иметь возможность рассуждать о последовательностях, содержащих один из двух типов данных: либо целое число, либо мой пользовательский тип данных, который не имеет никаких свойств, кроме типа. Я читал об «DeclareSort», что, похоже, означает, что мы можем создать собственный тип. Поэтому я использовал его следующим образом:
ct = DeclareSort('CT')
CT = Const('CT', ct)
Затем я попытался создать тип объединения между моим типом и целыми числами следующим образом:
u = Datatype('IntOrCT')
u.declare('IntV', ('int', IntSort()))
u.declare('CTV', ('ct', ct))
IntOrCT = u.create()
CTV = IntOrCT.CTV
IntV = IntOrCT.IntV
Теперь я пытаюсь использовать их в массиве. Однако я не могу добавить целые числа в свои массивы и получить: z3.z3types.Z3Exception: Z3 expression expected
# X = Array('x', IntOrCT, IntOrCT)
# Store(X, 0, 4)
Если я изменю IntOrCT на IntSort(), это сработает. Есть идеи, чего может не хватать в коде? или то, что я пытаюсь сделать, невозможно в z3?
Ответы 1
Вы создали массив, индексированный IntOrCT, в котором хранятся IntOrCT значения; поэтому вам нужно обернуть свой индекс и значения в соответствующие конструкторы:
X = Array('x', IntOrCT, IntOrCT)
print(Store(X, IntV(0), IntV(4)))
Когда я запускаю это, я получаю:
Store(x, IntV(0), IntV(4))