2

ここで説明したのと同じ理由で (ユーザー定義の未解釈関数)、独自の未解釈関数を定義したい

bvredxnor() : 指定されたビットベクトルのビットに対する xnor。

ここに示されている例 ( C API を使用したユニバーサル量指定子の例) に従うと、関数 (ビットベクトル) の引数にどのような種類を指定すればよいかわかりません。

指定された長さのビットベクトルの並べ替えを作成できましたが、任意の長さのビットベクトルに使用したいと考えています。

C API で利用可能なビットベクター関数を調べたところ、すべての引数の型が Z3_ast であることがわかったので、同じジェネリック型を使用できると考えていました。しかし、APIにはZ3_astソートを生成する関数はありません...（これを書いていると、タイプとソートの違いに触れているように感じますが、まだ少し不明です）

解釈されないソートを使用する解決策はありますか? もしそうなら、それを行う際に、型を大きくしすぎてモデルの精度をいくらか失うことはありませんか?このアーティファクトはデバッグ目的でのみ使用できますか? つまり、この関数をビットベクトルに適用すると、これは機能しますか?

前もって感謝します、

AG。

4

1 に答える 1

2

SMTLibは、可変長のビットベクトルを許可しません。つまり、ビットベクトルの長さにわたってパラメーター化された問題を表現することはできません。この理由は、カーディナリティの問題により、ビットベクトルに関するプロパティが必ずしも長さにわたってパラメトリックに保持されるとは限らないためです。つまり、次のことを考慮してください。

exists x0, x1, x2, x3, x4. distinct [x0, x1, x2, x3, x4]

このプロパティは、少なくとも5つの異なるビットベクトル値があることを示しています。これは、xの定義域の長さが3以上の場合に当てはまりますが、それ以外の場合は当てはまりません。したがって、ステートメントの有効性はドメインによって異なります。これは、一般的なSMTLibの1次的な性質の制限と見なすこともできます。

もちろん、上記はSMTLibに適用され、必ずしもZ3には適用されません。Leoと共同研究者は常に時代を先取りしており、Z3にはSMTLibが求めるものを超える多くのトリックがあります。Z3が、説明している方法でパラメトリックビットベクトル問題の概念をサポートしているとしたら、それは嬉しい驚きです。

于 2012-04-26T16:33:10.237 に答える