2

Z3 の Python バインディングを使用して、属性が関数である Z3 データ型を作成しようとしています。たとえば、次のように実行します。

Foo = Datatype('Foo')
Foo.declare('foo', [('my_function', Function('f', IntSort(), BoolSort()))])
Foo.create()

これは、int から bool への関数を取得するために(が type の変数である場合)呼び出すことができる、Fooattributeを使用してデータ型を作成しようとする試みです。my_functionmy_function xxFoo

ただし、2 行目で次のエラーが発生します。

z3types.Z3Exception: Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)

おそらく別の構文を使用して、関数を属性として Z3 データ型を宣言することは可能ですか?

それとも許されないものですか？z3の事後関数宣言は、Z3 では高階関数が許可されていないことを示唆しているため、これらのデータ型を使用した高階関数の作成を防ぐために、データ型に関数を追加することは許可されていない可能性があります。

4

1 に答える 1

2

Array 型を使用して、関数空間をエンコードできます。

Foo = Datatype('Foo')
Foo.declare('foo', ('my_function', ArraySort(IntSort(), BoolSort())))
print Foo.create()
于 2016-02-29T20:36:13.843 に答える