z3py 中的参数数据类型

Question

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

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

Answer 1

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

搜索标题为 "Datatypes."

的部分

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

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)

z3py 中的参数数据类型

parametric data types in z3py

z3

z3py