1

在使用 Z3Py 时，我定义了一个整数列表，如下所示：

List = Datatype('List')
List.declare('cons', ('head', IntSort()), ('tail', List))
List.declare('nil')
List = List.create()

现在，我在该列表上定义了一些简单的函数，如下所示：

len = Function('len', List, IntSort())

def len_defn():
  ls = List('ls')
  return And([
    len(List.nil) == 0,
    ForAll(ls, Implies(List.is_cons(ls), len(ls) == 1+len(List.tail(ls))))
  ])

不幸的是，这最终失败了，因为ls = List('ls')抛出了错误：

AttributeError: DatatypeSortRef instance has no __call__ method

尝试使用ls = Var(0, List)throw：

AttributeError: DatatypeRef instance has no attribute '__len__'

有谁知道通常应该如何处理数据类型的量化？

4

1 回答 1

2

要创建排序常量List，我们应该使用过程Const。

ls = Const('ls', List)

在 Z3Py 中，过程ForAll和Exists基于将 Z3 常量作为参数的 C API。大多数用户发现这些 C API 比基于 de Bruijn 索引的 API 更易于使用。

另一个问题，我们不应该重新定义len. len是一个 Python 内置函数。为避免您的程序出现问题，我们应该使用

Len = Function('len', List, IntSort())

这是重写的示例（也可在此处在线获得）

List = Datatype('List')
List.declare('cons', ('head', IntSort()), ('tail', List))
List.declare('nil')
List = List.create()
Len = Function('len', List, IntSort())

def len_defn():
  ls = Const('ls', List)
  return And([
    Len(List.nil) == 0,
    ForAll(ls, Implies(List.is_cons(ls), Len(ls) == 1+Len(List.tail(ls))))
  ])

print len_defn()
于 2013-03-04T17:08:08.347 回答