0

Z3Py で別の代数データ型に依存する代数データ型を作成できるかどうか疑問に思っています。

例として、独自の Bool データ型を定義し、Bool のリストを自分で定義したいとします。

from z3 import *
Bool = Datatype('Bool')
Bool.declare('TRUE')
Bool.declare('FALSE')
Bool = Bool.create()
TRUE = Bool.TRUE
FALSE = Bool.FALSE

これはうまくいきます：

BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
BoolList = BoolList.create()

これは次のメッセージで失敗します。

>>> BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: DatatypeSortRef instance has no __call__ method

その理由は、以前に定義されたデータ型への参照として Bool() が使用されているためです。代わりに Z3 ブールソートを使用すると、魅力的に機能します。

BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', BoolSort()), ('tail', BoolList))

別の代数データ型に依存する代数データ型の定義は不可能ですか、それとも s.th を渡す必要がありますか? Bool() 以外？

前もって感謝します！カルステン

4

1 に答える 1

1

さて、私は括弧を使用してはいけないところに使用したことが判明しました - カスタムデータ型「Bool」への参照は呼び出す必要はありません:

BoolList.declare('bCONS', ('hd', Bool), ('tail', BoolList))

うまく動作します:)

于 2014-05-12T11:57:46.733 に答える