对数据类型进行量化

Question

在使用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)抛出：

AttributeError: DatatypeRef instance has no attribute '__len__'

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

Answer 1

为了创建一个排序为List的常量，我们应该使用Const过程。

ls = Const('ls', List)

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

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

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

以下是重写的示例(also available online here)

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