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)スローの使用を試みる:

AttributeError: DatatypeRef instance has no attribute '__len__'

データ型の定量化を一般的にどのように処理する必要があるか、誰にもアイデアはありますか?

4

1 に答える 1

2

sort の定数を作成するにListは、プロシージャを使用する必要がありますConst。

ls = Const('ls', List)

Z3Py では、プロシージャForAllとExistsは、引数として Z3 定数を取る C API に基づいています。ほとんどのユーザーは、de Bruijn インデックスに基づくものよりもこれらの C 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 に答える