Моделирование вложенных кортежей / последовательностей в z3

Question

В настоящее время я создаю механизм символьного исполнения для небольшого подмножества Python. Самая сложная структура данных, поддерживаемая этим подмножеством, - это произвольно вложенные кортежи , то есть вы можете написать что-то вроде x = (1, 2, (3, 4), 5). В моем движке SE все значения представлены как объекты z3. Вчера мне было довольно сложно смоделировать эти вложенные кортежи в z3.

Что я пробовал:

• Массивы. Проблема: массивы - это, в общем, массивы, т. Е. Они охватывают прямоугольное пространство, что не подходит для моих кортежей.
• Последовательности. Мне нравится тип данных "последовательности"; однако он не поддерживает вложение. Например, вы не можете писать z3.Concat(z3.Unit(z3.IntVal(1)), z3.Unit(z3.Concat(z3.Unit(z3.IntVal(2)), z3.Unit(z3.IntVal(3))))), что вызывает z3.z3types.Z3Exception: b"Sort of function 'seq.++' does not match the declared type. Given domain: (Seq Int) (Seq (Seq Int))"
• Списки. Однако списки имеют один тип T, который я могу создать только для List или , например, Int. Насколько я знаю, в z3 нет чего-то вроде типов объединения или общего суперсорта.
• Неинтерпретируемые функции. Я думаю, что можно было бы ввести функцию tuple с сортировкой Tuple, и даже перегружать его для аргументов разной длины и сортировки. Однако я не знаю, как извлечь элемент из tuple(1, 2, 3), поскольку это выражение не определено рекурсивно.

Буду признателен за любую помощь экспертов по z3 / SMT здесь!

Заранее большое спасибо!

Answer 1

Почему бы просто не использовать кортежи для моделирования кортежей? Вы можете объявить общий кортежный тип, а затем многократно создавать его экземпляры для обработки вложенных.

Вот пример: https://rise4fun.com/z3/tutorialcontent/guide#h27, и то же самое можно закодировать и в z3py. См. Также https://ericpony.github.io/z3py-tutorial/advanced-examples.htm для получения дополнительных примеров. Официальное описание поддержки типов данных в SMTLib см. В разделе 4.2.3 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf .

Обратите внимание, что для каждого типа кортежа, который у вас будет, вам нужно будет объявить новый тип кортежа. В этом смысле SMT не является полиморфным. Этот процесс обычно называют мономорфизацией. Если в результате получается, что язык, который вы моделируете, имеет переменные, которые могут «изменять» форму (т. Е. Простой кортеж из двух кортежей становится кортежем из трех после присваивания), вам придется учитывать эту новую переменную и моделировать ее как такой. (Но это ничем не отличается от переменной, которой назначается int, а затем логическое значение. SMTLib является «просто типизированной», т. Е. Все переменные всегда имеют один объявленный тип.)

Попробуйте эту идею, и если вы столкнетесь с проблемами, отправьте образцы кода.