Взаимно рекурсивные типы данных в z3 и их взаимодействие со встроенными типами

В настоящее время я пытаюсь использовать Z3 для кодирования простой программной логики для нетипизированного языка с полиморфными списками.

Насколько я понимаю, из учебника Z3 Моуры и Бьорнера, это не возможно «вкладывать рекурсивные определения типов данных в другие типы, такие как массивы».

Итак, предположим, у меня есть следующий тип OCaml:

type value =
    | Num of float
    | String of string
    | List of value list

В идеале я хотел бы закодировать этот тип в Z3, используя встроенный тип Z3List, но я думаю, что это невозможно, потому что Z3 не поддерживает взаимную рекурсию между рекурсивными типами данных и другими типами . Может кто-нибудь подтвердить, что это так?

Если это так, я думаю, что единственный возможный способ для меня - определить мой собственный тип для списка значений, скажем my_list, и для типов my_list и value, чтобы они были взаимно рекурсивными. В OCaml:

type value =
    | Num    of float
    | String of string
    | List   of my_list
and my_list =
    | Cons   of value * my_list
    | nil

Но это означает, что я не смогу использовать встроенную инфраструктуру рассуждений, которую Z3 поддерживает для Z3Lists. Есть лучший способ сделать это?


logic recursive-datastructures z3 smt ocaml
person j3fsantos    schedule 24.04.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Правильно, что вам придется использовать сплющенную версию с my_list. Хорошая новость заключается в том, что встроенные рассуждения в списках в Z3 используют тот же механизм, что и другие типы данных, поэтому вы получите такую ​​же поддержку рассуждений с объявлением плоского типа данных.

person Nikolaj Bjorner    schedule 24.04.2017