Types de données mutuellement récursifs dans z3 et leur interaction avec les types intégrés

Question

J'essaie actuellement d'utiliser Z3 pour coder une logique de programme simple pour un langage non typé avec des listes polymorphes. Pour autant que je sache, à partir de the Z3 tutorial by Moura and Bjorner, il n'est pas possible d '"imbriquer des définitions de type de données récursives à l'intérieur d'autres types, tels que des tableaux".

Ainsi, supposons que je le type OCaml suivant:

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

Idéalement, je voudrais encoder ce type dans Z3 en utilisant le type Z3List intégré, mais je pense que cela est impossible, parce que Z3 ne prend pas en charge la récurrence mutuelle entre les types de données récursifs et les autres types. Quelqu'un peut-il confirmer que c'est le cas? Si c'est le cas, je suppose que la seule façon possible est de définir mon propre type pour une liste de valeurs, disons my_list, et que les types my_list et value soient mutuellement récursifs. En OCaml:

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

Mais cela signifie que je ne serai pas en mesure de tirer parti de l'infrastructure de raisonnement intégré qui prend en charge Z3 pour Z3Lists. Y a-t-il une meilleure manière de faire cela?

Answer 1

Il est correct que vous deviez utiliser la version aplatie avec my_list. La bonne nouvelle est que le raisonnement intégré sur les listes de Z3 utilise exactement le même mécanisme que les autres types de données, de sorte que vous obtiendrez le même raisonnement avec la déclaration de type de données.