Types de données avec des fonctions comme attributs dans Z3 Python

Question

J'utilise les liaisons Python pour Z3 et essaye de créer un type de données Z3 dont les attributs sont des fonctions. Par exemple, je pourrais exécuter les suivantes:

Foo = Datatype('Foo') 
Foo.declare('foo', [('my_function', Function('f', IntSort(), BoolSort()))]) 
Foo.create() 

Ceci est une tentative de créer un type de données Foo avec l'attribut my_function, où je serais en mesure d'appeler my_function x (si x est une variable de type Foo) afin de sortez de la fonction d'ints à bools.

Cependant, je rencontre l'erreur suivante à la deuxième ligne:

z3types.Z3Exception: Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort) 

Est-il possible de déclarer Z3 avec fonctions types de données attributs, en utilisant peut-être une syntaxe différente?

Ou est-ce quelque chose qui n'est pas autorisé? Le message function declaration in z3 me suggère que les fonctions d'ordre supérieur ne sont pas autorisées dans Z3, donc peut-être que l'ajout d'une fonction à un type de données n'est pas autorisé afin d'empêcher la création de fonctions d'ordre supérieur utilisant ces types de données.

Answer 1

Vous pouvez utiliser le type de tableau pour coder des espaces de fonction.

Foo = Datatype('Foo') 
Foo.declare('foo', ('my_function', ArraySort(IntSort(), BoolSort()))) 
print Foo.create()