1

Z3は整数の最小関数をサポートしていますか？つまり、最小2つの数値を返しますか？Z3のWebサイトで見つかりませんでした。

さらに、最小の数値セットを返すことができるある種の関数をサポートしていますか？次のようなもの：（assert（= y（min x1 x2 x3 x4 x5）））、ここでxとyは整数です。

ありがとう。

4

1 に答える 1

1

minは、今後の浮動小数点理論の予約キーワードです。コマンドを使用しdefine-funて、マクロmin2(バイナリ)、 (ターナリ) などを定義できます。 、 、および をmin3定義する例を次に示します。min2min3min4

http://rise4fun.com/Z3/akWje

SMT 2.0 標準は、任意の数の引数を持つマクロをサポートしていません。必要に応じて、Z3 API の 1 つを使用してそれを行うことができます。Python フロントエンドは非常に柔軟です。これは Z3Py の例です。

http://rise4fun.com/Z3Py/Vvp

于 2012-06-27T06:51:41.977 に答える