CODEWITHSUNDEEP
z3z3py
JRR
JRR

Reputation: 6152

parametric data types in z3py

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 )) ))))

Upvotes: 0

Views: 124

Answers (1)

alias
alias

Reputation: 30428

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)

Upvotes: 1

Related Questions