时间戳

首页 > 解决方案 > z3py 中的参数数据类型

z3 - z3py 中的参数数据类型

问题描述

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

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

标签： z3z3py

解决方案

是的。见这里：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)

推荐阅读