z3py 中的参数数据类型

【问题标题】：parametric data types in z3pyz3py 中的参数数据类型
【发布时间】：2020-05-10 04:22:03
【问题描述】：

z3py 是否具有创建参数数据类型的功能，例如使用以下 SMTLIB 代码生成的数据类型？

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

【问题讨论】：

标签： z3 z3py

【解决方案1】：

是的。见这里：https://ericpony.github.io/z3py-tutorial/advanced-examples.htm

搜索标题为“数据类型”的部分。

这是该页面中的示例，完全符合您的要求：

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)

【讨论】：