parametric data types in z3py

0
votes

Does z3py have functions to create a parametric data type, like what would be generated using the following SMTLIB code?

( declare - datatype List ( par ( T )
( ( nil ) ( cons ( car T ) ( cdr ( List T )) ))))
1
z3z3py

1 Answers

1
votes

Yes. See here: https://ericpony.github.io/z3py-tutorial/advanced-examples.htm

Search for the section titled "Datatypes."

Here's the example right from that page, that does exactly what you want:

def DeclareList(sort):
    List = Datatype('List_of_%s' % sort.name())
    List.declare('cons', ('car', sort), ('cdr', List))
    List.declare('nil')
    return List.create()

IntList     = DeclareList(IntSort())
RealList    = DeclareList(RealSort())
IntListList = DeclareList(IntList)